RE: Formal methods



Date view Thread view Subject view Author view

David Crocker (dcrocker(at)eschertech.com)
Wed, 13 Feb 2002 10:24:04 -0000


Gerard Le Lann wrote: >> > If the maximum horizontal velocity that the subsystem could handle was > documented in the top-level spec of the subsystem, then any engineer who > reused that subsystem should have been aware of the limitation and had a > duty to check that the limit would not be exceeded. But I suspect that it > was not documented in the top-level spec. Right. And the point is that you do not need a formal specification to get this type of checking enforced. If you insist on having this done via some formalism, engineers in charge will simply stop listening. << Correct; but a formal development process will ensure that this sort of limitation *is* uncovered, so it can be documented and taken into account when the module is re-used. Nancy Leveson wrote: >> One point that seems to be missing here is that there is a huge difference between a specification being mathematically complete and being complete from an engineering standpoint. There is no way that the use of proofs based on set theory or formal logic will detect that the throttle is being advanced at the wrong time or that all conditions under which it should be advanced have been specified. Finding such problems requires a domain expert, and sometimes even they miss them -- particularly when the specification is far from the notation they are used to using. The formal specification "True" is complete from a mathematical standpoint, but not when used to specify the requirements for the autopilot of an aircraft. << In my view, sensible use of formal methods involves (1) starting with a formalised version of the requirements, and (2) modelling to some degree enough of the whole system so that the requirements relate to the model. In the example of the autopilot, it would be appropriate to start by modeling the aircraft-autopilot combination; then it is possible to formally represent requirements such as "the angle of bank shall never exceed 30 degrees" or "the aircraft shall not be permitted to stall when the autopilot is engaged". The formal specification of the autopilot component would be written only when this has been done. Obviously, if the autopilot specification were "True" then these requirements would fail to verify. So proofs based on formal logic *can* detect that the throttle is being advanced at the wrong time, *provided* that the formalised requirements are sufficient to (directly or indirectly) identify what is meant by the "wrong time". Dr. David Crocker Escher Technologies Ltd. 3 Archipelago Business Park Lyon Way, Frimley GU16 5ER, U.K. +44 (0)1276 686569 www.eschertech.com


Date view Thread view Subject view Author view