三模冗余箭机系统的设计及形式化分析

摘要：

针对航天系统的具体需求,本文首先设计了三模冗余箭裁计算机系统.接着通过形式化方法时三模冗余箭机系统协议进行分析,采用UPPAAL模型工具建立了CPU时间自动机、表决时间自动机、仲裁时间自动机及脉冲发生单元时间自动机.最后对模型进行仿真及相关性质的验证.经过验证,提取了两个重要的参数取值约束关系.该约束关系对于系统的设计具有一定的启发性,同时也保障了系统的安全性及可靠性.

关键词：三模表决算法、形式化方法、时间自动机、系统验证

所属期刊栏目：4

分类号：TP391.9(计算技术、计算机技术)

在线出版日期：2009-02-18（万方平台首次上网日期，不代表论文的发表时间）

页数：共4页

页码：1257-1259,1263