"Increasing Confidence of Complex Hardware in Safety-Critical Avionics Using Formal Methods"

Kristoffer Karlsson and Håkan Forsberg
Saab Avitronics


Due to certification demands design of complex safety-critical programmable logics in avionics necessitates additional design assurance strategies. One such advanced design assurance strategy proposed by the certification authorities is the use of formal methods. Formal methods (FM) increase the ability to verify complex programmable logic designs incorporating large input/output-spaces and numerous state-holding elements.

Although FM remain one of the most contentious areas of verification practice, we believe that FM can be used to support the intricate work of developing and verifying safety-critical hardware designs in avionics.

This article covers the use of static and dynamic assertion-based verification of complex programmable logics in safety-critical avionic designs. We pursue this by our Overlapped Layered Modular Methodology (OLMM). We briefly introduce OLMM and thereafter discuss experiences of developing complex designs intended for the highest design assurance levels (levels A and B) using this methodology. These experiences have been gained from a case study within the framework of the SMS-254 (Strategy selection and Methodology for Safety-critical applications, compliant with RTCA DO-254) project carried out at Saab for the Swedish Ministry of Defense.


2006 MAPLD International Conference Home Page