• DocumentCode
    1288293
  • Title

    The Signal Synchronous Multiclock Approach to the Design of Distributed Embedded Systems

  • Author

    Gamatié, Abdoulaye ; Gautier, Thierry

  • Author_Institution
    LIFL, INRIA Lille-Nord Eur., Villeneuve-d´´Ascq, France
  • Volume
    21
  • Issue
    5
  • fYear
    2010
  • fDate
    5/1/2010 12:00:00 AM
  • Firstpage
    641
  • Lastpage
    657
  • Abstract
    This paper presents the design of distributed embedded systems using the synchronous multiclock model of the SIGNAL language. It proposes a methodology that ensures a correct-by-construction functional implementation of these systems from high-level models. It shows the capability of the synchronous approach to apply formal techniques and tools that guarantee the reliability of the designed systems. Such a capability is necessary and highly worthy when dealing with safety-critical systems. The proposed methodology is demonstrated through a case study consisting of a simple avionic application, which aims to pragmatically help the reader to understand the manipulated formal concepts, and to apply them easily in order to solve system correctness issues encountered in practice. The application functionality is first modeled as well as its distribution on a generic hardware architecture. This relies on the endochrony and endo-isochrony properties of SIGNAL specifications, defined previously. The considered architectures include asynchronous communication mechanisms, which are also modeled in SIGNAL and proved to achieve message exchanges correctly. Furthermore, the synchronizability of the different parts in the resulting system is addressed after its deployment on a specific execution platform with multirate clocks. After all these steps, a distributed code can be automatically generated.
  • Keywords
    avionics; embedded systems; formal specification; programming languages; reliability; safety-critical software; SIGNAL language; avionic application; distributed embedded systems design; endo-isochrony properties; endochrony properties; formal techniques; generic hardware architecture; safety-critical systems; synchronous multiclock model; Distributed embedded systems; Signal language; asynchronous mechanisms; correct-by-construction design methodology; formal validation; multiclock; safety-critical domains; synchronous model;
  • fLanguage
    English
  • Journal_Title
    Parallel and Distributed Systems, IEEE Transactions on
  • Publisher
    ieee
  • ISSN
    1045-9219
  • Type

    jour

  • DOI
    10.1109/TPDS.2009.125
  • Filename
    5196666