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

    61 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