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

• 作者: 张海斌
• 来源期刊: 电脑知识与技术：学术交流
• 学科: 工学
• 关键词: 三模表决算法 形式化方法 时间自动机 系统验证
• 年，卷（期）: 2008,（11Z）
• 页码范围: 1257-1259
• 页数: 3页
• 分类号: TP332

摘要

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

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	张海斌	同济大学电信学院	2	1	1.0	1.0