Utilize este identificador para referenciar este registo: https://hdl.handle.net/1822/14931

Registo completo
Campo DCValorIdioma
dc.contributor.authorFaria, José Miguel-
dc.contributor.authorMartins, J.-
dc.contributor.authorPinto, Jorge Sousa-
dc.date.accessioned2011-12-07T14:47:05Z-
dc.date.available2011-12-07T14:47:05Z-
dc.date.issued2012-
dc.identifier.isbn9783642305979por
dc.identifier.issn0302-9743por
dc.identifier.urihttps://hdl.handle.net/1822/14931-
dc.description.abstractThis 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.por
dc.description.sponsorshipFundação para a Ciência e a Tecnologia (FCT)por
dc.language.isoengpor
dc.rightsopenAccesspor
dc.subjectFormal verificationpor
dc.subjectModel chekingpor
dc.subjectSPINpor
dc.subjectAda programspor
dc.titleAn approach to model checking Ada programspor
dc.typeconferencePaper-
dc.peerreviewedyespor
sdum.publicationstatuspublishedpor
oaire.citationStartPage105por
oaire.citationEndPage118por
oaire.citationTitleProceedings of Inforum'11por
oaire.citationVolume7308 LNCSpor
dc.identifier.doi10.1007/978-3-642-30598-6_8por
sdum.journalLecture Notes in Computer Science (including Subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)por
sdum.conferencePublicationProceedings of Inforum'11-
Aparece nas coleções:HASLab - Artigos em revistas internacionais
DI/CCTC - Artigos (papers)

Ficheiros deste registo:
Ficheiro Descrição TamanhoFormato 
INFORUM-11-a.pdfDocumento principal204,81 kBAdobe PDFVer/Abrir

Partilhe no FacebookPartilhe no TwitterPartilhe no DeliciousPartilhe no LinkedInPartilhe no DiggAdicionar ao Google BookmarksPartilhe no MySpacePartilhe no Orkut
Exporte no formato BibTex mendeley Exporte no formato Endnote Adicione ao seu ORCID