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

Mikhail. A Lukin; Maxim Buzdalov; A. A. Shalyto

doi:10.1007/978-3-319-13338-6_13

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

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

ITMO University

Research output: Chapter in Book/Report/Conference proceeding › Conference Proceeding (ISBN)

Abstract

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.

Original language	English
Title of host publication	Hardware and Software
Subtitle of host publication	Verification and Testing 10th International Haifa Verification Conference, HVC 2014, Haifa, Israel, November 18-20, 2014, Proceedings
Publisher	Springer Nature
Pages	165-170
Number of pages	6
ISBN (Electronic)	978-3-319-13338-6
ISBN (Print)	978-3-319-13337-9
DOIs	https://doi.org/10.1007/978-3-319-13338-6_13
Publication status	Published - 06 Nov 2014
Externally published	Yes

Publication series

Name	Lecture Notes in Computer Science
Publisher	Springer Nature
Volume	8855
ISSN (Print)	0302-9743
ISSN (Electronic)	1611-3349

Keywords

automata-based programming
formal verification
model checking

Access to Document

10.1007/978-3-319-13338-6_13

Permanent link

Persistent link

Cite this

Lukin, M. A., Buzdalov, M., & Shalyto, A. A. (2014). Formal Verification of 800 Genetically Constructed Automata Programs: A Case Study . In Hardware and Software: Verification and Testing 10th International Haifa Verification Conference, HVC 2014, Haifa, Israel, November 18-20, 2014, Proceedings (pp. 165-170). (Lecture Notes in Computer Science; Vol. 8855). Springer Nature. https://doi.org/10.1007/978-3-319-13338-6_13

Lukin, Mikhail. A ; Buzdalov, Maxim ; Shalyto, A. A. / Formal Verification of 800 Genetically Constructed Automata Programs : A Case Study . Hardware and Software: Verification and Testing 10th International Haifa Verification Conference, HVC 2014, Haifa, Israel, November 18-20, 2014, Proceedings. Springer Nature, 2014. pp. 165-170 (Lecture Notes in Computer Science).

@inproceedings{fa6ff8c5d6934b609d808e4a6216cbdd,

title = "Formal Verification of 800 Genetically Constructed Automata Programs: A Case Study ",

abstract = "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.",

keywords = "automata-based programming, formal verification, model checking",

author = "Lukin, \{Mikhail. A\} and Maxim Buzdalov and Shalyto, \{A. A.\}",

year = "2014",

month = nov,

day = "6",

doi = "10.1007/978-3-319-13338-6\_13",

language = "English",

isbn = "978-3-319-13337-9",

series = "Lecture Notes in Computer Science",

publisher = "Springer Nature",

pages = "165--170",

booktitle = "Hardware and Software",

address = "Switzerland",

}

Lukin, MA, Buzdalov, M & Shalyto, AA 2014, Formal Verification of 800 Genetically Constructed Automata Programs: A Case Study . in Hardware and Software: Verification and Testing 10th International Haifa Verification Conference, HVC 2014, Haifa, Israel, November 18-20, 2014, Proceedings. Lecture Notes in Computer Science, vol. 8855, Springer Nature, pp. 165-170. https://doi.org/10.1007/978-3-319-13338-6_13

Formal Verification of 800 Genetically Constructed Automata Programs: A Case Study . / Lukin, Mikhail. A; Buzdalov, Maxim; Shalyto, A. A.
Hardware and Software: Verification and Testing 10th International Haifa Verification Conference, HVC 2014, Haifa, Israel, November 18-20, 2014, Proceedings. Springer Nature, 2014. p. 165-170 (Lecture Notes in Computer Science; Vol. 8855).

Research output: Chapter in Book/Report/Conference proceeding › Conference Proceeding (ISBN)

TY - GEN

T1 - Formal Verification of 800 Genetically Constructed Automata Programs

T2 - A Case Study

AU - Lukin, Mikhail. A

AU - Buzdalov, Maxim

AU - Shalyto, A. A.

PY - 2014/11/6

Y1 - 2014/11/6

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

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

KW - automata-based programming

KW - formal verification

KW - model checking

UR - https://www.scopus.com/pages/publications/84921654147

U2 - 10.1007/978-3-319-13338-6_13

DO - 10.1007/978-3-319-13338-6_13

M3 - Conference Proceeding (ISBN)

SN - 978-3-319-13337-9

T3 - Lecture Notes in Computer Science

SP - 165

EP - 170

BT - Hardware and Software

PB - Springer Nature

ER -

Lukin MA, Buzdalov M, Shalyto AA. Formal Verification of 800 Genetically Constructed Automata Programs: A Case Study . In Hardware and Software: Verification and Testing 10th International Haifa Verification Conference, HVC 2014, Haifa, Israel, November 18-20, 2014, Proceedings. Springer Nature. 2014. p. 165-170. (Lecture Notes in Computer Science). Epub 2014 Nov 3. doi: 10.1007/978-3-319-13338-6_13

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

Abstract

Publication series

Keywords

Access to Document

Permanent link

Other files and links

Fingerprint

Cite this