Emerging verification methods for complex hardware in avionics

This paper discusses the additional design assurance strategies stated in RTCA/DO-254, Appendix B - "Design assurance considerations for level A and level B functions." In particular, we address the use of formal specification languages such as the property specification language (PSL) in combination with dynamic (simulation) and static (formal) verification methods for programmed logic devices. Using these methods, we suggest a design assurance strategy for complex programmable airborne electronics compliant with the guidelines of RTCA/DO-254. The strategy is a semi-formal solution, a hybrid of static and dynamic assertion based verification.