Formal Proof of a Polychronous Protocol for Loosely Time-Triggered Architectures
In: Formal Methods and Software Engineering ISBN: 9783540204619 ICFEM Formal Methods and Software Engineering: 5th International Conference on Formal Engineering Methods, ICFEM 2003 5th International Conference on Formal Engineering Methods (ICFEM 2003) 5th International Conference on Formal Engineering Methods (ICFEM 2003), Nov 2003, Singapore, Singapore. pp.359-374, ⟨10.1007/978-3-540-39893-6_21⟩; (2003)
Online
unknown
Zugriff:
International audience; 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 proposed (e.g. in [1]) to provide an abstract synchronous specification on top of real-time architectures (e.g. loosely time-triggered architectures or LTTA). This abstract model is designed so as to satisfy the synchronous hypotheses and meet the implementation architecture constraints. It 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 in the theorem prover Coq and proves its correctness.
Titel: |
Formal Proof of a Polychronous Protocol for Loosely Time-Triggered Architectures
|
---|---|
Autor/in / Beteiligte Person: | Talpin, Jean-Pierre ; Nowak, David ; Kerboeuf, Mickaël ; Synchronous programming for the trusted component-based engineering of embedded systems and mission-critical systems (ESPRESSO) ; Institut de Recherche en Informatique et Systèmes Aléatoires (IRISA) ; Université de Rennes (UR)-Institut National des Sciences Appliquées - Rennes (INSA Rennes) ; Institut National des Sciences Appliquées (INSA)-Institut National des Sciences Appliquées (INSA)-Institut National de Recherche en Informatique et en Automatique (Inria)-Centre National de la Recherche Scientifique (CNRS)-Université de Rennes (UR)-Institut National des Sciences Appliquées - Rennes (INSA Rennes) ; Institut National des Sciences Appliquées (INSA)-Institut National des Sciences Appliquées (INSA)-Institut National de Recherche en Informatique et en Automatique (Inria)-Centre National de la Recherche Scientifique (CNRS)-Inria Rennes – Bretagne Atlantique ; Institut National de Recherche en Informatique et en Automatique (Inria) ; Laboratoire Spécification et Vérification [Cachan] (LSV) ; École normale supérieure - Cachan (ENS Cachan)-Centre National de la Recherche Scientifique (CNRS) ; Université de Rennes 1 (UR1) ; Université de Rennes (UNIV-RENNES)-Université de Rennes (UNIV-RENNES)-Institut National des Sciences Appliquées - Rennes (INSA Rennes) ; Institut National des Sciences Appliquées (INSA)-Université de Rennes (UNIV-RENNES)-Institut National des Sciences Appliquées (INSA)-Institut National de Recherche en Informatique et en Automatique (Inria)-Centre National de la Recherche Scientifique (CNRS)-Université de Rennes 1 (UR1) ; Institut National des Sciences Appliquées (INSA)-Université de Rennes (UNIV-RENNES)-Institut National des Sciences Appliquées (INSA)-Institut National de Recherche en Informatique et en Automatique (Inria)-Centre National de la Recherche Scientifique (CNRS)-Inria Rennes – Bretagne Atlantique |
Link: | |
Quelle: | Formal Methods and Software Engineering ISBN: 9783540204619 ICFEM Formal Methods and Software Engineering: 5th International Conference on Formal Engineering Methods, ICFEM 2003 5th International Conference on Formal Engineering Methods (ICFEM 2003) 5th International Conference on Formal Engineering Methods (ICFEM 2003), Nov 2003, Singapore, Singapore. pp.359-374, ⟨10.1007/978-3-540-39893-6_21⟩; (2003) |
Veröffentlichung: | Springer Berlin Heidelberg, 2003 |
Medientyp: | unknown |
ISBN: | 978-3-540-20461-9 (print) |
DOI: | 10.1007/978-3-540-39893-6_21 |
Schlagwort: |
|
Sonstiges: |
|