Improving saturation-based bounded model checking
Formal verification is becoming a fundamental step in assuring the correctness of safety-critical systems. Since these systems are often asynchronous and even distributed, their verification requires methods that can deal with huge or even infinite state spaces. Model checking is one of the current...
Elmentve itt :
| Szerzők: | |
|---|---|
| Dokumentumtípus: | Cikk |
| Megjelent: |
2016
|
| Sorozat: | Acta cybernetica
22 No. 3 |
| Kulcsszavak: | Aszinkron rendszerek - telítettség |
| Tárgyszavak: | |
| doi: | 10.14232/actacyb.22.3.2016.2 |
| Online Access: | http://acta.bibl.u-szeged.hu/40263 |
| LEADER | 01729nab a2200253 i 4500 | ||
|---|---|---|---|
| 001 | acta40263 | ||
| 005 | 20220620124049.0 | ||
| 008 | 170214s2016 hu o 0|| eng d | ||
| 022 | |a 0324-721X | ||
| 024 | 7 | |a 10.14232/actacyb.22.3.2016.2 |2 doi | |
| 040 | |a SZTE Egyetemi Kiadványok Repozitórium |b hun | ||
| 041 | |a eng | ||
| 100 | 1 | |a Darvas Dániel | |
| 245 | 1 | 0 | |a Improving saturation-based bounded model checking |h [elektronikus dokumentum] / |c Darvas Dániel |
| 260 | |c 2016 | ||
| 300 | |a 573-589 | ||
| 490 | 0 | |a Acta cybernetica |v 22 No. 3 | |
| 520 | 3 | |a Formal verification is becoming a fundamental step in assuring the correctness of safety-critical systems. Since these systems are often asynchronous and even distributed, their verification requires methods that can deal with huge or even infinite state spaces. Model checking is one of the current techniques to analyse the behaviour of systems, as part of the verification process. In this paper a symbolic bounded model checking algorithm is presented that relies on efficient saturation-based methods. The previous approaches are extended with new bounded state space exploration strategies. In addition, constrained saturation is also introduced to improve the efficiency of bounded model checking. Our measurements confirm that these approaches do not only offer a solution to deal with infinite state spaces, but in many cases they even outperform the original methods. | |
| 650 | 4 | |a Természettudományok | |
| 650 | 4 | |a Számítás- és információtudomány | |
| 695 | |a Aszinkron rendszerek - telítettség | ||
| 700 | 0 | 1 | |a Vörös András |e aut |
| 700 | 0 | 1 | |a Bartha Tamás |e aut |
| 856 | 4 | 0 | |u http://acta.bibl.u-szeged.hu/40263/1/actacyb_22_3_2016_2.pdf |z Dokumentum-elérés |