Formal Methods at Rockwell Collins

Rockwell Collins is a is an electronic systems manufacturer providing systems

and equipments for aircraft and helicopters. Formal methods, including theorem
proving as well as model checking techniques, have been used by Rockwell
Collins with success on several industrial applications like micro processors
or flight control software. In this presentation, we will briefly describe the
different activities of Rockwell Collins in this area,and then present a
recent analysis where model checking has been applied.

For several years, Rockwell Collins has been developing and using a
verification framework for MATLAB Simulink and SCADE Suite models that can
generate input for different proof engines. Recently, we have used this
framework to analyze aerospace domain models containing arithmetic
computations, using state-of-the-art SMT-solvers on the back-end.

In particular, we investigated the properties of a redundancy management unit
that is implemented using linear arithmetic operations as well as conditional
expressions (such as saturation) that increase the complexity of the state
space. The objective of the analysis was to verify functional and
non-functional properties, but also to parameterize certain parts of the model
based on the analysis of other parts. In particular, we were interested in
an approximation of the reachable state space of the system, which guarantees
the bounded-input bounded-output stability, and the absence of arithmetic
overflows. We also considered implementations using floating point arithmetic.

References:

Steven P. Miller, Michael W. Whalen, Darren D. Cofer: Software Model Checking
Takes Off
Communications of the ACM Vol. 53 No. 2
http://cacm.acm.org/magazines/2010/2/69362-software-model-checking-takes-off/fulltext

Michael Dierkes: Analysis of a triplex sensor voter at Rockwell Collins France
Presentation at the TAPAS 2010 workshop
http://www.di.ens.fr/tapas2010/TAPAS_Michael_Dierkes.pdf