Sciweavers

Share
ICST
2010
IEEE

Timed Moore Automata: Test Data Generation and Model Checking

9 years 8 months ago
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
Helge Löding, Jan Peleska
Added 26 Jan 2011
Updated 26 Jan 2011
Type Journal
Year 2010
Where ICST
Authors Helge Löding, Jan Peleska
Comments (0)
books