Using Executable VDM++ Models in an Industrial Application - Self-defense System for Fighter Aircraft

When developing complex software systems, one of the most significant challenges is to make sure that the customer and developer agree on the requirements of the system. By using executable models early in the development process, a higher degree of confidence can be gained in the system design and misunderstandings or ambiguous functional requirements can be avoided. This paper presents an industrial case of a communication protocol between two parts of a selfdefense system used on-board fighter aircraft. An executable model of both systems were created using the Vienna Development Method (VDM), and exercised using many scenarios to cover different corner cases. This was done as an alternative to analysing all the scenarios by hand, which would be much more time consuming and far more error prone. The results of the scenario based tests were used to communicate with the customer and ensure that agreement of the requirements was reached