Formal and Fault Tolerant Design

Aljer, Ammar; Devienne, Philippe

Type de document :

Direction scientifique d'une publication (ouvrage, numéro spécial de revue, proceedings): Proceedings

Titre :

Formal and Fault Tolerant Design

Auteur(s) :

Aljer, Ammar [Auteur]

Laboratoire de Génie Civil et Géo-Environnement (LGCgE) - ULR 4515 [LGCgE]
Université de Lille
Devienne, Philippe [Auteur]

LIFL - DART/Émeraude

Titre de la manifestation scientifique :

8th European Conference on Modelling Foundations and Applications (ECMFA 2012)

Lieu de publication :

Lyngby, Denmark

Date de publication :

2012-07

ISBN :

978-87-643-1014-6

Discipline(s) HAL :

Informatique [cs]

Résumé en anglais : [en]

Software quality and reliability were verified for a long time at thepost-implementation level (test, fault scenario …). The design of embeddedsystems and digital circuits is more and more complex because of integrationdensity, ...
Lire la suite >Software quality and reliability were verified for a long time at thepost-implementation level (test, fault scenario …). The design of embeddedsystems and digital circuits is more and more complex because of integrationdensity, heterogeneity. Now almost ¾ of the digital circuits contain at least oneprocessor, that is, can execute software code. In other words, co-design is themost usual case and traditional verification by simulation is no more practical.Moreover, the increase in integration density comes with a decrease in the reliability of the components. So fault detection, diagnostics techniques, introspection are essential for defect tolerance, fault tolerance and self repair of safetycritical systems.The use of a formal specification language is considered as the foundation of areal validation. What we would like to emphasize is that refinement (from anabstract model to the point where the system will be implemented) could be andshould be formal too in order to ensure the traceability of requirements, to manage such development projects and so to design fault-tolerant systems correctby proven construction. Such a thorough approach can be achieved by the automation or semi-automation of the refinement process.We have studied how to ensure the traceability of these requirements in a component-based approach. Reliability, fault tolerance can be seen here as particular refinement steps. For instance, a given formal specification of a system/component may be refined by adding redundancy (data, computation, component) and be verified to be fault-tolerant w.r.t. some given fault scenarios. Aself-repair component can be defined as the refinement of its original form enhanced with error detection.We describe in this paper the PCSI project (Zero Defect Systems) based on BMethod, VHDL and PSL. The three modeling approaches can collaborate together and guarantee the codesign of embedded systems for which the requirements and the fault-tolerant aspects are taken into account for the beginning andformally verified all along the implementation process.Lire moins >

Langue :

Anglais

Audience :

Internationale

Collections :

Laboratoire Génie Civil et géo-Environnement (LGCgE) - ULR 4515

Source :

Harvested from HAL

Formal and Fault Tolerant Design BibTeX CSV Excel RIS

Formal and Fault Tolerant Design

BibTeX

CSV

Excel

RIS