Applications of Prolog tools in the validation of aerospace software

Summarises some experience of the use of Prolog-based tools in the analysis and formal verification of software for aerospace applications. The author firstly reviews tools used for the analysis of some Z8002 assembly code software for use in a jet engine fuel control unit. After this, he considers more recent tool development to support the analysis of Motorola 68020 assembly code in an aerospace context. As a final example of the use of Prolog, he considers the additional tools which are being developed for use with the SPARK Examiner Version B, to support formal verification of SPARK source code. (SPARK-the SPADE Ada Kernel-is a subset of Ada already in use in a number of aerospace projects). He then concludes with a brief review of some advantages and disadvantages of Prolog for such tools