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

研究启动奖：层次谓词转移网络的理论、分析与应用

• 批准号: 9308003
• 负责人: Xudong He
• 金额: $ 7.59万
• 依托单位: North Dakota State University Fargo
• 依托单位国家: 美国
• 项目类别: Standard Grant
• 财政年份: 1993
• 资助国家: 美国
• 起止时间: 1993-08-15 至 1997-07-31
• 项目状态: 已结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=9308003&HistoricalAwards=false
• 关键词: Research; Initiation; Award; Theory; Analysis

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.

正式方法对于确保极高的 安全和使命关键的可靠性要求 系统是众所周知的，但成熟的正式方法， 仍然缺乏并发和分布式系统。 系统的层次谓词转移网 规范和时序逻辑技术， 最近开发了谓词转换网。 本研究通过以下方面进一步推进了以前的工作 目标：1）定义一个代数语义的 层次谓词转移网，以执行 各种代数变换; 2）设计一个更 可用且功能强大的规范方法， 层次谓词的实际应用 将网络过渡到现实世界的系统; 3）开发一个 各种有效的分析技术，以确保 层次谓词转移网的正确性 规范. 这项研究代表了重要的一步 对层次谓词的深入理解 过渡网及其与其他 规范方法，并将奠定基础，一个新的 有效的形式化规范和验证 并行和分布式系统的方法论 层次谓词转移网。