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 条
  • [1] A Formal Architecture Pattern for Real-Time Distributed Systems
    Al-Nayeem, Abdullah
    Sun, Mu
    Qiu, Xiaokang
    Sha, Lui
    Miller, Steven P.
    Cofer, Darren D.
    2009 30TH IEEE REAL-TIME SYSTEMS SYMPOSIUM, PROCEEDINGS, 2009, : 161 - +
  • [2] TAM - A FORMAL FRAMEWORK FOR THE DEVELOPMENT OF DISTRIBUTED REAL-TIME SYSTEMS
    SCHOLEFIELD, DJ
    ZEDAN, HSM
    LECTURE NOTES IN COMPUTER SCIENCE, 1991, 571 : 411 - 428
  • [3] A Formal Framework for Conformance Testing of Distributed Real-Time Systems
    Krichen, Moez
    PRINCIPLES OF DISTRIBUTED SYSTEMS, 2010, 6490 : 139 - 142
  • [4] Assurance patterns for distributed real-time embedded systems
    Konrad, S
    ICSE 05: 27TH INTERNATIONAL CONFERENCE ON SOFTWARE ENGINEERING, PROCEEDINGS, 2005, : 657 - 657
  • [5] A formal approach for architectural modeling and prototyping of distributed real-time systems
    Deng, Y
    Lu, SK
    Evangelist, M
    THIRTIETH HAWAII INTERNATIONAL CONFERENCE ON SYSTEM SCIENCES, VOL 1: SOFTWARE TECHNOLOGY AND ARCHITECTURE, 1997, : 481 - 490
  • [6] FORMAL SPECIFICATION OF REAL-TIME SYSTEMS
    GORSKI, J
    COMPUTER PHYSICS COMMUNICATIONS, 1988, 50 (1-2) : 71 - 88
  • [7] Formal methods in real-time systems
    Olderog, ER
    10TH EUROMICRO WORKSHOP ON REAL-TIME SYSTEMS, PROCEEDINGS, 1998, : 254 - 263
  • [8] REAL-TIME DISTRIBUTED SYSTEMS
    BARBACCI, MR
    COMPUTER HARDWARE DESCRIPTION LANGUAGES AND THEIR APPLICATIONS, 1993, 32 : 3 - 12
  • [9] FORMAL TRAINING ANALYSIS FOR DISTRIBUTED REAL-TIME PROGRAMS
    WEDDE, HF
    KOREL, B
    HUIZINGA, DM
    REAL-TIME SYSTEMS, 1994, 7 (01) : 57 - 90
  • [10] Transformational formal development of real-time systems
    Lano, K
    Sanchez, A
    TRANSFORMATION-BASED REACTIVE SYSTEMS DEVELOPMENT, 1997, 1231 : 184 - 198