Dyuthi @ CUSAT >
e-SCHOLARSHIP >
Computer Science >
Faculty >
Dr.Santhosh Kumar G >
Please use this identifier to cite or link to this item:
http://purl.org/purl/4179
|
Title: | Modeling of ALFA Programs Using PVS Theorem Prover |
Authors: | Santhosh Kumar, G Shimmi, Asokan Jaya Lal, N |
Keywords: | ALFA Formal Modeling Formal Verification Prototype Verification System; Type Correctness Conditions |
Issue Date: | 2009 |
Publisher: | IEEE |
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 |
Description: | 2009 International Conference on Advances in Recent Technologies in Communication and Computing |
URI: | http://dyuthi.cusat.ac.in/purl/4179 |
Appears in Collections: | Dr.Santhosh Kumar G
|
Items in DSpace are protected by copyright, with all rights reserved, unless otherwise indicated.
|