Istituto di Scienza e Tecnologie dell'Informazione     
Bernardeschi C., Fantechi A., Gnesi S., Mongardi G. Proving safety properties for embedded control systems. In: Dependable Computing - EDCC-2. 2nd European Dependable Computing Conference (Taormina, ottobre 1996). Proceedings, pp. 321 - 332. A. Hlawiczka, J.G. Silva, L. Simoncini (eds.). (Lecture Notes in Computer Science, vol. 1150). Springer, 1996.
It is well-known that a fundamental problem in embedded control systems is the verification of the safety requirements. Formal methods and related support tools can successfully be applied in the formal proof that a system is safe. However, the complexity of real systems is such that automated tools often fail to formally validate such systems. A typical case is when ldquostate explosionrdquo problems arise. In this paper, we show some ędbstraction techniquesrdquo to make the problem of safety requirements validation tractable by current tools. These abstraction techniques have been defined inside a verification methodology that has been tested on the specification of a railway computer based interlocking signalling control system. The conditions under which this methodology can be applied to systems in different application areas are finally discussed.
DOI: 10.1007/3-540-61772-8_46

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