Modeling of ALFA Programs Using PVS Theorem Prover

Dyuthi/Manakin Repository

Modeling of ALFA Programs Using PVS Theorem Prover

Show simple item record Santhosh Kumar, G Shimmi, Asokan Jaya Lal, N 2014-07-21T04:10:44Z 2014-07-21T04:10:44Z 2009
dc.description 2009 International Conference on Advances in Recent Technologies in Communication and Computing en_US
dc.description.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. en_US
dc.description.sponsorship Cochin University of Science and Technology en_US
dc.language.iso en en_US
dc.publisher IEEE en_US
dc.subject ALFA en_US
dc.subject Formal Modeling en_US
dc.subject Formal Verification en_US
dc.subject Prototype Verification System en_US
dc.subject Type Correctness Conditions en_US
dc.title Modeling of ALFA Programs Using PVS Theorem Prover en_US
dc.type Article en_US

Files in this item

Files Size Format View Description
Modeling of ALF ... ing PVS Theorem Prover.pdf 386.2Kb PDF View/Open pdf

This item appears in the following Collection(s)

Show simple item record

Search Dyuthi

Advanced Search


My Account