Description of the current application |
Our lives become very dependent on various software-intensive systems. They include aircraft, aerospace, railways, automotive devices and controls, medical devices. The software that controls such device is a good example of a safety-critical application. It is clear that our ability to detect defects in such systems (software or devices) is essential and testing, verification and validation are the most important issues in the development of such systems.
Model checking is a formal method that is well suited to prepare testing suit in advance of doing real testing of the device. It is estimated that 30%-70% of the total development cost is related to testing. A model checker is considering every possible combination of system input and state and determines whether or not a specified set of properties is true. The main difficulty of model checking is the so called state explosion. The CPU time and memory required for the verification usually grow exponentially with the size of the system verified. In such situations BOINC type computing projects can become an efficient (and unique!) strategy to allocate very large number of computers, enabling to solve these important applications.
Currently, application (version 6) is solving (crunching) a problem proposed by our colleagues from the KTU Information Technology Development Institute (ITDI) (leader Prof. R. Šeinauskas). The system has 206 inputs and 107 outputs. For each input signal (of length 206, with "0" or "1" value for each input) the system is producing output signal (of length 107, with "0" or "1" value for each output). Input "i" and output "j" are called related if the change in the value of "i" causes the change in the value of "j". The goal is to find all (or at least as many as possible) relations existing in the system under testing. A more detailed description of this problem is given in the following publications: [1], [2].
The problem is that to find all relations we would need to test all possible input signals, which number is 2206, what is impossible, of course. Currently, Monte Carlo based method (proposed by Prof. R. Čiegis, VGTU) is used. Each Working Unit (the single task for client computer) tests a specified number of input signals, randomly generated by using the Monte Carlo method with a given value of threshold parameter. After finishing its computations, the task returns to the project server a matrix of found relations (206x107), which is combined with the matrices obtained earlier by other Working Units.
Literature
1) Bareisa, E.; Jusas, V.; Motiejunas, K.; Seinauskas, R.
The Criteria of Functional Delay Test Quality Assessment.
Proceedings 10th EUROMICRO Conference on Digital System Design, Architectures, Methods and Tools (DSD 2007). 2007, pp. 207-214, ISBN:0-7695-2978-X.
2) Bareisa, E.; Jusas, V.; Motiejunas, K.; Seinauskas, R.
Transition Fault Test Reuse.
Digital System Design: Architectures, Methods and Tools, 2006.
DSD 2006, 9th EUROMICRO Conference. pp. 323-330.