Obtaining Trust In Autonomous Systems: Tools For Formal Model Synthesis And Validation

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.