Scholarlink

<p>Ensuring the correct and safe behavior of a spacecraft is a main objective in space-system design. Since spacecraft consist of highly complex and tightly integrated components developed by large teams of engineers from various different disciplines, this is a challenging task. Increasingly, formal verification methods such as model checking are applied to establish the correctness of safety-critical parts or subsystems. Generally, the often limited scalability of model checking due to the state-space explosion problem hinders the wide-spread adoption of this technique. In this paper, we systematically examine the scalability of model checking for verifying behavioral models that arise within early space-system design phases. For this, we created a representative model for the mode management of a satellite that can be scaled in terms of its size and the complexity of interactions between system components. The model can be transformed into the input languages of various model-checking tools, which enables a comparative study of various model-checking algorithms and also facilitates analyzing the impact of different communication schemes on the scalability. The evaluation shows promising results regarding the applicability of model checking within the spacecraft design process.</p>

错误：搜索内容不能为空，请输入英文关键词
错误：关键词超出字数限制，请精简
高级检索

Model checking of spacecraft operational designs: a scalability analysis

  • 期刊论文

  • 出版模式：

    开放获取

  • 发表日期：

    2025年4月15日

查看全文
  • Philipp Chrszon,
  • Paulina Maurer,
  • George Saleip,
  • Sascha Müller,
  • Philipp M. Fischer,
  • Andreas Gerndt,
  • Michael Felderer

摘要

Ensuring the correct and safe behavior of a spacecraft is a main objective in space-system design. Since spacecraft consist of highly complex and tightly integrated components developed by large teams of engineers from various different disciplines, this is a challenging task. Increasingly, formal verification methods such as model checking are applied to establish the correctness of safety-critical parts or subsystems. Generally, the often limited scalability of model checking due to the state-space explosion problem hinders the wide-spread adoption of this technique. In this paper, we systematically examine the scalability of model checking for verifying behavioral models that arise within early space-system design phases. For this, we created a representative model for the mode management of a satellite that can be scaled in terms of its size and the complexity of interactions between system components. The model can be transformed into the input languages of various model-checking tools, which enables a comparative study of various model-checking algorithms and also facilitates analyzing the impact of different communication schemes on the scalability. The evaluation shows promising results regarding the applicability of model checking within the spacecraft design process.