Abstract
This paper describes a tool-supported method for the formal verification of Ada programs. It presents ATOS, a tool that automatically extracts from an Ada program a SPIN model, together with a set of desirable properties. ATOS is also capable of extracting properties from a specification annotated by the user in the program, inspired by the SPARK Annotation language. The goal of ATOS is to help in the verification of sequential and concurrent Ada programs, based on model checking. © 2012 Springer-Verlag.
Cite
CITATION STYLE
Faria, J. M., Martins, J., & Pinto, J. S. (2012). An approach to model checking Ada programs. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 7308 LNCS, pp. 105–118). https://doi.org/10.1007/978-3-642-30598-6_8
Register to see more suggestions
Mendeley helps you to discover research relevant for your work.
