Deadlock Analysis for a Fault-Tolerant System
Deadlock Analysis for a Fault-Tolerant System
复制标题
容错系统的死锁分析
DOI：
10.1007/bfb0000463
复制
发表时间：
1997
期刊：
影响因子：
--
通讯作者：
Hui Shi
中科院分区：
文献类型：
--
作者：
B. Buth;M. Kouvaras;J. Peleska;Hui Shi
本文提出了一种用形式化方法验证大规模嵌入式系统通信特性的方法。举例说明了戴姆勒-奔驰航空航天公司为国际空间站国际空间站设计和实施的容错系统所执行的工业验证项目所取得的实例和结果。该方法基于CSP规范和模型检测工具FDR。通过应用抽象技术将规范限制在基本通信行为、根据进程结构的模块化以及为应用程序开发的一组通用理论，将任务拆分为可管理的子任务。
This article presents an approach for the verification of communication properties in large-scale real-world embedded systems by means of formal methods. It is illustrated by examples and results obtained during an industrial verification project performed for a fault-tolerant system designed and implemented by Daimler-Benz Aerospace for the International Space Station ISS. The approach is based on CSP specifications and the model-checking tool FDR. The task is split into manageable subtasks by applying an abstraction technique for restricting the specifications to the essential communication behaviour, modularization according to the process structure, and a set of generic theories developed for the application.