Reference : A Formal Specification and Validation of a Control System in Presence of Byzantine Errors
Scientific congresses, symposiums and conference proceedings : Paper published in a book
Engineering, computing & technology : Computer science
Security, Reliability and Trust
http://hdl.handle.net/10993/46826
A Formal Specification and Validation of a Control System in Presence of Byzantine Errors
English
Gnesi, Stefania [> >]
Latella, Diego [> >]
Lenzini, Gabriele mailto [University of Luxembourg > Interdisciplinary Centre for Security, Reliability and Trust (SNT) >]
Amendola, Arturo [> >]
Abbaneo, Carlo [> >]
Marmo, Pietro [> >]
2000
Proc.~of the 6th Int. Conference Tool and Algorithms for the Construction and Analysis of Systems (TACAS 2000), in ETAPS 2000 -- March 25 - April 2, 2000, Berlin, Germany
Springer
Lecture Notes In Computer Science
535-549
Yes
International
3-540-67282-6
6th Int. Conference Tool and Algorithms for the Construction and Analysis of Systems (TACAS 2000)
from 25-03-2000 to 2-04-2000
Berlin
Germany
[en] This paper describes an experience in formal specification and fault tolerant behavior validation of a railway critical system. The work, performed in the context of a real industrial project, had the following main targets: (a) to validate specific safety properties in the presence of byzantine system components or of some hardware temporary faults; (b) to design a formal model of a critical railway system at a right level of abstraction so that could be possible to verify certain safety properties and at the same time to use the model to simulate the system. For the model specification we used the Promela language, while the verification was performed using the SPIN model checker. Safety properties were specifi%% Part Glue ed by means of both assertions and temporal logic formulae. To make the problem of validation tractable in the SPIN environment, we used ad hoc abstraction techniques. http://matrix.iei.pi.cnr.it/~lenzini/papers/tacas00.ps.gz 2018-09-18 22:51:18 +0000 2019-06-15 18:30:22 +0200
Researchers ; Professionals
http://hdl.handle.net/10993/46826

There is no file associated with this reference.

Bookmark and Share SFX Query

All documents in ORBilu are protected by a user license.