Using Formal Methods to Specify Data-Driven Cyber-Physical Systems

This paper presents a review of formal methods, covering both timed automata and Signal Temporal Logic (STL) approaches, and proposes an integration of formal methods with a data-driven representation of an Autonomous Vehicles (AV) case study. The data-driven representation of the system is done through the concept of SmartData, a data construct that includes concepts of location, timing, and semantics, providing an alternative to represent critical systems through the data they rely on. The timing and dependency relationship between different SmartData are derived into an STL expression that specifies the property monitors to verify each piece of data. The same verification is also presented in the form of timed automata, a closer representation of the tools adopted for runtime verification. The SmartData representation and STL and timed automata models are depicted through a case study considering an autonomous vehicles application. Finally, we demonstrate a general scenario for mapping data-driven systems using SmartData directly into timed automata.