یک منطق پویا مبتنی بر ساعت برای تجزیه و تحلیل زمانبندی مشخصات CCSL
ترجمه نشده

یک منطق پویا مبتنی بر ساعت برای تجزیه و تحلیل زمانبندی مشخصات CCSL

عنوان فارسی مقاله: یک منطق پویا مبتنی بر ساعت برای تجزیه و تحلیل زمانبندی مشخصات CCSL
عنوان انگلیسی مقاله: A clock-based dynamic logic for schedulability analysis of CCSL specifications
مجله/کنفرانس: علم برنامه نویسی کامپیوتر - Science of Computer Programming
رشته های تحصیلی مرتبط: مهندسی کامپیوتر
گرایش های تحصیلی مرتبط: مهندسی الگوریتم ها و محاسبات، مهندسی نرم افزار
کلمات کلیدی فارسی: زبان مشخصات محدودیت ساعت، منطق پویا، سیستم های تعبیه شده در زمان واقعی، تجزیه و تحلیل قابلیت زمانبندی، اثبات قضیه
کلمات کلیدی انگلیسی: Clock constraint specification language - Dynamic logic - Real-time embedded systems - Schedulability analysis - Theorem proving
نوع نگارش مقاله: مقاله پژوهشی (Research Article)
نمایه: scopus - master journals - JCR
شناسه دیجیتال (DOI): https://doi.org/10.1016/j.scico.2020.102546
دانشگاه: School of Mathematics and Statistics, Southwest University, China
ناشر: الزویر - Elsevier
نوع ارائه مقاله: ژورنال
نوع مقاله: ISI
سال انتشار مقاله: 2021
ایمپکت فاکتور: 1.738 در سال 2020
شاخص H_index: 62 در سال 2021
شاخص SJR: 0.366 در سال 2020
شناسه ISSN: 0167-6423
شاخص Quartile (چارک): Q3 در سال 2020
فرمت مقاله انگلیسی: PDF
تعداد صفحات مقاله انگلیسی: 29
وضعیت ترجمه: ترجمه نشده است
قیمت مقاله انگلیسی: رایگان
آیا این مقاله بیس است: خیر
آیا این مقاله مدل مفهومی دارد: ندارد
آیا این مقاله پرسشنامه دارد: ندارد
آیا این مقاله متغیر دارد: ندارد
کد محصول: E15287
رفرنس: دارای رفرنس در داخل متن و انتهای مقاله
ترجمه فارسی فهرست مطالب

نکات برجسته


خلاصه


کلید واژه ها


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

  • اشتراک گذاری در

دیدگاه خود را بنویسید:

تاکنون دیدگاهی برای این نوشته ارسال نشده است

یک منطق پویا مبتنی بر ساعت برای تجزیه و تحلیل زمانبندی مشخصات CCSL
نوشته های مرتبط
مقالات جدید
پیوندها