@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 = "德国",
}