Timed Moore Automata: Test Data Generation and Model Checking

Abstract—In this paper we introduce Timed Moore Automata, a specification formalism which is used in industrial train control applications for specifying the real-time behavior of cooperating reactive software components. We define an operational semantics for the sequential components (units) abstraction of time that is suitable for checking timeout behavior of these units. A model checking algorithm for livelock detection is presented, and two alternative methods of test case/test data generation techniques are introduced. The first one is based on Kripke structures as used in explicit model checking, while the second method does not require an explicit representation but relies on SAT solving techniques. Keywords-Timed Moore Automata, model-based testing, model checking, livelocks

• Type: Journal
• Year: 2010
• Where: ICST
• Authors: Helge Löding, Jan Peleska
• Keywords: Checking, ICST 2010, Moore Automata, Reactive Software Components, Software Engineering