Quang-Minh Ta
LIPN, Université Sorbonne Paris Nord
Cyber-physical systems are ubiquitous in modern society and are characterized by the use of computational algorithms to control and interact with physical processes in real time.
Many methods have been proposed to verify their component properties in real time. In [WAH23], the verification problem is reduced to a pattern-matching problem, where the execution log is represented as a timed word and the specification is expressed as a timed automaton. This approach allows for the evaluation of parameter constraints that enable the property to hold.
Patterns [GHJV93] were originally designed to unify recurring structures in the software development process. The idea of using patterns to simplify the specification process for non-expert practitioners was later proposed in [DAC98]. Subsequent works on specification patterns, such as [And13] and [AP15], adapted and enriched these patterns for use in different contexts, particularly concurrent real-time systems, while also providing concrete software implementations and generalizing previous approaches.
In this work, we propose a new set of patterns specialized for the monitoring of cyber-physical systems. The proposed patterns are based on [AP15] and certain technique introduced in [WAH23], significantly simplifying the specification process for end users.
For example, a user who wishes to verify the property: “If sensor A reaches a certain state, then the read value of sensor B must remain within a specified range for T seconds during a time interval from M to N” would normally need to manually construct a timed automaton containing multiple states and transitions. Our framework instead classifies such specifications into predefined patterns and automatically translates a high-level user-friendly description into the corresponding observer automaton. This relieves users of the need to understand the internal mechanisms of the verification process.
The proposed pattern set is expressive and includes features such as the ability to specify temporal intervals of interest, compatibility with both event-style and signal-style logs, and the ability to express lasting properties of signals. The patterns can also compute essential quantitative information such as maximum/minimum values, occurrence counts in addition to answering Boolean verification queries for properties of different natures.
A concrete implementation of the proposed patterns is being developed as an external Java plugin for the Imitator model checker [And21]. The program accepts specifications written according to the proposed declarative syntax together with execution logs of the target system. It then automatically translates the specifications into observer automata and interfaces with Imitator to produce the final verification results for the user.
[And13] Étienne André. Observer patterns for real-time systems. In 18th International Conference on Engineering of Complex Computer Systems, pages 125–134, 2013.
[And21] Étienne André. Imitator 3: Synthesis of timing parameters beyond decidability. In International Conference on Computer Aided Verification, pages 552–565. Springer, 2021.
[AP15] Étienne André and Laure Petrucci. Unifying patterns for modelling timed relationships in systems and properties. PNSE@ Petri Nets, 1372:25–40, 2015.
[DAC98] Matthew B. Dwyer, George S. Avrunin, and James C. Corbett. Property specification patterns for finite-state verification. In Proceedings of the Second Workshop on Formal Methods in Software Practice, FMSP’98, pages 7–15, New York, NY, USA, 1998. Association for Computing Machinery.
[GHJV93] Erich Gamma, Richard Helm, Ralph Johnson, and John Vlissides. Design patterns: Abstraction and reuse of object-oriented design. In European conference on object-oriented programming, pages 406–431. Springer, 1993.
[WAH23] Masaki Waga, Étienne André, and Ichiro Hasuo. Parametric timed pattern matching. ACM Transactions on Software Engineering and Methodology, 32(1):1–35, 2023.