PUMA
Istituto di Scienza e Tecnologie dell'Informazione     
Bernardeschi C., Fantechi A., Gnesi S. Formal validation of the GUARDS inter-consistency mechanism. In: Computer Safety, Reliability and Security. 18th International Conference, SAFECOMP'99. Proceedings (Toulouse (France), September 1999). Proceedings, vol. 1698 pp. 420 - 430. M. Felici, K. Kanoun and A. Pasquini (eds.). (Lecture Notes in Computer Science). Springer, 1999.
 
 
Abstract
(English)
In this paper we report the experience carried out to specify and validate the Inter-consistency mechanism developed within the Eu- ropean project GUARDS as a component of an architecture for embedded safety-critical systems. The validation approach is based on model checking technique and exploits the veri cation methodology supported by the JACK environment. The properties that guarantee the desired behaviour of the mechanism are speci ed as temporal logic formulae; the JACK model checker is then used to verify that the behaviour of the mechanism satis es such properties also in presence of faults.
Subject 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