Periodic scheduling for MARTE/CCSL: Theory and practice
Periodic scheduling for MARTE/CCSL: Theory and practice
复制标题
DOI：
10.1016/j.scico.2017.08.015
复制
发表时间：
2017-09
期刊：
影响因子：
--
通讯作者：
Min Zhang;Feng Dai;F. Mallet
中科院分区：
文献类型：
--
作者：
Min Zhang;Feng Dai;F. Mallet
用于实时和嵌入式系统建模和分析的UML概要文件（MARTE）用于设计和分析实时和嵌入式系统。时钟约束规范语言（ccsl）是MARTE的配套语言。它将逻辑时钟作为第一公民引入，作为正式指定模型预期行为的一种方式，从而允许正式验证。ccsl描述了响应式嵌入式系统的无限行为。在本文中，我们引入并重点讨论了周期调度的概念，以便对这些无限行为进行很好的有限抽象。在研究了这些调度的理论性质之后，我们给出了一种基于ccslin的可执行操作语义的实际处理方法，即使用Maude重写逻辑。我们还提出了一种算法来自动寻找具有所提出的充分条件的周期调度程序，并通过自定义仿真和有界LTL模型检查对ccslconstraints进行形式化分析。
The UML profile for Modeling and Analysis of Real-Time and Embedded systems (MARTE) is used to design and analyze real-time and embedded systems. The Clock Constraint Specification Language (ccsl) is a companion language for MARTE. It introduces logical clocks as first class citizens as a way to formally specify the expected behavior of models, thus allowing formal verification.ccsldescribes the expected infinite behaviors of reactive embedded systems. In this paper we introduce and focus on the notion of periodic schedule to allow for a nice finite abstraction of these infinite behaviors. After studying the theoretical properties of those schedules we give a practical way to deal with them based on the executable operational semantics ofccslin rewriting logic with Maude. We also propose an algorithm to find automatically periodic schedulers with the proposed sufficient condition, and to perform formal analysis ofccslconstraints by means of customized simulation and bounded LTL model checking.