Title
Obtaining Trust in Autonomous Systems: Tools for Formal Model Synthesis and Validation
Abstract
An important and growing class of cyber physical systems are autonomous vehicles (AVs). While the U.S. military has used AVs, such as unmanned air vehicles, for many years, civilian use of these vehicles, e.g., by the FBI, has been steadily increasing. Plans to equip AVs with cameras, scientific instruments, and weapons, such as tear gas and pepper spray, have led to growing mistrust of AVs and calls for greater human control and oversight. This paper describes two kinds of trust needed in systems involving AVs and how a formal model and model-based simulation can help obtain such trust. It introduces two new tools to be integrated into FOrmal Requirements Modeling and AnaLysis (FORMAL), an upgrade of NRL's Software Cost Reduction (SCR) toolset; the new tools support formal modeling and symbolic execution (via simulation) of cyber physical systems. The first tool synthesizes a formal model from scenarios. The synthesized model forms a basis for formal verification, and for model validation using simulation. The second tool, which combines the existing SCR simulator with the eBotworks 3D autonomy simulator, overcomes the SCR simulator's major limitations---its support for only discrete computation and its inability to simulate continuous movement. To evaluate the new tools, the paper describes synthesis of a formal model of a Navy unmanned ground vehicle currently under development and simulation of its behavior.
Year
DOI
Venue
2015
10.1109/FormaliSE.2015.16
FormaliSE@ICSE
Field
DocType
ISSN
Model checking,Systems engineering,Computer science,Unmanned ground vehicle,Real-time computing,Scientific instrument,Cyber-physical system,Autonomous system (Internet),Symbolic execution,Formal methods,Embedded system,Formal verification
Conference
2380-873X
ISBN
Citations 
PageRank 
978-1-5386-0422-9
0
0.34
References 
Authors
17
2
Name
Order
Citations
PageRank
Constance L. Heitmeyer1898151.71
Elizabeth I. Leonard21108.48