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.