Skip to Main content Skip to Navigation
Conference papers

A Logical Approach for the Schedulability Analysis of CCSL

Abstract : The Clock Constraint Specification Language (CCSL) is a clock-based formalism for formal specification and analysis of real-time embedded systems. Previous approaches for the schedulability analysis of CCSL specifications are mainly based on model checking or SMT-checking. In this paper we propose a logical approach mainly based on theorem proving. We build a dynamic logic called 'clock-based dynamic logic' (cDL) to capture the CCSL specifications and build a proof calculus to analyze the schedule problem of the specifications. Comparing with previous approaches, our method benefits from the dynamic logic that provides a natural way of capturing the dynamic behaviour of CCSL and a divide-and-conquer way for 'decomposing' a complex formula into simple ones for an SMT-checking procedure. Based on cDL, we outline a method for the schedulability analysis of CCSL. We illustrate our theory through one example
Document type :
Conference papers
Complete list of metadatas

Cited literature [24 references]  Display  Hide  Download
Contributor : Frédéric Mallet <>
Submitted on : Monday, January 6, 2020 - 4:26:10 PM
Last modification on : Wednesday, October 14, 2020 - 4:23:26 AM
Long-term archiving on: : Wednesday, April 8, 2020 - 12:10:00 AM


Files produced by the author(s)




Yuanrui Zhang, Frédéric Mallet, Huibiao Zhu, Yixiang Chen. A Logical Approach for the Schedulability Analysis of CCSL. TASE 2019 - 13th International Symposium on Theoretical Aspects of Software Engineering, Jul 2019, Guilin, China. pp.25-32, ⟨10.1109/TASE.2019.00-23⟩. ⟨hal-02402976⟩



Record views


Files downloads