CINECA IRIS Institutional Research Information System
IRIS è la soluzione IT che facilita la raccolta e la gestione dei dati relativi alle attività e ai prodotti della ricerca. Fornisce a ricercatori, amministratori e valutatori gli strumenti per monitorare i risultati della ricerca, aumentarne la visibilità e allocare in modo efficace le risorse disponibili.
EnglishIt 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 “state explosion” problems arise. In this paper, we show some «dbstraction techniques” 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.
| Titolo: | Proving safety properties for embedded control systems | |
| Autori interni: | ||
| Anno del prodotto: | 1996 | |
| Rivista: | ||
| Abstract: | 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 “state explosion” problems arise. In this paper, we show some «dbstraction techniques” 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. | |
| Handle: | http://hdl.handle.net/11568/46635 | |
| ISBN: | 9783540617723 | |
| Appare nelle tipologie: | 4.1 Contributo in Atti di convegno |
File in questo prodotto:
Copyright © 2021