高级检索
    陈博, 李曦, 周学海. 安全关键的信息物理系统中时序行为的组合与精化[J]. 计算机研究与发展, 2023, 60(8): 1895-1911. DOI: 10.7544/issn1000-1239.202220041
    引用本文: 陈博, 李曦, 周学海. 安全关键的信息物理系统中时序行为的组合与精化[J]. 计算机研究与发展, 2023, 60(8): 1895-1911. DOI: 10.7544/issn1000-1239.202220041
    Chen Bo, Li Xi, Zhou Xuehai. Composition and Refinement of Timing Behavior in Safety-Critical Cyber Physical Systems[J]. Journal of Computer Research and Development, 2023, 60(8): 1895-1911. DOI: 10.7544/issn1000-1239.202220041
    Citation: Chen Bo, Li Xi, Zhou Xuehai. Composition and Refinement of Timing Behavior in Safety-Critical Cyber Physical Systems[J]. Journal of Computer Research and Development, 2023, 60(8): 1895-1911. DOI: 10.7544/issn1000-1239.202220041

    安全关键的信息物理系统中时序行为的组合与精化

    Composition and Refinement of Timing Behavior in Safety-Critical Cyber Physical Systems

    • 摘要: 信息物理系统(cyber physical systems, CPS)通常被应用于安全关键的场景中,需要进行实时监控,并计算反馈信息,实现对外部环境的自动控制与管理. 基于模型驱动的开发方法是针对实时的、异构的CPS进行开发的,而模型的可组合性是其中的核心关键点. 针对时序行为的可组合问题,首先通过时序约束语言(clock constraint specification language, CCSL)建立系统的时序行为需求模型,在此基础上通过迁移系统描述CCSL的时序行为语义,并给出其组合操作方法及可组合性的形式化定义. 进一步地,对时序行为进行精化操作,给出从时序行为需求模型到任务执行模型的转换方法. 同时,基于L*方法对模型行为进行学习,实现组合验证以缓解状态爆炸问题,并验证精化后模型的可组合性. 最后通过仿真实验及主从智能小车实例对精化与验证方法进行评估. 相关数据显示,精化与组合验证方法在处理时间和内存使用上具有一定的性能优势.

       

      Abstract: Cyber physical systems (CPS) are usually used in safety critical scenarios, which require real-time monitoring, compute the feedback data, and realize automatic control and management of the external environment. Model driven development method is the main way to develop real-time and heterogeneous CPS, and the composability of the model is the key point. In this paper, the timing behavior specification model of the system is established by the clock constraint specification language (CCSL), and on this basis, the timing behavior semantics of CCSL is described by the transition systems, and its composition operation method and the formal definition of composability is given. Further, the timing behavior is refined, and the transformation method from the timing behavior model of specification to the task execution model is given, The timing constraint behavior at the specification level is transformed into the timing constraint behavior at the task level. At the same time, the model behavior is learned based on the L* method to realize compositional verification to alleviate the state explosion problem, and the composability of the refined model is verified. Finally, the refinement and verification methods are evaluated by simulation experiments and the master-slave intelligent vehicle example. The relevant data shows that, the refined method and compositional verification methods have some performance advantages in processing time and memory consumption.

       

    /

    返回文章
    返回