Formal and Fault Tolerant Design
Document type :
Direction scientifique d'une publication (ouvrage, numéro spécial de revue, proceedings): Proceedings
Title :
Formal and Fault Tolerant Design
Author(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

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

LIFL - DART/Émeraude
Conference title :
8th European Conference on Modelling Foundations and Applications (ECMFA 2012)
Publication place :
Lyngby, Denmark
Publication date :
2012-07
ISBN :
978-87-643-1014-6
HAL domain(s) :
Informatique [cs]
English abstract : [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, ...
Show more >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.Show less >
Show more >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.Show less >
Language :
Anglais
Audience :
Internationale
Source :