Research Initiation Award: Theory, Analysis and Applications of Hierarchical Predicate Transition Nets

形式化方法对于确保安全和关键任务系统的极高可靠性要求的重要性是众所周知的，但对于并发和分布式系统仍然缺乏成熟的形式化方法。最近发展了用于系统规范的层次谓词变迁网和用于分析谓词变迁网的时序逻辑技术。本研究的目的是：1)定义层次谓词变迁网的代数语义，以便进行各种代数变换；2)设计一种更实用、更强大的规格说明方法学，以促进层次谓词变迁网在现实系统中的实际应用；3)开发各种有效的分析技术，以确保层次谓词变迁网规范的正确性。这一研究为深入理解层次谓词变迁网及其与其他规格说明方法的关系迈出了重要的一步，并将为基于层次谓词变迁网的并发和分布式系统的形式化描述和验证奠定基础。

The importance of formal methods for ensuring extreme high reliability requirements of safety and mission critical systems is widely known, but mature formal methods for concurrent and distributed systems are still lacking. Hierarchical predicate transition nets for system specifications and temporal logic techniques for analyzing predicate transition nets have recently been developed. This research furthers previous work with the following objectives: 1) to define an algebraic semantics of hierarchical predicate transition nets in order to carry out various algebraic transformations; 2) to design a more usable and powerful specification methodology to facilitate the practical applications of hierarchical predicate transition nets to realworld systems; 3) to develop a variety of effective analysis techniques to ensure the correctness of hierarchical predicate transition net specifications. This research represents a significant step towards a solid understanding of hierarchical predicate transition nets and their relationship with other specification methods and will lay the foundation of a new and effective formal specification and verification methodology for concurrent and distributed systems based on hierarchical predicate transition nets.