Sistema ETD

banca dati delle tesi e dissertazioni accademiche elettroniche

 

Tesi etd-04152014-095935


Tipo di tesi
Tesi di laurea magistrale
Autore
D'URSO, ENRICO
Indirizzo email
e.durso@live.com
URN
etd-04152014-095935
Titolo
Emulink: a graphical modelling environment for PVS
Struttura
INGEGNERIA DELL'INFORMAZIONE
Corso di studi
INGEGNERIA INFORMATICA
Commissione
relatore Prof. Bernardeschi, Cinzia
relatore Ing. Domenici, Andrea
Parole chiave
  • CHI+MED
  • software engineering
  • PVSio-web
  • PVS
  • PVSio
  • StateCharts
  • formal verification
Data inizio appello
08/05/2014;
Disponibilità
completa
Riassunto analitico
Software testing is one of the most important phases in software development
process. It can be used to show the presence of bugs, but never to show their
absence. A complementary approach to make software safer is to use formal
verification techniques. They guarantee correctness of an implementation
with respect to given specifications and they can greatly increase our under-
standing of a system by revealing inconsistencies, ambiguities, and incom-
pleteness that might otherwise go undetected. Experience has demonstrated
that software engineers without significant mathematical ability can hardly
use verification tools and techniques. In this thesis we present Emulink, a
tool that can help software engineers to create formal specifications in PVS
(Prototype Verification System) starting from a stateCharts based diagram.
Emulink has a cloud-based architecture, and a simple Internet browser can
be used to run its front end. We show an application of Emulink to model
and analyse software from a commercial medical device. The tool and the
presented example were developed in collaboration with researchers working
within the CHI+MED research project (http://www.chi-med.ac.uk), which
aims to improve the safety of medical devices.
File