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