Design for validation [digital avionics]

Outlines an approach for the development of ultrareliable digital avionics for civil air transports-a design-for-validation philosophy that includes rigorous application of formal methods. The basic concept of the methodology is introduced, and the role of formal methods is explored. System design begins with a detailed description of the system requirements written in a formal, mathematical language. The system design then proceeds in a hierarchical fashion from a highest-level specification of the system down to a detailed implementation level. Therefore, formal methods are applied to the total systems, not just to the individual subsystems, and all interactions between subsystems are formally described and understood. The impact of the design-for-validation philosophy on the system design process is demonstrated by two simple examples