The time Petri net model of the ship-to-air missile launrh control software is constructed and the safety is analyzed with the assist of Tina toolbox, to determine the reachability of hazard statements, consider about the sequence of occurrence of software behaviors, some methods are proposed to improvement the software and avoid the hazard statements.%文中借助时间Petri网出色的图形表达能力和对动态行为的描述,在Tina工具辅助下完成了对舰空导弹发射控制软件建模和安全性分析,分析了高风险状态的可达性,考虑到软件时效对安全性的影响,提出了一些改进建议以避免高危状态的出现.
展开▼