Integrated Simulation and Formal Verification of a Simple Autonomous Vehicle

被引：9

作者：

Domenici, Andrea ^{[1
]}

Fagiolini, Adriano ^{[2
]}

Palmieri, Maurizio ^{[1
,3
]}

机构：

[1] Univ Pisa, Dept Informat Engn, Pisa, Italy

[2] Univ Palermo, Dept Energy Informat Engn & Math Models DEIM, Palermo, Italy

[3] Univ Florence, DINFO, Florence, Italy

来源：

SOFTWARE ENGINEERING AND FORMAL METHODS, SEFM 2017 | 2018年 / 10729卷

关键词：

FPGAS; PVS;

D O I：

10.1007/978-3-319-74781-1_21

中图分类号：

TP31 [计算机软件];

学科分类号：

081202 ; 0835 ;

摘要：

This paper presents a proof-of-concept application of an approach to system development based on the integration of formal verification and co-simulation. A simple autonomous vehicle has the task of reaching an assigned straight path and then follow it, and it can be controlled by varying its turning speed. The correctness of the proposed control law has been formalized and verified by interactive theorem proving with the Prototype Verification System. Concurrently, the system has been co-simulated using the Prototype Verification System and the MathWorks Simulink tool: The vehicle kinematics have been simulated in Simulink, whereas the controller has been modeled in the logic language of the Prototype Verification System and simulated with the interpreter for the same language available in the theorem proving environment. With this approach, co-simulation and formal verification corroborate each other, thus strengthening developers' confidence in their analysis.

引用

页码：300 / 314

页数：15

共 25 条

[1]

[Anonymous], TECHNICAL REPORT

[2]

Attarzadeh Niaki Seyed Hosein, 2011, 2011 6th IEEE International Symposium on Industrial Embedded Systems (SIES), P238, DOI 10.1109/SIES.2011.5953667

[3] A PVS-Simulink Integrated Environment for Model-Based Analysis of Cyber-Physical Systems [J].

Bernardeschi, Cinzia ;

Domenici, Andrea ;

Masci, Paolo .

IEEE TRANSACTIONS ON SOFTWARE ENGINEERING, 2018, 44 (06) :512-533

[4] Verifying safety properties of a nonlinear control by interactive theorem proving with the Prototype Verification System [J].

Bernardeschi, Cinzia ;

Domenici, Andrea .

INFORMATION PROCESSING LETTERS, 2016, 116 (06) :409-415

[5] ASSESS: A Simulator of Soft Errors in the Configuration Memory of SRAM-Based FPGAs [J].

Bernardeschi, Cinzia ;

Cassano, Luca ;

Domenici, Andrea ;

Sterpone, Luca .

IEEE TRANSACTIONS ON COMPUTER-AIDED DESIGN OF INTEGRATED CIRCUITS AND SYSTEMS, 2014, 33 (09) :1342-1355

[6] GABES: A genetic algorithm based environment for SEU testing in SRAM-FPGAs [J].

Bernardeschi, Cinzia ;

Cassano, Luca ;

Cimino, Mario G. C. A. ;

Domenici, Andrea .

JOURNAL OF SYSTEMS ARCHITECTURE, 2013, 59 (10) :1243-1254

[7]

Blochwitz T., 2011, Proc. 8th Int. Modelica Conf., Dresden, P105, DOI DOI 10.3384/ECP11063105

[8]

Carreño V, 2000, LECT NOTES COMPUT SC, V1869, P90

[9]

Dutertre B., 1996, Theorem Proving in Higher Order Logics. 9th International Conference, TPHOLs'96. Proceedings, P141

[10]

Fitzgerald J. S., 2007, VIENNA DEV METHOD, DOI [10.1002/9780470050118.ecse447, DOI 10.1002/9780470050118.ECSE447]

← 1 2 3 →