Title :
Modeling of ALFA Programs Using PVS Theorem Prover
Author :
Asokan, Shimmi ; Kumar, G. Santhosh ; Lal, N. Jaya
Author_Institution :
Dept. of Comput. Sci., Cochin Univ. of Sci. & Technol., Kochi, India
Abstract :
In safety critical software failure can have a high price. Such software should be free of errors before it is put into operation. Application of formal methods in the software development life cycle helps to ensure that the software for safety critical missions are ultra reliable. PVS theorem prover, a formal method tool, can be used for the formal verification of software in ADA language for flight software application (ALFA.). This paper describes the modeling of ALFA programs for PVS theorem prover. An ALFA2PVS translator is developed which automatically converts the software in ALFA to PVS specification. By this approach the software can be verified formally with respect to underflow/overflow errors and divide by zero conditions without the actual execution of the code.
Keywords :
aerospace computing; formal specification; program interpreters; program verification; safety-critical software; software fault tolerance; specification languages; theorem proving; ADA language; ALFA program; ALFA2PVS translator; PVS theorem prover; flight software application; formal method; formal verification; overflow error; safety critical software; software development life cycle; software failure; software specification; underflow error; Application software; Communications technology; Computer languages; Formal specifications; Formal verification; Humans; Software prototyping; Software safety; Software tools; Sparks; ALFA; Formal Modeling; Formal Verification; Prototype Verification System; Type Correctness Conditions;
Conference_Titel :
Advances in Recent Technologies in Communication and Computing, 2009. ARTCom '09. International Conference on
Conference_Location :
Kottayam, Kerala
Print_ISBN :
978-1-4244-5104-3
Electronic_ISBN :
978-0-7695-3845-7
DOI :
10.1109/ARTCom.2009.134
