Formal correctness, safety, dependability, and performance analysis of a satellite

M.A. Esteve, Joost P. Katoen, V.Y. Nguyen, B. Postma, Y. Yushstein

Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review

56 Citations (Scopus)

Abstract

This paper reports on the usage of a broad palette of formal modeling and analysis techniques on a regular industrial-size design of an ultra-modern satellite platform. These efforts were carried out in parallel with the conventional software development of the satellite platform. The model itself is expressed in a formalized dialect of AADL. Its formal nature enables rigorous and automated analysis, for which the recently developed COMPASS toolset was used. The whole effort revealed numerous inconsistencies in the early design documents, and the use of formal analyses provided additional insight on discrete system behavior (comprising nearly 50 million states), on hybrid system behavior involving discrete and continuous variables, and enabled the automated generation of large fault trees (66 nodes) for safety analysis that typically are constructed by hand. The model's size pushed the computational tractability of the algorithms underlying the formal analyses, and revealed bottlenecks for future theoretical research. Additionally, the effort led to newly learned practices from which subsequent formal modeling and analysis efforts shall benefit, especially when they are injected in the conventional software development lifecycle. The case demonstrates the feasibility of fully capturing a system-level design as a single comprehensive formal model and analyze it automatically using a toolset based on (probabilistic) model checkers.
Original languageUndefined
Title of host publication34th International Conference on Software Engineering, ICSE 2012
Place of PublicationUSA
PublisherIEEE Computer Society
Pages1022-1031
Number of pages10
ISBN (Print)978-1-4673-1066-6
DOIs
Publication statusPublished - Jun 2012
Event34th International Conference on Software Engineering, ICSE 2012 - Zürich, Switzerland
Duration: 2 Jun 20129 Jun 2012
Conference number: 34

Publication series

NameACM Proceedings - International Conference on Software Engineering
PublisherIEEE Computer Society
ISSN (Print)0270-5257

Conference

Conference34th International Conference on Software Engineering, ICSE 2012
Abbreviated titleICSE
CountrySwitzerland
CityZürich
Period2/06/129/06/12

Keywords

  • EWI-22518
  • METIS-293191
  • IR-82694

Cite this

Esteve, M. A., Katoen, J. P., Nguyen, V. Y., Postma, B., & Yushstein, Y. (2012). Formal correctness, safety, dependability, and performance analysis of a satellite. In 34th International Conference on Software Engineering, ICSE 2012 (pp. 1022-1031). (ACM Proceedings - International Conference on Software Engineering). USA: IEEE Computer Society. https://doi.org/10.1109/ICSE.2012.6227118
Esteve, M.A. ; Katoen, Joost P. ; Nguyen, V.Y. ; Postma, B. ; Yushstein, Y. / Formal correctness, safety, dependability, and performance analysis of a satellite. 34th International Conference on Software Engineering, ICSE 2012. USA : IEEE Computer Society, 2012. pp. 1022-1031 (ACM Proceedings - International Conference on Software Engineering).
@inproceedings{13897cd999154aa7bb20f6859c15ad93,
title = "Formal correctness, safety, dependability, and performance analysis of a satellite",
abstract = "This paper reports on the usage of a broad palette of formal modeling and analysis techniques on a regular industrial-size design of an ultra-modern satellite platform. These efforts were carried out in parallel with the conventional software development of the satellite platform. The model itself is expressed in a formalized dialect of AADL. Its formal nature enables rigorous and automated analysis, for which the recently developed COMPASS toolset was used. The whole effort revealed numerous inconsistencies in the early design documents, and the use of formal analyses provided additional insight on discrete system behavior (comprising nearly 50 million states), on hybrid system behavior involving discrete and continuous variables, and enabled the automated generation of large fault trees (66 nodes) for safety analysis that typically are constructed by hand. The model's size pushed the computational tractability of the algorithms underlying the formal analyses, and revealed bottlenecks for future theoretical research. Additionally, the effort led to newly learned practices from which subsequent formal modeling and analysis efforts shall benefit, especially when they are injected in the conventional software development lifecycle. The case demonstrates the feasibility of fully capturing a system-level design as a single comprehensive formal model and analyze it automatically using a toolset based on (probabilistic) model checkers.",
keywords = "EWI-22518, METIS-293191, IR-82694",
author = "M.A. Esteve and Katoen, {Joost P.} and V.Y. Nguyen and B. Postma and Y. Yushstein",
note = "10.1109/ICSE.2012.6227118",
year = "2012",
month = "6",
doi = "10.1109/ICSE.2012.6227118",
language = "Undefined",
isbn = "978-1-4673-1066-6",
series = "ACM Proceedings - International Conference on Software Engineering",
publisher = "IEEE Computer Society",
pages = "1022--1031",
booktitle = "34th International Conference on Software Engineering, ICSE 2012",
address = "United States",

}

Esteve, MA, Katoen, JP, Nguyen, VY, Postma, B & Yushstein, Y 2012, Formal correctness, safety, dependability, and performance analysis of a satellite. in 34th International Conference on Software Engineering, ICSE 2012. ACM Proceedings - International Conference on Software Engineering, IEEE Computer Society, USA, pp. 1022-1031, 34th International Conference on Software Engineering, ICSE 2012, Zürich, Switzerland, 2/06/12. https://doi.org/10.1109/ICSE.2012.6227118

Formal correctness, safety, dependability, and performance analysis of a satellite. / Esteve, M.A.; Katoen, Joost P.; Nguyen, V.Y.; Postma, B.; Yushstein, Y.

34th International Conference on Software Engineering, ICSE 2012. USA : IEEE Computer Society, 2012. p. 1022-1031 (ACM Proceedings - International Conference on Software Engineering).

Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review

TY - GEN

T1 - Formal correctness, safety, dependability, and performance analysis of a satellite

AU - Esteve, M.A.

AU - Katoen, Joost P.

AU - Nguyen, V.Y.

AU - Postma, B.

AU - Yushstein, Y.

N1 - 10.1109/ICSE.2012.6227118

PY - 2012/6

Y1 - 2012/6

N2 - This paper reports on the usage of a broad palette of formal modeling and analysis techniques on a regular industrial-size design of an ultra-modern satellite platform. These efforts were carried out in parallel with the conventional software development of the satellite platform. The model itself is expressed in a formalized dialect of AADL. Its formal nature enables rigorous and automated analysis, for which the recently developed COMPASS toolset was used. The whole effort revealed numerous inconsistencies in the early design documents, and the use of formal analyses provided additional insight on discrete system behavior (comprising nearly 50 million states), on hybrid system behavior involving discrete and continuous variables, and enabled the automated generation of large fault trees (66 nodes) for safety analysis that typically are constructed by hand. The model's size pushed the computational tractability of the algorithms underlying the formal analyses, and revealed bottlenecks for future theoretical research. Additionally, the effort led to newly learned practices from which subsequent formal modeling and analysis efforts shall benefit, especially when they are injected in the conventional software development lifecycle. The case demonstrates the feasibility of fully capturing a system-level design as a single comprehensive formal model and analyze it automatically using a toolset based on (probabilistic) model checkers.

AB - This paper reports on the usage of a broad palette of formal modeling and analysis techniques on a regular industrial-size design of an ultra-modern satellite platform. These efforts were carried out in parallel with the conventional software development of the satellite platform. The model itself is expressed in a formalized dialect of AADL. Its formal nature enables rigorous and automated analysis, for which the recently developed COMPASS toolset was used. The whole effort revealed numerous inconsistencies in the early design documents, and the use of formal analyses provided additional insight on discrete system behavior (comprising nearly 50 million states), on hybrid system behavior involving discrete and continuous variables, and enabled the automated generation of large fault trees (66 nodes) for safety analysis that typically are constructed by hand. The model's size pushed the computational tractability of the algorithms underlying the formal analyses, and revealed bottlenecks for future theoretical research. Additionally, the effort led to newly learned practices from which subsequent formal modeling and analysis efforts shall benefit, especially when they are injected in the conventional software development lifecycle. The case demonstrates the feasibility of fully capturing a system-level design as a single comprehensive formal model and analyze it automatically using a toolset based on (probabilistic) model checkers.

KW - EWI-22518

KW - METIS-293191

KW - IR-82694

U2 - 10.1109/ICSE.2012.6227118

DO - 10.1109/ICSE.2012.6227118

M3 - Conference contribution

SN - 978-1-4673-1066-6

T3 - ACM Proceedings - International Conference on Software Engineering

SP - 1022

EP - 1031

BT - 34th International Conference on Software Engineering, ICSE 2012

PB - IEEE Computer Society

CY - USA

ER -

Esteve MA, Katoen JP, Nguyen VY, Postma B, Yushstein Y. Formal correctness, safety, dependability, and performance analysis of a satellite. In 34th International Conference on Software Engineering, ICSE 2012. USA: IEEE Computer Society. 2012. p. 1022-1031. (ACM Proceedings - International Conference on Software Engineering). https://doi.org/10.1109/ICSE.2012.6227118