An increasing number of functionality in today's machine and plant automation is being shifted from pure mechanics or electronics into software. Therefore the system behavior must be checked for compliance with the demanded software functionality by software tests. The precondition for test case execution is a start state, the system has to take in. In order to evaluate the testability of a system, it must be verified whether the test case triggering system state is reachable. We propose a transformation approach of the control software model and the corresponding environment model (physics) to timed automata for model checking to exploit the power of the query language Timed Computation Tree Logic for start state reachability analysis. The applicability is demonstrated on a laboratory plant.      «

An increasing number of functionality in today's machine and plant automation is being shifted from pure mechanics or electronics into software. Therefore the system behavior must be checked for compliance with the demanded software functionality by software tests. The precondition for test case execution is a start state, the system has to take in. In order to evaluate the testability of a system, it must be verified whether the test case triggering system state is reachable. We propose a trans...     »