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

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.