Crynodeb
Engineering of mission critical software requires a program to be verified that it satisfies a number of properties. This is often done using model checking. However, construction of a program model to be verified and analyzing counterexamples is not an easy task. This can be made easier with the automata-based programming paradigm.
There exist some cases when there are many programs to verify and it is impossible to construct a precise enough finite-state model of the environment. We present an approach for automata program verification under such conditions. Our case study is based on 800 automata programs which solve a simple path-planning problem. As a result, we verified that at least 231 of them are provably correct.
There exist some cases when there are many programs to verify and it is impossible to construct a precise enough finite-state model of the environment. We present an approach for automata program verification under such conditions. Our case study is based on 800 automata programs which solve a simple path-planning problem. As a result, we verified that at least 231 of them are provably correct.
Iaith wreiddiol | Saesneg |
---|---|
Teitl | Hardware and Software |
Is-deitl | Verification and Testing 10th International Haifa Verification Conference, HVC 2014, Haifa, Israel, November 18-20, 2014, Proceedings |
Cyhoeddwr | Springer Nature |
Tudalennau | 165-170 |
Nifer y tudalennau | 6 |
ISBN (Electronig) | 978-3-319-13338-6 |
ISBN (Argraffiad) | 978-3-319-13337-9 |
Dynodwyr Gwrthrych Digidol (DOIs) | |
Statws | Cyhoeddwyd - 06 Tach 2014 |
Cyhoeddwyd yn allanol | Ie |
Cyfres gyhoeddiadau
Enw | Lecture Notes in Computer Science |
---|---|
Cyhoeddwr | Springer Nature |
Cyfrol | 8855 |
ISSN (Argraffiad) | 0302-9743 |
ISSN (Electronig) | 1611-3349 |