IDEAS home Printed from https://ideas.repec.org/a/eee/reensy/v132y2014icp20-35.html
   My bibliography  Save this article

Spacecraft early design validation using formal methods

Author

Listed:
  • Bozzano, Marco
  • Cimatti, Alessandro
  • Katoen, Joost-Pieter
  • Katsaros, Panagiotis
  • Mokos, Konstantinos
  • Nguyen, Viet Yen
  • Noll, Thomas
  • Postma, Bart
  • Roveri, Marco

Abstract

The size and complexity of software in spacecraft is increasing exponentially, and this trend complicates its validation within the context of the overall spacecraft system. Current validation methods are labor-intensive as they rely on manual analysis, review and inspection. For future space missions, we developed – with challenging requirements from the European space industry – a novel modeling language and toolset for a (semi-)automated validation approach. Our modeling language is a dialect of AADL and enables engineers to express the system, the software, and their reliability aspects. The COMPASS toolset utilizes state-of-the-art model checking techniques, both qualitative and probabilistic, for the analysis of requirements related to functional correctness, safety, dependability and performance. Several pilot projects have been performed by industry, with two of them having focused on the system-level of a satellite platform in development. Our efforts resulted in a significant advancement of validating spacecraft designs from several perspectives, using a single integrated system model. The associated technology readiness level increased from level 1 (basic concepts and ideas) to early level 4 (laboratory-tested).

Suggested Citation

  • Bozzano, Marco & Cimatti, Alessandro & Katoen, Joost-Pieter & Katsaros, Panagiotis & Mokos, Konstantinos & Nguyen, Viet Yen & Noll, Thomas & Postma, Bart & Roveri, Marco, 2014. "Spacecraft early design validation using formal methods," Reliability Engineering and System Safety, Elsevier, vol. 132(C), pages 20-35.
    • Handle: RePEc:eee:reensy:v:132:y:2014:i:c:p:20-35
    DOI: 10.1016/j.ress.2014.07.003
    as

    Download full text from publisher

    File URL: http://www.sciencedirect.com/science/article/pii/S0951832014001586
    Download Restriction: Full text for ScienceDirect subscribers only
    File URL: https://libkey.io/10.1016/j.ress.2014.07.003?utm_source=ideas
    LibKey link: if access is restricted and if your library uses this service, LibKey will redirect you to where you can use your library subscription to access this item
    ---><---

    As the access to this document is restricted, you may want to search for a different version of it.

    References listed on IDEAS

    as
    1. Castet, Jean-Francois & Saleh, Joseph H., 2012. "On the concept of survivability, with application to spacecraft and space-based networks," Reliability Engineering and System Safety, Elsevier, vol. 99(C), pages 123-138.
    Full references (including those not matched with items on IDEAS)

    Citations

    Citations are extracted by the CitEc Project, subscribe to its RSS feed for this item.
    as


    Cited by:

    1. Bolton, Matthew L. & Molinaro, Kylie A. & Houser, Adam M., 2019. "A formal method for assessing the impact of task-based erroneous human behavior on system safety," Reliability Engineering and System Safety, Elsevier, vol. 188(C), pages 168-180.
    2. Mobin, Mohammadsadegh & Li, Zhaojun & Cheraghi, S. Hossein & Wu, Gongyu, 2019. "An approach for design Verification and Validation planning and optimization for new product reliability improvement," Reliability Engineering and System Safety, Elsevier, vol. 190(C), pages 1-1.
    3. Hu, Yunpeng & Peng, Qibo & Ni, Qing & Wu, Xinfeng & Ye, Dongming, 2023. "Event-based safety and reliability analysis integration in model-based space mission design," Reliability Engineering and System Safety, Elsevier, vol. 229(C).
    4. Bolbot, Victor & Theotokatos, Gerasimos & Bujorianu, Luminita Manuela & Boulougouris, Evangelos & Vassalos, Dracos, 2019. "Vulnerabilities and safety assurance methods in Cyber-Physical Systems: A comprehensive review," Reliability Engineering and System Safety, Elsevier, vol. 182(C), pages 179-193.
    5. Pakonen, Antti & Buzhinsky, I & Björkman, K, 2021. "Model checking reveals design issues leading to spurious actuation of nuclear instrumentation and control systems," Reliability Engineering and System Safety, Elsevier, vol. 205(C).
    6. Lu, Yu & Peng, Zhaoguang & Miller, Alice A. & Zhao, Tingdi & Johnson, Christopher W., 2015. "How reliable is satellite navigation for aviation? Checking availability properties with probabilistic verification," Reliability Engineering and System Safety, Elsevier, vol. 144(C), pages 95-116.
    7. Li, Rui & Verhagen, Wim J.C. & Curran, Richard, 2020. "A systematic methodology for Prognostic and Health Management system architecture definition," Reliability Engineering and System Safety, Elsevier, vol. 193(C).
    8. Cheng, Ruijun & Zhou, Jin & Chen, Dewang & Song, Yongduan, 2016. "Model-based verification method for solving the parameter uncertainty in the train control system," Reliability Engineering and System Safety, Elsevier, vol. 145(C), pages 169-182.

    Most related items

    These are the items that most often cite the same works as this one and are cited by the same works as this one.
    1. Jean-Francois Castet & Joseph H Saleh, 2013. "Interdependent Multi-Layer Networks: Modeling and Survivability Analysis with Applications to Space-Based Networks," PLOS ONE, Public Library of Science, vol. 8(4), pages 1-13, April.
    2. Poulin, Craig & Kane, Michael B., 2021. "Infrastructure resilience curves: Performance measures and summary metrics," Reliability Engineering and System Safety, Elsevier, vol. 216(C).
    3. Kenneth Martínez & David Claudio, 2023. "Expanding Fundamental Boundaries between Resilience and Survivability in Systems Engineering: A Literature Review," Sustainability, MDPI, vol. 15(6), pages 1-27, March.
    4. Geng, Sunyue & Liu, Sifeng & Fang, Zhigeng, 2021. "Resilient communication model for satellite networks using clustering technique," Reliability Engineering and System Safety, Elsevier, vol. 215(C).
    5. Cheng, Ruijun & Zhou, Jin & Chen, Dewang & Song, Yongduan, 2016. "Model-based verification method for solving the parameter uncertainty in the train control system," Reliability Engineering and System Safety, Elsevier, vol. 145(C), pages 169-182.
    6. Payuna Uday & Karen Marais, 2015. "Designing Resilient Systems‐of‐Systems: A Survey of Metrics, Methods, and Challenges," Systems Engineering, John Wiley & Sons, vol. 18(5), pages 491-510, October.
    7. Chatterjee, Abheek & Layton, Astrid, 2020. "Mimicking nature for resilient resource and infrastructure network design," Reliability Engineering and System Safety, Elsevier, vol. 204(C).
    8. Lowe, Christopher J. & Macdonald, Malcolm, 2020. "Space mission resilience with inter-satellite networking," Reliability Engineering and System Safety, Elsevier, vol. 193(C).

    Corrections

    All material on this site has been provided by the respective publishers and authors. You can help correct errors and omissions. When requesting a correction, please mention this item's handle: RePEc:eee:reensy:v:132:y:2014:i:c:p:20-35. See general information about how to correct material in RePEc.

    If you have authored this item and are not yet registered with RePEc, we encourage you to do it here. This allows to link your profile to this item. It also allows you to accept potential citations to this item that we are uncertain about.

    If CitEc recognized a bibliographic reference but did not link an item in RePEc to it, you can help with this form .

    If you know of missing items citing this one, you can help us creating those links by adding the relevant references in the same way as above, for each refering item. If you are a registered author of this item, you may also want to check the "citations" tab in your RePEc Author Service profile, as there may be some citations waiting for confirmation.

    For technical questions regarding this item, or to correct its authors, title, abstract, bibliographic or download information, contact: Catherine Liu (email available below). General contact details of provider: https://www.journals.elsevier.com/reliability-engineering-and-system-safety .

    Please note that corrections may take a couple of weeks to filter through the various RePEc services.

    IDEAS is a RePEc service. RePEc uses bibliographic data supplied by the respective publishers.