Specification and Validation of the SACI-1 On-Board Computer Using Timed-CSP-Z and Petri Nets
Specification and Validation of the SACI-1 On-Board Computer Using Timed-CSP-Z and Petri Nets
复制标题
使用 Timed-CSP-Z 和 Petri 网的 SACI-1 机载计算机的规范和验证
DOI：
10.1007/3-540-44919-1_13
复制
发表时间：
2003
影响因子：
1.5
通讯作者：
S. Cavalcante
中科院分区：
文献类型：
--
作者：
Adnan Sherif;A. Sampaio;S. Cavalcante
本文主要研究集成形式化方法在容错实时系统(巴西微小卫星星载计算机)的形式化描述和验证中的应用。这项工作涉及一个框架的应用，该框架涵盖了从形式规范到分析和使用工具来证明系统的性质。我们使用了Timed-CSP-Z(Timed-CSP-Z)来描述系统的行为，然后提出了一种将规范转换为TER网的策略，TER网是一种基于时间的高级Petri网形式化方法。转换使我们能够使用解百纳工具来分析系统的行为。
In this paper we focus on the application of integrated formal methods to the specification and validation of a fault tolerant real-time system (the on-board computer of a Brazilian micro-satellite). The work involves the application of a framework which covers from the formal specification to the analysis and use of tools to prove properties of the system. We used Timed-CSP-Z, a combination of Timed CSP and Z, to specify the system behavior, and then a strategy for converting the specification to TER Nets, a high level Petri Nets based formalism with time. The conversion enables us to use the CABERNET tool to analyse the behavior of the system.