Abstract
This tutorial provides an introduction to the practical use of formal (mathematical) methods in the development of airborne software. Formal methods can be used to find defects and other problems in software life cycle data that might be very difficult to find using conventional approaches, 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 with enough detail that participants should be able to later repeat the examples on their own using open source software tools. Some of these examples will demonstrate how functional requirements expressed in Natural Language can be translated into formal representations suitable for analysis. Other examples will demonstrate how formal analysis can be used in the context of model-based development to find defects in models of varying complexity. Participants will learn about the currently available tools and will see hands-on how to use the QVtrace formal design verification tool and its QCT formal language in some of these examples. The tutorial will also provide an overview of the formal methods supplement RTCA DO-333, which provides specific guidance for the use of formal methods towards earning RTCA DO 178C/ EUROCAE ED 12C certification credit.
Instructor Biographies
Dr. Jeffrey Joyce is a co-founder and Managing Director of an engineering consultancy, Critical Systems Labs, that provides clients with expertise in the development of critical systems. As a member of RTCA SC 205, he contributed to the development of RTCA DO-178C and, in particular, the formal methods supplements RTCA DO-333. Jeff has nearly 30 years of experience in the development of software-intensive critical systems across a variety of technical domains including aerospace, automotive, rail signaling, energy, medical devices and defence. He earned a PhD from the University of Cambridge in 1990 investigating the applications of formal methods to critical systems.
Dr. Jordan Kyriakidis has 15 years experience leading diverse teams of driven and high-performance individuals; first as a scientist with numerous international publications, and now as Cofounder and CEO of QRA Corp, an emerging Design Verification company. QRA’s solutions help companies and governments identify and mitigate risk in complex projects from the RFP-stage onwards, especially projects involving the introduction of new technologies in regulated industries. Jordan has lived and worked in Europe, the US, and in Canada. He holds a PhD, summa cum laude, in Quantum Theory from the University of Basel, Switzerland.
