A Formal Specification and Validation of a Control System in Presence of Byzantine Errors

Gnesi, S. and Latella, D. and Lenzini, G. and Amendola, A. and Abbaneo, C. and Marmo, P. (2000) A Formal Specification and Validation of a Control System in Presence of Byzantine Errors. In: 6th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2000, 27-31 March 2000, Berlin, Germany.

PDF
Restricted to UT campus only: Request a copy
176Kb

Abstract:	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 specified 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.
Item Type:	Conference or Workshop Item
Copyright:	© 2000 Springer
Faculty:	Electrical Engineering, Mathematics and Computer Science (EEMCS)
Link to this item:	http://purl.utwente.nl/publications/67122
Official URL:	http://dx.doi.org/10.1007/3-540-46419-0_36
Export this item as:	BibTeX EndNote HTML Citation Reference Manager

Show download statistics for this publication

Repository Staff Only: item control page