Name
Abstract | ||
|---|---|---|
The Clock Constraint Specification Language (CCSL) is a clock-based formalism for the specification and analysis of real-time embedded systems. The major goal of schedulability analysis of CCSL specifications is to solve the schedule problem, which is to answer 'whether there exists a clock behaviour (also called a 'schedule') that conforms to a given CCSL specification'. Existing works on schedulability analysis of CCSL specifications are mainly based on model checking or SMT-solving. In this paper, however, we propose a theorem-proving approach to the problem. To this end, we define a clock-based dynamic logic (cDL) in which we can specify the clock behaviours and the clock relations in CCSL. With cDL, given a CCSL specification SP, we can express its schedule problem as a cDL formula phi(sp). Then solving the schedule problem is equivalent to checking the validity of phi(sp) in the proof system of cDL. By analyzing the proof tree of phi(sp), we can generate a concrete schedule satisfying SP. Compared to the previous approaches, our method is not limited to special types of CCSL specifications and schedules and does not depend on the bounds that are set for approximate checking. We implement our cDL in Coq. We use an example throughout the paper to illustrate our method. (C) 2020 Elsevier B.V. All rights reserved. |
Year | DOI | Venue |
|---|---|---|
2021 | 10.1016/j.scico.2020.102546 | SCIENCE OF COMPUTER PROGRAMMING |
Keywords | DocType | Volume |
Clock constraint specification language, Dynamic logic, Real-time embedded systems, Schedulability analysis, Theorem proving | Journal | 202 |
ISSN | Citations | PageRank |
0167-6423 | 0 | 0.34 |
References | Authors | |
0 | 6 | |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Yuanrui Zhang | 1 | 7 | 3.58 |
| Frédéric Mallet | 2 | 328 | 34.84 |
| Huibiao Zhu | 3 | 2 | 8.48 |
| YiXiang Chen | 4 | 209 | 36.98 |
| Bo Liu | 5 | 0 | 0.34 |
| Zhiming Liu | 6 | 749 | 58.11 |