The goal of this document is to define a case study in formal verification, based on a complex real-world application developed by Ansaldo Trasporti. The application, called ACC, is a highly programmable and scalable interlocking system for the control of large railway stations. In the case study, several features of the ACC are omitted in order to limit the complexity. However, the case study still retains a close similarity to the architecture of the ACC, and raises a number of problems of interest for the problem of the formal validation of the real system
Formal Validation of an Interlocking System for Large Railway Stations: A Case Study
Cimatti, Alessandro;Giunchiglia, Fausto;Traverso, Paolo
1997-01-01
Abstract
The goal of this document is to define a case study in formal verification, based on a complex real-world application developed by Ansaldo Trasporti. The application, called ACC, is a highly programmable and scalable interlocking system for the control of large railway stations. In the case study, several features of the ACC are omitted in order to limit the complexity. However, the case study still retains a close similarity to the architecture of the ACC, and raises a number of problems of interest for the problem of the formal validation of the real systemFile in questo prodotto:
Non ci sono file associati a questo prodotto.
I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.
