• CHI+MED
• software engineering
• PVSio-web
• PVS
• PVSio
• StateCharts
• formal verification

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.