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

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

doi:10.1007/3-540-46419-0_36

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

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

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › Academic › peer-review

6 Citations (Scopus)

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.

Original language	English
Title of host publication	Tools and Algorithms for the Construction and Analysis of Systems
Subtitle of host publication	6th International Conference, TACAS 2000, held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2000, Berlin, Germany, March 25 – April 2, 2000, Proceedings
Editors	Susanne Graf, Michael Schwartzbach
Place of Publication	Berlin, Heidelberg
Publisher	Springer
Pages	535-549
Number of pages	15
ISBN (Electronic)	978-3-540-46419-8
ISBN (Print)	978-3-540-67282-1
DOIs	https://doi.org/10.1007/3-540-46419-0_36
Publication status	Published - Mar 2000
Event	6th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2000 - Berlin, Germany Duration: 27 Mar 2000 → 31 Mar 2000 Conference number: 6

Publication series

Name	Lecture Notes in Computer Science
Publisher	Springer
Volume	1785
ISSN (Print)	0302-9743

Conference

Conference	6th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2000
Abbreviated title	TACAS
Country/Territory	Germany
City	Berlin
Period	27/03/00 → 31/03/00

Keywords

Formal verification
Safety critical systems
Fault tolerant behavior
Linear temporal logic
Model checking

Access to Document

10.1007/3-540-46419-0_36

Cite this

Gnesi, S., Latella, D., Lenzini, G., Abbaneo, C., Amendola, A., & Marmo, P. (2000). A Formal Specification and Validation of a Control System in Presence of Byzantine Errors. In S. Graf, & M. Schwartzbach (Eds.), Tools and Algorithms for the Construction and Analysis of Systems: 6th International Conference, TACAS 2000, held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2000, Berlin, Germany, March 25 – April 2, 2000, Proceedings (pp. 535-549). (Lecture Notes in Computer Science; Vol. 1785). Springer. https://doi.org/10.1007/3-540-46419-0_36

Gnesi, S. ; Latella, D. ; Lenzini, G. et al. / A Formal Specification and Validation of a Control System in Presence of Byzantine Errors. Tools and Algorithms for the Construction and Analysis of Systems: 6th International Conference, TACAS 2000, held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2000, Berlin, Germany, March 25 – April 2, 2000, Proceedings. editor / Susanne Graf ; Michael Schwartzbach. Berlin, Heidelberg : Springer, 2000. pp. 535-549 (Lecture Notes in Computer Science).

@inproceedings{6d2c828666ff4ad790ec7e4dd1aeece6,

title = "A Formal Specification and Validation of a Control System in Presence of Byzantine Errors",

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.",

keywords = "Formal verification, Safety critical systems, Fault tolerant behavior, Linear temporal logic, Model checking",

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

year = "2000",

month = mar,

doi = "10.1007/3-540-46419-0_36",

language = "English",

isbn = "978-3-540-67282-1",

series = "Lecture Notes in Computer Science",

publisher = "Springer",

pages = "535--549",

editor = "Susanne Graf and Michael Schwartzbach",

booktitle = "Tools and Algorithms for the Construction and Analysis of Systems",

note = "6th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2000, TACAS ; Conference date: 27-03-2000 Through 31-03-2000",

}

Gnesi, S, Latella, D, Lenzini, G, Abbaneo, C, Amendola, A & Marmo, P 2000, A Formal Specification and Validation of a Control System in Presence of Byzantine Errors. in S Graf & M Schwartzbach (eds), Tools and Algorithms for the Construction and Analysis of Systems: 6th International Conference, TACAS 2000, held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2000, Berlin, Germany, March 25 – April 2, 2000, Proceedings. Lecture Notes in Computer Science, vol. 1785, Springer, Berlin, Heidelberg, pp. 535-549, 6th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2000, Berlin, Germany, 27/03/00. https://doi.org/10.1007/3-540-46419-0_36

A Formal Specification and Validation of a Control System in Presence of Byzantine Errors. / Gnesi, S.; Latella, D.; Lenzini, G. et al.
Tools and Algorithms for the Construction and Analysis of Systems: 6th International Conference, TACAS 2000, held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2000, Berlin, Germany, March 25 – April 2, 2000, Proceedings. ed. / Susanne Graf; Michael Schwartzbach. Berlin, Heidelberg: Springer, 2000. p. 535-549 (Lecture Notes in Computer Science; Vol. 1785).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › Academic › peer-review

TY - GEN

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

AU - Gnesi, S.

AU - Latella, D.

AU - Lenzini, G.

AU - Abbaneo, C.

AU - Amendola, A.

AU - Marmo, P.

N1 - Conference code: 6

PY - 2000/3

Y1 - 2000/3

N2 - 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.

AB - 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.

KW - Formal verification

KW - Safety critical systems

KW - Fault tolerant behavior

KW - Linear temporal logic

KW - Model checking

U2 - 10.1007/3-540-46419-0_36

DO - 10.1007/3-540-46419-0_36

M3 - Conference contribution

SN - 978-3-540-67282-1

T3 - Lecture Notes in Computer Science

SP - 535

EP - 549

BT - Tools and Algorithms for the Construction and Analysis of Systems

A2 - Graf, Susanne

A2 - Schwartzbach, Michael

PB - Springer

CY - Berlin, Heidelberg

T2 - 6th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2000

Y2 - 27 March 2000 through 31 March 2000

ER -

Gnesi S, Latella D, Lenzini G, Abbaneo C, Amendola A, Marmo P. A Formal Specification and Validation of a Control System in Presence of Byzantine Errors. In Graf S, Schwartzbach M, editors, Tools and Algorithms for the Construction and Analysis of Systems: 6th International Conference, TACAS 2000, held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2000, Berlin, Germany, March 25 – April 2, 2000, Proceedings. Berlin, Heidelberg: Springer. 2000. p. 535-549. (Lecture Notes in Computer Science). doi: 10.1007/3-540-46419-0_36

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

Abstract

Publication series

Conference

Keywords

Access to Document

Fingerprint

Cite this