An Executable Semantics of Clock Constraint Specification Language and its Applications

Min Zhang 1 Frédéric Mallet 2
2 AOSTE - Models and methods of analysis and optimization for systems with real-time and embedding constraints
Inria de Paris, CRISAM - Inria Sophia Antipolis - Méditerranée , Laboratoire I3S - COMRED - COMmunications, Réseaux, systèmes Embarqués et Distribués
Abstract : The Clock Constraint Specification Language (ccsl) is a language to specify logical and timed constraints between logical clocks. Given a set of clock constraints specified in ccsl, formal analysis is preferred to check if there exists a schedule that satisfies all the constraints, if the constraints are valid or not, and if the constraints satisfy expected properties. In this paper, we present a formal executable semantics of ccsl in rewriting logic and demonstrate some applications of the formal semantics to its formal analysis: 1) to automatically find bounded or periodic schedules that satisfy all the given constraints; 2) to simulate the execution of schedules with customized simulation policies; and 3) to verify LTL properties of ccsl constraints by bounded model checking. Compared with other existing modeling approaches, advantages with the rewriting-based semantics of ccsl are that we do not need to assume a bounded number of steps for the formalization, and we can exhaustively explore all the solutions within a given bound for the analysis.
Document type :
Conference papers
Complete list of metadatas

Cited literature [15 references]  Display  Hide  Download

https://hal.inria.fr/hal-01353824
Contributor : Frédéric Mallet <>
Submitted on : Sunday, August 14, 2016 - 4:03:42 PM
Last modification on : Monday, November 5, 2018 - 3:36:03 PM
Long-term archiving on : Tuesday, November 15, 2016 - 10:25:08 AM

File

main (1).pdf
Files produced by the author(s)

Identifiers

Collections

Citation

Min Zhang, Frédéric Mallet. An Executable Semantics of Clock Constraint Specification Language and its Applications. Formal Techniques for Safety-Critical Systems, Nov 2015, Luxembourg, Luxembourg. pp.37-51, ⟨10.1007/978-3-319-29510-7_2⟩. ⟨hal-01353824⟩

Share

Metrics

Record views

532

Files downloads

169