摘要 1 未来的太空任务(例如火星科学实验室)需要设计一些最复杂的载人自主软件系统。根据最近的一些估计,任务关键型软件的认证成本超过了其开发成本。当前面向过程的方法尚未达到为并发软件的开发和验证提供指导方针的详细程度。时间和并发性是自主空间系统中最关键的概念。在这项工作中,我们介绍了第一个并发和以时间为中心的框架的设计和实现,用于在 JPL 任务数据系统框架 (MDS) 中验证和语义并行化实时 C++。激励我们工作的工业项目的最终目标是提供认证工件并加速测试自主飞行系统中的复杂软件交互。作为案例研究,我们展示了 MDS 目标网络的验证和语义并行化。