基于 TASTE 设计的空间系统形式化验证
软件工程
2021-11-22 v1
摘要
基于模型的系统工程（MBSE）是一种开发方法，旨在构建构造即正确的系统，前提是使用清晰、无歧义且完整的模型在设计过程中对其进行描述。该方法由若干工程工具支持，这些工具使开发步骤自动化，例如代码、文档、测试用例等的生成。TASTE [1] 是 ESA 支持的实用 MBSE 工具集，它封装了多种技术用于系统设计（数据建模、架构建模、行为建模/实现）、自动生成二进制应用并对其进行验证。TASTE 中一个尚未解决的问题是，针对指定属性对系统设计进行形式化验证。在本文中，我们描述了基于 IF 模型检测器 [4] 的方法，以实现对 TASTE 设计属性的形式化验证。该方法目前在 ESA 的 MoC4Space 项目中开发。
引用
@article{arxiv.2111.10132,
title = {Formal verification of space systems designed with TASTE},
author = {I Dragomir and M Bozga and Iulian Ober and D Silveira and T Jorge and E Alaña and M Perrotin},
journal= {arXiv preprint arXiv:2111.10132},
year = {2021}
}