Difference between revisions of "Automated Testing through LTSmin"

From Master Projects
Jump to: navigation, search
Line 3: Line 3:
 
|Student name=Kevin de Berk
 
|Student name=Kevin de Berk
 
|Project start date=2013/05/06
 
|Project start date=2013/05/06
|Project end date=2013/11/01
+
|Project end date=2014/02/14
 
|Supervisor=Wan Fokkink
 
|Supervisor=Wan Fokkink
 +
|Second supervisor=Machiel van der Bijl
 
|Company=Axini
 
|Company=Axini
|Thesis title=Automated Testing through LTSmin
+
|Thesis title=Model checking test models
|Finished=No
+
|Thesis=http://few.vu.nl/~kdk800/paper.pdf
|Thesis=Thesis.pdf
 
 
|Poster=Posternaam.pdf
 
|Poster=Posternaam.pdf
 +
|Finished=Yes
 
}}
 
}}
  
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.
+
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
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===
 
===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.
 
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.

Revision as of 09:34, 17 February 2014


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: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.