Introduction to Formal Methods using RTCA DO 178C
Jeffrey Joyce, Critical Systems Labs
This tutorial provides an introduction to the practical use of formal (mathematical) methods in the development of airborne software. Such methods can be used to find defects and other problems in software life cycle data that might be very difficult to find using conventional methods such as review and test. Participants will learn how formal methods can be selectively applied in the software life cycle to produce certification data in compliance with RTCA DO 178C/ EUROCAE ED 12C. Several illustrative examples will be presented in a manner with enough detail that participants should be able to later repeat the examples on their own using open source software tools. One of these examples will demonstrate how functional requirements expressed in English can be translated into a formal representation. Another example will demonstrate how formal analysis can be used in the context of model based development to find a defect in the model of a software function. The tutorial also provides an overview of the formal methods supplement of RTCA DO 178C/ EUROCAE ED 12C which provide specific guidance for the use of formal methods towards earning certification credit.