Automated Testing through LTSmin
|has title::Model checking test models|
|Master:||project within::Technical Artificial Intelligence|
|Student name:||student name::Kevin de Berk|
|Second supervisor:||Machiel van der Bijl|
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.