Automated Testing through LTSmin

has title::Model checking test models
status: finished
Master:	project within::Technical Artificial Intelligence
Student name:	student name::Kevin de Berk
Dates
Start	start date:=2013/05/06
End	end date:=2014/02/14
Supervision
Supervisor:	Wan Fokkink
Second supervisor:	Machiel van der Bijl
Company:	has company::Axini
Thesis:	[[has thesis::Media:Media:http://few.vu.nl/~kdk800/paper.pdf]]
Poster:	has poster::Media:Posternaam.pdf

Signature supervisor

..................................

Abstract

This thesis is about model checking testing models. These testing models are used during the automated testing of software systems and encode symbolic transition systems that are necessarily open. Open models need to be closed before they can be model checked by LTSmin. The open models are closed by the automatic generation and insertion of an environment process. They are then translated to DVE and model checked. The model closing algorithm does preserve the verifiable properties for the models that it can close, but cannot deal with models that have an infinitely large underlying labeled transition system. Future research is suggested to deal with this issue. Keywords: model checking, closing open models, symbolic transition systems, labeled transition systems, Kripke structures, LTL, LTSmin, Ruby, automated testing, software development

Abstract KIM 1

Testing is not enough to ensure the correctness of a system. Model checking is becoming an increasingly more popular solution to this end. With this method, a system is translated to a graph model and then subjected to reachability analysis and cycle detection to determine correctness. Axini is a company specialized in automated testing. They translate system requirements to STS models and want to use model checking to determine the correctness of their models w.r.t. to the original requirements. This project is on connecting their models to a promising model checking tool, LTSmin.