Sciweavers

Share
ICFEM
2003
Springer

Formal Proof of a Polychronous Protocol for Loosely Time-Triggered Architectures

8 years 9 months ago
Formal Proof of a Polychronous Protocol for Loosely Time-Triggered Architectures
The verification of safety critical systems has become an area of increasing importance in computer science. The notion of reactive system has emerged to concentrate on problems related to the control of interaction and response-time in mission-critical systems. Synchronous languages have proved to be well-adapted to the verification of reactive systems. It is nonetheless commonly argued that real-life systems often do not satisfy the strong hypotheses assumed by the synchronous approach: they are not synchronous. Protocols have however been pro.g. in [1]) to provide an abstract synchronous specification on top of real-time architectures (e.g. loosely time-triggered architectures or his abstract model is designed so as to satisfy the synchronous hypotheses and meet the implementation architecture constraints. It is makes it possible to design, specify and verify reactive systems in the context of the synchronous approach. In this aim, the present article formalizes the LTTA protocol...
Mickaël Kerboeuf, David Nowak, Jean-Pierre Ta
Added 06 Jul 2010
Updated 06 Jul 2010
Type Conference
Year 2003
Where ICFEM
Authors Mickaël Kerboeuf, David Nowak, Jean-Pierre Talpin
Comments (0)
books