基于PROMELA的卫星自主控制逻辑安全性分析方法  

作　　者：赵景晖 

机构地区：[1]西安邮电大学,西安710000

出　　处：《电脑编程技巧与维护》2024年第3期174-176,共3页Computer Programming Skills & Maintenance

摘　　要：随着微处理技术的发展,卫星自主控制逻辑日趋复杂。传统的使用流程图、程序走查、单元测试、系统测试的方法,存在过于依赖相关人员主观能力和无法遍历全部程序执行路径的问题。基于线性时态逻辑的SPIN验证工具可以对使用PROMELA建模的分布式有限状态系统执行路径进行遍历,并可判定使用线性时态逻辑(LTL)公式表达的安全性目标是否能够被满足。研究给出了一种使用PROMELA对卫星自主控制逻辑进行建模的方法,并以卫星自主分离过程判定过程为例,对实际分析和改进过程进行演示。

关 键 词：逻辑验证 PROMELA语言 卫星设计 

分 类 号：TP311.52[自动化与计算机技术—计算机软件与理论] V448.22[自动化与计算机技术—计算机科学与技术]