Formal patterns for multirate distributed real-time systems

被引:14
|
作者
Bae, Kyungmin [1 ]
Meseguer, Jose [1 ]
Olveczky, Peter Csaba [2 ]
机构
[1] Univ Illinois, Champaign, IL 61820 USA
[2] Univ Oslo, N-0316 Oslo, Norway
基金
美国国家科学基金会;
关键词
Distributed real-time systems; Multirate systems; Synchronizers; Model checking; Rewriting logic;
D O I
10.1016/j.scico.2013.09.010
中图分类号
TP31 [计算机软件];
学科分类号
081202 ; 0835 ;
摘要
Distributed real-time systems (DRTSs), such as avionics and automotive systems, are very hard to design and verify. Besides the difficulties of asynchrony, clock skews, and network delays, an additional source of complexity comes from the multirate nature of many such systems, which must implement several levels of hierarchical control at different rates. In previous work we showed how the design and implementation of a single-rate DRTS which should behave in a virtually synchronous way can be drastically simplified by the PALS model transformation that generates the DRTS from a much simpler synchronous model. In this work we present several simple model transformations and a multirate extension of the PALS pattern which can be combined to reduce the design and verification of a virtually synchronous multirate DRTS to the much simpler task of specifying and verifying a single synchronous system. We illustrate the ideas with a multirate hierarchical control system where a central controller orchestrates control systems in the ailerons and tail of an airplane to perform turning maneuvers. (C) 2013 Elsevier B.V. All rights reserved.
引用
收藏
页码:3 / 44
页数:42
相关论文
共 50 条
  • [31] Signal: A formal design environment for real-time systems
    LeGuernic, P
    TAPSOFT '95: THEORY AND PRACTICE OF SOFTWARE DEVELOPMENT, 1995, 915 : 789 - 790
  • [32] Formal verification of real-time systems with preemptive scheduling
    Didier Lime
    Olivier (H. ) Roux
    Real-Time Systems, 2009, 41 : 118 - 151
  • [33] A practical approach to formal design of real-time systems
    Baresi, L
    Braberman, V
    Felder, M
    Pezze, M
    Piezianek, F
    INFORMATION INTELLIGENCE AND SYSTEMS, VOLS 1-4, 1996, : 1014 - 1019
  • [34] Formal verification of real-time systems with data processing
    Tóth, Tamás (totht@mit.bme.hu), 1600, (61):
  • [35] Formal modeling and verification of real-time concurrent systems
    Yan, Fei
    Tang, Tao
    2007 IEEE INTERNATIONAL CONFERENCE ON VEHICULAR ELECTRONICS AND SAFETY, PROCEEDINGS, 2007, : 219 - 224
  • [36] Formal verification of real-time systems with preemptive scheduling
    Lime, Didier
    Roux, Olivier H.
    REAL-TIME SYSTEMS, 2009, 41 (02) : 118 - 151
  • [37] ANIMATION PROTOTYPING OF FORMAL SPECIFICATIONS OF REAL-TIME SYSTEMS
    HUGHES, TS
    COOLING, JE
    MICROPROCESSING AND MICROPROGRAMMING, 1990, 30 (1-5): : 381 - 388
  • [38] Fine real-time processing in distributed systems
    Yakoh, T
    Sato, H
    Aoyama, T
    2000 IEEE INTERNATIONAL WORKSHOP ON FACTORY COMMUNICATION SYSTEMS, PROCEEDINGS, 2000, : 135 - 142
  • [39] Real-time coordination in distributed multimedia systems
    Limniotes, TA
    Papadopoulos, GA
    PARALLEL AND DISTRIBUTED PROCESSING, PROCEEDINGS, 2000, 1800 : 685 - 691
  • [40] Load profiling in distributed real-time systems
    Bestavros, A
    INFORMATION SCIENCES, 1997, 101 (1-2) : 1 - 27