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

Chen, Xiaohong; Yin, Ling; Yu, Yijun and Jin, Zhi (2017). Transforming Timing Requirements into CCSL Constraints to Verify Cyber-Physical Systems. In: ICFEM 2017: Formal Methods and Software Engineering, Lecture Notes in Computer Science vol.10610, Springer, Cham, pp. 54–70.

DOI: https://doi.org/10.1007/978-3-319-68690-5_4

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.

Viewing alternatives

Metrics

Public Attention

Altmetrics from Altmetric

Number of Citations

Citations from Dimensions

Item Actions

Export

About

Recommendations