RE: Formal methods



Date view Thread view Subject view Author view

David Crocker (dcrocker(at)eschertech.com)
Sun, 10 Feb 2002 16:04:23 -0000


Peter, >> Until people get *much* better at composing specifications and detecting conflicts in requirements automatically, integrated testing and all-up testing will remain the main methods of detecting compositional screw-ups in system component architectures. Recall Ariane 501 and (depending on who is to be believed) Osprey. The necessity for, and efficacy of, integrated testing appears to increase with the complexity of the system. << I would argue that it is the lack of formal specifications that prevents the construction of reliable systems by composing components or modules. If components have been formally specified and then proven to behave according to the specification, it is possible to construct a formally-verified system from these components. However, if components have not been formally specified and verified, the range of inputs and states for which the component is reliable is likely to be limited to those inputs and states that were relevant in the original project for which the component was developed. If the component is transplanted to another environment, that environment may violate the implicit assumptions originally made during development and testing. As I understand it, the failure of Ariane was due to an overflow in a floating point to integer conversion. Had the software been formally verified, it would have been necessary to prove that such an overflow could not occur provided the inputs to the module satisfied the preconditions. Either the module would have been specified with preconditions that were appropriate to its original environment and were sufficient to avoid the possibility of overflow, or the design and/or coding would have been changed to avoid the overflow without having to impose the precondition. In the former case, it would have been evident that the precondition could not be met in the new environment; in the latter case, the module would have been safe to re-use anyway. Either way, the error would have been avoided. 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