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 presents an introduction to formal methods, with special attention to the techniques needed to analyse and verify requirements with support of automatic tools.

Sommario non disponibile.