ETL: A New Temporal Language for the Verification of Cyber-Physical Systems

The efficient verification of complex cyber-physical systems such as power plants or power grids requires to use model checking or simulation as early as possible in the engineering process. However, formal methods are difficult to use due to their level of abstraction far from natural language. To alleviate this difficulty, a new high-level requirements modelling language named FORM-L with a precise syntax and semantics adapted to the verification of CPS and still close to natural language was especially conceived for practitioners. This paper presents the syntax and semantics of a new temporal language named ETL (Extended Temporal Language) for the simulation of the temporal aspects of FORM-L. Examples of real-time requirements verification are presented using a Modelica implementation of ETL, in particular regarding the verification of real-time properties of finite-state machines.