论文部分内容阅读
用Petri网对联锁系统中的核心部分--联锁机中的联锁软件进行形式化定义和分析,以减少联锁系统中的不确定性因素,降低联锁软件的复杂性,保证联锁软件定义的正确性,并对该定义进行了形式化验证.同时以进路建立过程作为事例,说明了用Perti网形式化定义联锁软件的具体过程.采用分层模型化技术对联锁软件中的各个变迁(模块)进行逐级分解和验证,最终得到经过验证的、足够详细的联锁软件模型.利用该模型能对系统的一些重要性能(如安全性和实时性)进行分析和改进.