Experience with the application of discrete formal methods to the development of engine control software

摘要

In this paper we outline an approach to the application of Formal Methods to the development of aircraft engine control software. We outline the difficulties in applying traditional formalisms to control software and propose an approach in which the discrete requirements are specified as aggregations of state-based and reactive requirements; the particular value of (formally) aggregating requirements is that assumptions are discharged in their context or else propagated outward toward the sensory environment. We briefly discuss extensions of the approach to distributed engine control and avionics systems.