A Semantically-Based Methodology for Proving Safety, Liveness, and Security Properties of Parallel Systems

当前建立并发系统行为属性的研究使用了几种不同的聚合语义，每一种都有自己的适用领域。这个项目开发了一个统一的外延语义框架，用于在广泛的范例中推理并发程序的安全性和活动性属性，包括共享变量并行、异步通信进程、数据流网络和Java风格的并发对象。基于“转换轨迹”的单一、简单的数学模型被用来解释这些范例，允许跨范例分析和比较程序和规范。这种指称方法还支持句法指导的推理或构词推理。通过将并发性与过程和局部变量声明相结合，开发的框架将支持Java风格的并发面向对象编程，并有助于为设计正确和安全的Java程序开发正式的基础。确定了适用于多种范式的推理原则，以及特定于特定范式的等价律。为了展示转移跟踪方法的实用性和优势，将基于语义的技术应用于安全协议。该项目还探索了基于语义的推理在提高自动模型检测效率方面的适用性。

Current research to establish behavioral properties of concurrent systems uses several different paradigmatic semantics, each with its own domain of applicability. This project develops a unifying denotational semantic framework for reasoning about safety and liveness properties of concurrent programs in a broad variety of paradigms, including shared-variable parallelism, asynchronous communicating processes, dataflow networks, and Java-style concurrent objects. A single, simple, mathematical model based on "transition traces" is applied to interpret these paradigms, permitting analysis and comparison of programs and specifications across paradigms. This denotational approach additionally supports syntax-directed, or compositional, reasoning. By combining concurrency with procedures and local variable declarations, the framework developed will support Java-style concurrent object-oriented programming and assist in developing a formal basis for the design of correct and secure Java programs. Principles of reasoning that apply to multiple paradigms, as well as laws of equivalence specific to a particular paradigm, are identified. To demonstrate the utility and advantages of the transition-trace approach, semantically-based techniques are applied to security protocols. The project also explores the applicability of semantically-based reasoning in improving the efficiency of automated model checking.