The Open UniversitySkip to content
 

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 (Digital Object Identifier) Link: https://doi.org/10.1007/978-3-319-68690-5_4
Google Scholar: Look up in Google Scholar

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.

Item Type: Conference or Workshop Item
Copyright Holders: 2017 Springer International Publishing AG
ISBN: 3-319-68689-5, 978-3-319-68689-9
ISSN: 0302-9743
Extra Information: originally presented at IFCEM 2017: International Conference on Formal Engineering Methods, Xi'an, China, 13-17 Nov 2017.
Keywords: cyber-physical systems; problem frames; timing requirements; CCSL constraints
Academic Unit/School: Faculty of Science, Technology, Engineering and Mathematics (STEM) > Computing and Communications
Faculty of Science, Technology, Engineering and Mathematics (STEM)
Item ID: 58379
Depositing User: ORO Import
Date Deposited: 19 Dec 2018 11:32
Last Modified: 29 Mar 2019 10:31
URI: http://oro.open.ac.uk/id/eprint/58379
Share this page:

Metrics

Altmetrics from Altmetric

Citations from Dimensions

Actions (login may be required)

Policies | Disclaimer

© The Open University   contact the OU