基于分层模型和规则描述的离散事件系统形式化方法

离散事件系统（DES）具有的分布、异步和并发等特点造成了对其建模和分析的复杂性，导致DES可信性低。很多DES均是安全关键（Safety Critical）系统，可信性低将造成严重的后果，甚至灾难。因此提高DES可信性成为信息、数学、控制等多门学科共同关注的热点。在计算机科学领域内，形式化方法是解决这一问题的有效途径。课题提出并建立基于对象的DES分层建模方法，创建以对象为节点的树状分层模型；研究对象之间关系的形式化描述问题，提出基于规则的形式化描述方法；构建用于规则描述的逻辑规则描述语言（LRDL），并证明其一致性、准确性和完备性；分析该方法与Petri网的关系，探求它们之间的转化方法。课题研究最终将形成一套明确、完整，易于人员理解和机器实现的DES形式化方法，保证DES建模和分析一致、严谨和高效，有效提高DES的可信性。