Automated Testing through LTSmin

From Master Projects
Revision as of 11:31, 16 August 2013 by Kdk800 (talk | contribs)

Jump to: navigation, search

has title::Automated Testing through LTSmin
status: ongoing
Master: project within::Technical Artificial Intelligence
Student name: student name::Kevin de Berk
Start start date:=2013/05/06
End end date:=2013/11/01
Supervisor: Wan Fokkink
Company: has company::Axini
Thesis: has thesis::Media:Thesis.pdf
Poster: has poster::Media:Posternaam.pdf

Signature supervisor



It is often said that automated testing can show the presence of bugs, but not their absence. This problem has become especially apparent with modern-day systems, which are often so complex that testing cannot even begin to uncover the vast space of all possible system behaviors. Even with a thoroughly tested complex system, there might still be more bugs that can appear when least expected, with possibly drastic consequences. To ensure the absence of bugs in complex financial systems, computer network protocols, medical systems, and railroad systems; one needs to resort to formal methods.

Formal methods can be applied to expose the complete picture: that there are no bugs. One can manually prove the correctness of a system by e.g. reasoning over the implemented components with induction, but this is often too slow. This process can be automated, but current state-of-the-art solvers still requires too much human guidance to be fully automatic.

A formal method that shows great potential for determining the absence of bugs is model checking. It is easy to automate and it has been used to find bugs in existing systems that were tested. A model checker takes a abstract representation of a system and then checks whether the representation adheres to certain properties. This representation is often a graph where the vertices are the possible system states and the edges the valid transitions from one state to another. A model checker is given a required property encoded in a formal logic, and then visits all reachable states within this graph and tries to find a state that invalidates the property. When it doesn't find such a state, then it has formally shown that the representation is correct with respect to the given property.

Axini is a company located in Amsterdam and is specialized in automated testing. Axini has automated this process by using system requirements to manually generate STS models, and then checking whether the models and the implemented systems agree on certain behaviors w.r.t to the requirements. When they don't, then either the system, the model (or both) are incorrect.

This project is an attempt to build a system that will allow Axini to check their own model for correctness so that they can determine which of the two systems doesn't adhere to the requirements. The model checker will be LTSmin, which is a high-performance model checking tool developed by researchers at the University of Twente.

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.