Formal Specification of a Flight Guidance System
Fung Francis, Jamsek Damir · 1998
In this report, we investigate the use of formal methods on the semi-formal specification of a Flight Guidance System described in Steven P. Miller and Karl F. Hoech''s Specifying the Mode Logic of a Flight Guidance System in CoRE. The CoRE method can be used with the formal semantics of the SCR discrete-time formal model. However, Miller and Hoech''s specification does not satisfy the restrictions of this formal model; for instance, they use concurrent mode machines that drive each other. Furthermore, Miller and Hoech add several notions for CoRE in their specification, without formal definitions. We use the Z notation to give a formal semantics for the Flight Guidance System, by adapting the SCR formal model''s definitions of event and transitions, which mesh well with Z conventions. In particular, we do not define any micro-time semantics. We give formal definitions for Miller and Hoech''s extensions to CoRE, except for the continuous transition to FLC, which seems to be best expressed using micro-time semantics. We perform experiments of formal verification on the specification using Z/EVES. In restricted versions of the specification, we are able to do table consistency checking and to verify properties such as determinism and system invariants.