An approach to model checking Ada programs

• Autor(es): Faria, José Miguel ; Martins, J. ; Pinto, Jorge Sousa
• Data: 2012
• Identificador Persistente: http://hdl.handle.net/1822/14931
• Origem: RepositóriUM - Universidade do Minho
• Assunto(s): Formal verification; Model cheking; SPIN; Ada programs
• Tipo de Documento: Artigo
• Idioma: Inglês

Descrição

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.