TY - GEN
T1 - Clocks vs. instants relations
T2 - 14th ACM/IEEE International Conference on Formal Methods and Models for System Design, MEMOCODE 2016
AU - Peters, Judith
AU - Przigoda, Nils
AU - Wille, Robert
AU - Drechsler, Rolf
N1 - Publisher Copyright:
© 2016 IEEE.
PY - 2016/12/27
Y1 - 2016/12/27
N2 - The specification of non-functional requirements, e. g., on timing forms an essential part of modern system design. Modeling languages such as MARTE/CCSL provide dedicated description means enabling engineers to formally define the ticking of the clocks to be implemented in terms of clock constraints and the actually intended timing behavior in terms of instant relations. But thus far, instant relations have only been utilized in order to monitor the correct execution of the clock constraints. In this work, we propose a methodology which, for the first time, verifies clock constraints against the given instant relations. To this end, the timing behavior is represented in terms of an automaton followed by its verification through satisfiability solvers. A case study illustrates the application of the proposed methodology.
AB - The specification of non-functional requirements, e. g., on timing forms an essential part of modern system design. Modeling languages such as MARTE/CCSL provide dedicated description means enabling engineers to formally define the ticking of the clocks to be implemented in terms of clock constraints and the actually intended timing behavior in terms of instant relations. But thus far, instant relations have only been utilized in order to monitor the correct execution of the clock constraints. In this work, we propose a methodology which, for the first time, verifies clock constraints against the given instant relations. To this end, the timing behavior is represented in terms of an automaton followed by its verification through satisfiability solvers. A case study illustrates the application of the proposed methodology.
UR - http://www.scopus.com/inward/record.url?scp=85010791792&partnerID=8YFLogxK
U2 - 10.1109/MEMCOD.2016.7797750
DO - 10.1109/MEMCOD.2016.7797750
M3 - Conference contribution
AN - SCOPUS:85010791792
T3 - 2016 ACM/IEEE International Conference on Formal Methods and Models for System Design, MEMOCODE 2016
SP - 78
EP - 84
BT - 2016 ACM/IEEE International Conference on Formal Methods and Models for System Design, MEMOCODE 2016
PB - Institute of Electrical and Electronics Engineers Inc.
Y2 - 18 November 2016 through 20 November 2016
ER -