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
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