Transforming Timing Requirements into CCSL Constraints to Verify Cyber-Physical Systems

Abstract

The timing requirements of embedded cyber-physical systems (CPS) constrain CPS behaviors made by scheduling analysis. Lack of physical entity properties modeling and the need of scheduling analysis require a systematic approach to specify timing requirements of CPS at the early phase of requirements engineering. In this work, we extend the Problem Frames notations to capture timing properties of both cyber and physical domain entities into Clock Constraint Specification Language (CCSL) constraints which is more explicit that LTL for scheduling analysis. Interpreting them using operational semantics as finite state machines, we are able to transform these timing requirements into CCSL scheduling constraints, and verify their consistency on NuSMV. Our TimePF tool-supported approach is illustrated through the verification of timing requirements for a representative problem in embedded CPS.