PUMA
Istituto di Scienza e Tecnologie dell'Informazione     
Paterṇ F., Santoro C. Requirements and formal properties on ATC. The MEFISTO Project ESPRIT Reactive LTR 24963 Project WP 1-9. Internal note CNUCE-B4-98-064, 1998.
 
 
Abstract
(English)
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.
Subject Model-checking
Formal methods
D.2.4 Software/Program Verification


Icona documento 1) Download Document PDF


Icona documento Open access Icona documento Restricted Icona documento Private

 


Per ulteriori informazioni, contattare: Librarian http://puma.isti.cnr.it

Valid HTML 4.0 Transitional