Please use this identifier to cite or link to this item:
Author(s): André Carvalho
Nuno Silva
Simão Melo de Sousa
Nelma Moreira
Title: A tool for automatic model extraction of Ada/SPARK programs
Issue Date: 2010
Abstract: This paper presents a brief description of the current work on a tool that analyses temporal behaviour of Ada/RavenSPARK programs. The approach takes as a basis two previous publications that introduce innovative methods in the field of verification of real-time systems. The development of a tool that automatically generates models (timed automata) from Ada/RavenSPARK source code and uses the model checker to verify timing properties is discussed.
Subject: Ciência de computadores, Ciências da computação e da informação
Computer science, Computer and information sciences
Scientific areas: Ciências exactas e naturais::Ciências da computação e da informação
Natural sciences::Computer and information sciences
Document Type: Capítulo ou Parte de Relatório
Rights: openAccess
Appears in Collections:FCUP - Capítulo ou Parte de Relatório

Files in This Item:
File Description SizeFormat 
48497.pdfArtigo130.54 kBAdobe PDFThumbnail

This item is licensed under a Creative Commons License Creative Commons