Specification and Runtime Verification of Temporal Assessments in Simulink

Formalization of specifications is a key step towards rigorous system design of complex engineered systems such as cyber physical systems. Temporal logics are a suitable expressive formalism for capturing temporal specifications. However, since engineers and practitioners are often unfamiliar with the symbols and vocabulary of temporal logic, informal natural-language specifications still are used abundantly in practice. This tool paper presents the Temporal Assessments feature in Simulink^® Test™ that strives to achieve the best of both worlds. It provides graphical user interfaces and visual examples for users to interactively create temporal specifications without the need to author logical formulae by hand, yet any user-authored temporal assessment is a valid logical formula in an internal representation. Iterative folding of clauses enables the specification to be presented to read like English language sentences. Key highlights of the feature along with examples of authoring and runtime verification of temporal logic specifications are presented.

This is the authors’ preprint. The paper appears in the Proceedings of the International Conference on Runtime Verification (RV) 2021. The final authenticated version is available online.

Read full paper.