SMT-based bounded schedulability analysis of the clock constraint specification language

Min Zhang; Fu Song; Frédéric Mallet; Xiaohong Chen

doi:10.1007/978-3-030-16722-6_4

SMT-based bounded schedulability analysis of the clock constraint specification language

Min Zhang, Fu Song, Frédéric Mallet, Xiaohong Chen

Software Engineering Institute

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › peer-review

12 Scopus citations

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.

Original language	English
Title of host publication	Fundamental Approaches to Software Engineering - 22nd International Conference, FASE 2019, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2019, Proceedings
Editors	Reiner Hähnle, Wil van der Aalst
Publisher	Springer Verlag
Pages	61-78
Number of pages	18
ISBN (Print)	9783030167219
DOIs	https://doi.org/10.1007/978-3-030-16722-6_4
State	Published - 2019
Event	22nd International Conference on Fundamental Approaches to Software Engineering, FASE 2019, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2019 - Prague, Czech Republic Duration: 6 Apr 2019 → 11 Apr 2019

Publication series

Name	Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume	11424 LNCS
ISSN (Print)	0302-9743
ISSN (Electronic)	1611-3349

Conference

Conference	22nd International Conference on Fundamental Approaches to Software Engineering, FASE 2019, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2019
Country/Territory	Czech Republic
City	Prague
Period	6/04/19 → 11/04/19

Keywords

CCSL
Logical time
Real-time system
SMT
Schedulability

Access to Document

10.1007/978-3-030-16722-6_4

Cite this

Zhang, M., Song, F., Mallet, F., & Chen, X. (2019). SMT-based bounded schedulability analysis of the clock constraint specification language. In R. Hähnle, & W. van der Aalst (Eds.), Fundamental Approaches to Software Engineering - 22nd International Conference, FASE 2019, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2019, Proceedings (pp. 61-78). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 11424 LNCS). Springer Verlag. https://doi.org/10.1007/978-3-030-16722-6_4

Zhang, Min ; Song, Fu ; Mallet, Frédéric et al. / SMT-based bounded schedulability analysis of the clock constraint specification language. Fundamental Approaches to Software Engineering - 22nd International Conference, FASE 2019, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2019, Proceedings. editor / Reiner Hähnle ; Wil van der Aalst. Springer Verlag, 2019. pp. 61-78 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).

@inproceedings{bbcc3b4d112a4ba596638adc03a46e9b,

title = "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.",

keywords = "CCSL, Logical time, Real-time system, SMT, Schedulability",

author = "Min Zhang and Fu Song and Fr{\'e}d{\'e}ric Mallet and Xiaohong Chen",

note = "Publisher Copyright: {\textcopyright} The Author(s) 2019.; 22nd International Conference on Fundamental Approaches to Software Engineering, FASE 2019, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2019 ; Conference date: 06-04-2019 Through 11-04-2019",

year = "2019",

doi = "10.1007/978-3-030-16722-6\_4",

language = "英语",

isbn = "9783030167219",

series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",

publisher = "Springer Verlag",

pages = "61--78",

editor = "Reiner H{\"a}hnle and \{van der Aalst\}, Wil",

booktitle = "Fundamental Approaches to Software Engineering - 22nd International Conference, FASE 2019, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2019, Proceedings",

address = "德国",

}

Zhang, M, Song, F, Mallet, F & Chen, X 2019, SMT-based bounded schedulability analysis of the clock constraint specification language. in R Hähnle & W van der Aalst (eds), Fundamental Approaches to Software Engineering - 22nd International Conference, FASE 2019, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2019, Proceedings. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 11424 LNCS, Springer Verlag, pp. 61-78, 22nd International Conference on Fundamental Approaches to Software Engineering, FASE 2019, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2019, Prague, Czech Republic, 6/04/19. https://doi.org/10.1007/978-3-030-16722-6_4

SMT-based bounded schedulability analysis of the clock constraint specification language. / Zhang, Min; Song, Fu; Mallet, Frédéric et al.
Fundamental Approaches to Software Engineering - 22nd International Conference, FASE 2019, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2019, Proceedings. ed. / Reiner Hähnle; Wil van der Aalst. Springer Verlag, 2019. p. 61-78 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 11424 LNCS).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › peer-review

TY - GEN

T1 - SMT-based bounded schedulability analysis of the clock constraint specification language

AU - Zhang, Min

AU - Song, Fu

AU - Mallet, Frédéric

AU - Chen, Xiaohong

N1 - Publisher Copyright: © The Author(s) 2019.

PY - 2019

Y1 - 2019

N2 - 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.

AB - 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.

KW - CCSL

KW - Logical time

KW - Real-time system

KW - SMT

KW - Schedulability

UR - https://www.scopus.com/pages/publications/85064894362

U2 - 10.1007/978-3-030-16722-6_4

DO - 10.1007/978-3-030-16722-6_4

M3 - 会议稿件

AN - SCOPUS:85064894362

SN - 9783030167219

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 61

EP - 78

BT - Fundamental Approaches to Software Engineering - 22nd International Conference, FASE 2019, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2019, Proceedings

A2 - Hähnle, Reiner

A2 - van der Aalst, Wil

PB - Springer Verlag

T2 - 22nd International Conference on Fundamental Approaches to Software Engineering, FASE 2019, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2019

Y2 - 6 April 2019 through 11 April 2019

ER -

Zhang M, Song F, Mallet F, Chen X. SMT-based bounded schedulability analysis of the clock constraint specification language. In Hähnle R, van der Aalst W, editors, Fundamental Approaches to Software Engineering - 22nd International Conference, FASE 2019, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2019, Proceedings. Springer Verlag. 2019. p. 61-78. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)). doi: 10.1007/978-3-030-16722-6_4

SMT-based bounded schedulability analysis of the clock constraint specification language

Abstract

Publication series

Conference

Keywords

Access to Document

Other files and links

Fingerprint

Cite this