| Summary: | A previous project, FAROAS, established a formal requirements specification for the control of aircraft flying in the eastern half of the North Atlantic. The requirements, written in Many Sorted First Order Logic, are held in a tools environment supporting validation in 5 key ways: full grammatical checking, inspection by domain experts, formal reasoning about their properties, automatic generation of a prototype for use with a test harness for batch testing, and a graphical interface for animation. Each of these five validation strategies uncovered errors in the initial encoding of the requirements, and their use improved the accuracy of the model. Unfortunately our experience led us to believe that these diverse forms of validation were still insufficient as far as uncovering bugs and fixing bugs was concerned; for example, tests may succeed for the wrong reasons, and where tests fail (i.e the expert decision is at variance with the prototype 's decision) it is still very difficult t.
|
|---|