Specification and Runtime Verification of Temporal Assessments in Simulink
Akshay Rajhans, Anastasia Mavrommati, Pieter Mosterman and Roberto Valenti
Abstract: 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 TestTM 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.