|Keywords:||model checking; model-based testing; laziness; parallelization; heuristics|
|Full text PDF:||http://digbib.ubka.uni-karlsruhe.de/volltexte/documents/3891208|
This thesis focuses on the lightweight formal method of model-based testing for checking safety properties, and derives a new and more feasible approach. For liveness properties, dynamic testing is impossible, so feasibility is increased by specializing on an important class of properties, livelock freedom, and deriving a more feasible model checking algorithm for it. All mentioned improvements are substantiated by experiments.