یک منطق پویا مبتنی بر ساعت برای تجزیه و تحلیل زمانبندی مشخصات CCSL
نکات برجسته
خلاصه
کلید واژه ها
1. مقدمه
2. زبان مشخصات محدودیت ساعت
3. یک مثال گویا
4. نحو و معناشناسی cDL
5. حساب اثبات cDL
6. تجزیه و تحلیل برنامه ریزی مشخصات CCSL در cDL
7. مکانیزاسیون cDL
8. کار و بحث مرتبط
9. نتیجه گیری و کارهای آینده
بیانیه مشارکت نویسندگی CRediT
اعلامیه منافع رقابتی
تقدیر و تشکر
ضمیمه A. اثبات گزاره 6.4 و قضیه 6.2
ضمیمه B. اثبات سالم بودن سیستم cDL
منابع
Highlights
Abstract
Keywords
1. Introduction
2. The clock constraint specification language
3. An illustrative example
4. Syntax and semantics of cDL
5. Proof calculus of cDL
6. Schedulability analysis of CCSL specifications in cDL
7. Mechanization of cDL
8. Related work and discussion
9. Conclusion and future work
CRediT authorship contribution statement
Declaration of Competing Interest
Acknowledgements
Appendix A. Proof of Proposition 6.4 and Theorem 6.2
Appendix B. Proof of soundness of cDL system
References
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 . Then solving the schedule problem is equivalent to checking the validity of in the proof system of cDL. By analyzing the proof tree of , 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.
1. Introduction
The clock constraint specification language (CCSL) [2] is a specification language for specifying the constraints between the occurrences of events in real-time embedded systems (RTESs). It was firstly defined as an annex of UML/MARTE [3], but later developed as an independent language equipped with a formal semantics [4]. CCSL gives a concrete syntax to deal with logical clocks, made popular by Leslie Lamport [5] and synchronous languages (such as Esterel). In CCSL, ‘clocks’ are treated as first-class citizens for capturing discrete-time events, and clock expressions are used for specifying the logical and chronometrical constraints between the occurrences of events. CCSL is a specification language and not a programminglanguage. It only allows an abstract specification of a set of possible behaviours and does not attempt to provide a single operational deterministic execution. All the values are ignored to focus only on clock issues. CCSL has been widely used in the specification and analysis of different RTESs, e.g. see [6–8].