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.