SMT-Based Bounded Schedulability Analysis of the Clock Constraint Specification Language

Abstract : The Clock Constraint Specification Language (CCSL) is a formalism for specifying logical-time constraints on events for the design of real-time embedded systems. A central verification problem of CCSL is to check whether events are schedulable under logical constraints. Although many efforts have been made addressing this problem, the problem is still open. In this paper, we show that the bounded scheduling problem is NP-complete and then propose an efficient SMT-based decision procedure which is sound and complete. Based on this decision procedure , we present a sound algorithm for the general scheduling problem. We implement our algorithm in a prototype tool and illustrate its utility in schedulability analysis in designing real-world systems and automatic proving of algebraic properties of CCSL constraints. Experimental results demonstrate its effectiveness and efficiency.
Document type :
Conference papers
Complete list of metadatas

Cited literature [3 references]  Display  Hide  Download

https://hal.inria.fr/hal-02080763
Contributor : Frédéric Mallet <>
Submitted on : Wednesday, March 27, 2019 - 8:25:13 AM
Last modification on : Thursday, March 28, 2019 - 3:25:18 AM
Long-term archiving on : Friday, June 28, 2019 - 12:50:10 PM

File

paper_30.pdf
Files produced by the author(s)

Identifiers

  • HAL Id : hal-02080763, version 1

Collections

Citation

Min Zhang, Fu Song, Frédéric Mallet, Chen Xiaohong. SMT-Based Bounded Schedulability Analysis of the Clock Constraint Specification Language. FASE 2019 - Fundamental Approaches to Software Engineering, Apr 2019, Prague, Czech Republic. ⟨hal-02080763⟩

Share

Metrics

Record views

77

Files downloads

148