Paper Info
Title
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) with an abstraction of time that is suitable for checking timeout behavior of these units. A model checking algorithm for live lock 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.
Year
DOI
Venue
2010
10.1109/ICST.2010.60
ICST
Keywords
Field
DocType
automata theory,program testing,software engineering,Kripke structures,cooperating reactive software components,data generation techniques,industrial train control applications,model checking algorithm,operational semantics,sequential components,timed Moore automata,Timed Moore Automata,livelocks,model checking,model-based testing
Data modeling,Abstraction model checking,Operational semantics,Automata theory,Programming language,Model checking,Computer science,Automaton,Theoretical computer science,Real-time computing,Model-based testing,Test data generation
Conference
Citations 
PageRank 
References 
9
0.84
0
Authors
2
Name
Order
Citations
PageRank
Helge Löding1453.14
Jan Peleska253248.74