Model-Based Scenario Testing and Model Checking with Applications in the Railway Domain
Date Issued
2015-02-05
Author(s)
Supervisors
Referees
Abstract
This thesis introduces Timed Moore Automata, a specification formalism, which extends the classical Moore Automata by adding the concept of abstract timers without concrete delay time values, which can be started and reset, and which can change their state from running to elapsed. The formalism is used in real-world railway domain applications, and algorithms for the automated test data generation and explicit model checking of Timed Moore Automata models are presented. In addition, this thesis deals with test data generation for larger scale test models using standardized modeling formalisms. An existing framework for the automated test data generation is presented, and its underlying work-flow is extended and modified in order to allow user interaction and guidance within the generation process. As opposed to specifying generation constraints for entire test scenarios, the modified work flow then allows for an iterative approach to elaborating and formalizing test generation goals.
Subjects
Moore Automata
;
Domain-specific Languages
;
Unified Modelling Language
;
Model Checking
;
Model-based Testing
;
Interactive Test Generation
;
Scenario Testing
Institution
Type
Dissertation
Secondary publication
No
Language
English
File(s)![Thumbnail Image]()
Loading...
Name
00104235-1.pdf
Size
1.94 MB
Format
Adobe PDF
Checksum
(MD5):adb3c930625b8eb4238589330e0187a2