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

https://hal.inria.fr/hal-02402976
Contributor : Frédéric Mallet <>
Submitted on : Monday, January 6, 2020 - 4:26:10 PM
Last modification on : Tuesday, January 7, 2020 - 8:59:02 AM

File

TASE_2019_paper_30_190125.pdf
Files produced by the author(s)

Identifiers

Collections

Citation

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⟩

Share

Metrics

Record views

29

Files downloads

47