@inproceedings{1e18e872dba64f14b049f2ea6595f646,
title = "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.",
keywords = "CCSL, Dynamic logic, Schedulability analysis",
author = "Yuanrui Zhang and Frederic Mallet and Huibiao Zhu and Yixiang Chen",
note = "Publisher Copyright: {\textcopyright} 2019 IEEE.; 13th International Symposium on Theoretical Aspects of Software Engineering, TASE 2019 ; Conference date: 29-07-2019 Through 31-07-2019",
year = "2019",
month = jul,
doi = "10.1109/TASE.2019.00-23",
language = "英语",
series = "Proceedings - 2019 13th International Symposium on Theoretical Aspects of Software Engineering, TASE 2019",
publisher = "Institute of Electrical and Electronics Engineers Inc.",
pages = "25--32",
booktitle = "Proceedings - 2019 13th International Symposium on Theoretical Aspects of Software Engineering, TASE 2019",
address = "美国",
}