A Formal Specification and Validation of a Safety Critical Railway Control System

S. Gnesi; D. Latella; G. Lenzini; A. Amendola; C. Abbaneo; P. Marmo

A Formal Specification and Validation of a Safety Critical Railway Control System

S. Gnesi, D. Latella, G. Lenzini, A. Amendola, C. Abbaneo, P. Marmo

Research output: Contribution to conference › Paper › peer-review

32 Downloads (Pure)

Abstract

This paper describes an important experiment in formal specification and validation, both performed in the context of an industrial project jointly performed by Ansaldobreda Segnalamento Ferroviario and CNR Institutes IEI and CNUCE of Pisa. Within this project we developed two formal models of a control system which is part of a wider safety-critical system for the management of medium-large railway networks. Each model describes different aspects of the system at a different level of abstraction. On these models we performed verification of both safety properties - in the hypothesis of Byzantine errors or in presence of some defined hardware faults -- and liveness properties of a dependable communication protocols. The properties has been specified by means of assertions and temporal logical formulae. As a specification language we used Promela language while the verification was performed using the model checker Spin.

Original language	English
Number of pages	25
Publication status	Published - Apr 2000
Event	5th International ERCIM Workshop on Formal Methods for Industrial Critical Systems, FMICS 2000 - Berlin, Germany Duration: 3 Apr 2000 → 4 Apr 2000 Conference number: 5 https://fmics.inria.fr/workshop-5/

Workshop

Workshop	5th International ERCIM Workshop on Formal Methods for Industrial Critical Systems, FMICS 2000
Abbreviated title	FMICS
Country/Territory	Germany
City	Berlin
Period	3/04/00 → 4/04/00
Internet address	https://fmics.inria.fr/workshop-5/

Keywords

IR-56175
EWI-987

Access to Document

gnesi00formal

Cite this

@conference{365021447bc249e490ff9c8d2e4798c3,

title = "A Formal Specification and Validation of a Safety Critical Railway Control System",

abstract = "This paper describes an important experiment in formal specification and validation, both performed in the context of an industrial project jointly performed by Ansaldobreda Segnalamento Ferroviario and CNR Institutes IEI and CNUCE of Pisa. Within this project we developed two formal models of a control system which is part of a wider safety-critical system for the management of medium-large railway networks. Each model describes different aspects of the system at a different level of abstraction. On these models we performed verification of both safety properties - in the hypothesis of Byzantine errors or in presence of some defined hardware faults -- and liveness properties of a dependable communication protocols. The properties has been specified by means of assertions and temporal logical formulae. As a specification language we used Promela language while the verification was performed using the model checker Spin.",

keywords = "IR-56175, EWI-987",

author = "S. Gnesi and D. Latella and G. Lenzini and A. Amendola and C. Abbaneo and P. Marmo",

note = "Imported from DIES; 5th International ERCIM Workshop on Formal Methods for Industrial Critical Systems, FMICS 2000, FMICS ; Conference date: 03-04-2000 Through 04-04-2000",

year = "2000",

month = apr,

language = "English",

url = "https://fmics.inria.fr/workshop-5/",

}

TY - CONF

T1 - A Formal Specification and Validation of a Safety Critical Railway Control System

AU - Gnesi, S.

AU - Latella, D.

AU - Lenzini, G.

AU - Amendola, A.

AU - Abbaneo, C.

AU - Marmo, P.

N1 - Conference code: 5

PY - 2000/4

Y1 - 2000/4

N2 - This paper describes an important experiment in formal specification and validation, both performed in the context of an industrial project jointly performed by Ansaldobreda Segnalamento Ferroviario and CNR Institutes IEI and CNUCE of Pisa. Within this project we developed two formal models of a control system which is part of a wider safety-critical system for the management of medium-large railway networks. Each model describes different aspects of the system at a different level of abstraction. On these models we performed verification of both safety properties - in the hypothesis of Byzantine errors or in presence of some defined hardware faults -- and liveness properties of a dependable communication protocols. The properties has been specified by means of assertions and temporal logical formulae. As a specification language we used Promela language while the verification was performed using the model checker Spin.

AB - This paper describes an important experiment in formal specification and validation, both performed in the context of an industrial project jointly performed by Ansaldobreda Segnalamento Ferroviario and CNR Institutes IEI and CNUCE of Pisa. Within this project we developed two formal models of a control system which is part of a wider safety-critical system for the management of medium-large railway networks. Each model describes different aspects of the system at a different level of abstraction. On these models we performed verification of both safety properties - in the hypothesis of Byzantine errors or in presence of some defined hardware faults -- and liveness properties of a dependable communication protocols. The properties has been specified by means of assertions and temporal logical formulae. As a specification language we used Promela language while the verification was performed using the model checker Spin.

KW - IR-56175

KW - EWI-987

M3 - Paper

T2 - 5th International ERCIM Workshop on Formal Methods for Industrial Critical Systems, FMICS 2000

Y2 - 3 April 2000 through 4 April 2000

ER -

A Formal Specification and Validation of a Safety Critical Railway Control System

Abstract

Workshop

Keywords

Access to Document

Fingerprint

Cite this