Formal Verification of 800 Genetically Constructed Automata Programs: A Case Study

Mikhail. A Lukin, Maxim Buzdalov, A. A. Shalyto

Allbwn ymchwil: Pennod mewn Llyfr/Adroddiad/Trafodion CynhadleddTrafodion Cynhadledd (Nid-Cyfnodolyn fathau)

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.
Iaith wreiddiolSaesneg
TeitlHardware and Software
Is-deitlVerification and Testing 10th International Haifa Verification Conference, HVC 2014, Haifa, Israel, November 18-20, 2014, Proceedings
CyhoeddwrSpringer Nature
Tudalennau165-170
Nifer y tudalennau6
ISBN (Electronig)978-3-319-13338-6
ISBN (Argraffiad)978-3-319-13337-9
Dynodwyr Gwrthrych Digidol (DOIs)
StatwsCyhoeddwyd - 06 Tach 2014
Cyhoeddwyd yn allanolIe

Cyfres gyhoeddiadau

EnwLecture Notes in Computer Science
CyhoeddwrSpringer Nature
Cyfrol8855
ISSN (Argraffiad)0302-9743
ISSN (Electronig)1611-3349

Ôl bys

Gweld gwybodaeth am bynciau ymchwil 'Formal Verification of 800 Genetically Constructed Automata Programs: A Case Study'. Gyda’i gilydd, maen nhw’n ffurfio ôl bys unigryw.

Dyfynnu hyn