An approach to model checking Ada programs

• Author(s): Faria, José Miguel ; Martins, J. ; Pinto, Jorge Sousa
• Date: 2012
• Persistent ID: http://hdl.handle.net/1822/14931
• Origin: RepositóriUM - Universidade do Minho
• Subject(s): Formal verification; Model cheking; SPIN; Ada programs
• Document Type: Article
• Language: English

Description

This paper describes a tool-supported method for the formal verification of Ada programs. It presents ATOS, a tool that automati- cally extracts a model in SPIN from an Ada Program, together with a set of properties that state the correctness of the model. ATOS is also capable of extracting properties from user-provided annotations in Ada programs, inspired by the Spark Annotation language. The goal of ATOS is to help in the verification of sequential and concurrent Ada pro- grams based on model checking. The paper introduces the details of the proposed mechanisms, as well as the results of experimental validation, through a case study.