Search

In this paper, we provide a toolchain that facilitates the integration of formal verification techniques into model-based design. Applying verification tools to industrially relevant models requires three main ingredients: a formal model, a formal verification method, and a set of formal specifications. Our focus is on hybrid automata as the model and on reachability analysis as the method. Much progress has been made towards developing efficient and scalable reachability algorithms tailored to hybrid automata. However, it is not easy to encode rich formal specifications such that they can be interpreted by existing tools for reachability. Herein, we consider specifications expressed in pattern templates which are predefined properties with placeholders for state predicates. Pattern templates are close to the natural language and can be easily understood by both expert and non-expert users. We provide (i) formal definitions for selected patterns in the formalism of hybrid automata and (ii) monitors which encode the properties as the reachability of an error state. By composing these monitors with the formal model under study, the property can be checked by off-the-shelf fully automated verification tools. We illustrate the workflow on an electro-mechanical brake use case.

We present the proof-of-concept tool formalSpec for semi-automatic translation of system requirements from controlled natural language into hybrid automata. These can be automatically integrated as monitor automata with an existing SpaceEx system model.