Utilize este identificador para referenciar este registo:
https://hdl.handle.net/1822/14931
Título: | An approach to model checking Ada programs |
Autor(es): | Faria, José Miguel Martins, J. Pinto, Jorge Sousa |
Palavras-chave: | Formal verification Model cheking SPIN Ada programs |
Data: | 2012 |
Revista: | Lecture Notes in Computer Science (including Subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) |
Resumo(s): | 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. |
Tipo: | Artigo em ata de conferência |
URI: | https://hdl.handle.net/1822/14931 |
ISBN: | 9783642305979 |
DOI: | 10.1007/978-3-642-30598-6_8 |
ISSN: | 0302-9743 |
Arbitragem científica: | yes |
Acesso: | Acesso aberto |
Aparece nas coleções: | HASLab - Artigos em revistas internacionais DI/CCTC - Artigos (papers) |
Ficheiros deste registo:
Ficheiro | Descrição | Tamanho | Formato | |
---|---|---|---|---|
INFORUM-11-a.pdf | Documento principal | 204,81 kB | Adobe PDF | Ver/Abrir |