Defining Contracts for Autonomous Hybrid Systems in Structured Natural Language

In the era of self-driving vehicles and highly autonomous distributed control systems, hybrid systems increasingly use machine learning techniques to make good control decisions in unexpected situations. These systems are often safety-critical, making the application of formal methods to ensure their correctness highly desirable. However, building formal specifications is time-consuming and requires high expertise. In this paper, we present an approach for the definition in structured natural language of formal specifications as they are required for deductive verification of autonomous hybrid systems. To achieve this we extend the Formal Requirements Elicitation Tool (FRET) with templates that support reusable contracts for intelligent hybrid systems. FRET then helps to derive differential dynamic logic (dL) properties and contracts from the requirements written in structured natural language using these templates. The resulting dL specifications can be used both for the deductive verification of a given intelligent hybrid system under the assumption that learning components adhere to their contracts, and to enforce safe actions at runtime. We demonstrate the applicability of our approach with several case studies. We show that the necessary properties and contracts can be derived using our FRET templates.