DocumentCode
276913
Title
Applications of Prolog tools in the validation of aerospace software
Author
O´Neill, I.M.
Author_Institution
Program Validation Ltd., Southampton, UK
fYear
1992
fDate
33624
Firstpage
42430
Lastpage
42433
Abstract
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
Keywords
PROLOG; aerospace computing; assembly language; program verification; software tools; Motorola 68020 assembly code; Prolog-based tools; SPADE Ada Kernel; SPARK Examiner Version B; Z8002 assembly code; aerospace software; jet engine fuel control unit; software verification;
fLanguage
English
Publisher
iet
Conference_Titel
Industrial Applications of AI (Artificial Intelligence), IEE Colloquium on (Digest No.014)
Conference_Location
London
Type
conf
Filename
167699
Link To Document