MEFISTO WP1-9
Paternò, F., Santoro, C.
Requirements and Formal properties on ATC
In software engineering, precise notations
have been developed to specify unambiguous requirements, and ensure that all cases of appropriate
system behaviour are considered and documented. Using one such notation, it is possible develop
techniques to automatically analyse software artefacts at early stages of the software development life
cycle. In particular, one of the advantages of using formal methods in the design of human-computer
interfaces is the possibility to rigorously reason about user interface properties. Model checking
techniques provide a useful support to this end because it can be fully automated and can check properties
of real applications such as Air Traffic Control (ATC). The aim of this report is to present an introduction
to formal methods, with special attention to the techniques needed to analyse and verify requirements
with support of automatic tools.
Home
Overview
Contact list
Planning of Work
Documents
Workspace
Related Links
Statistics