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