Foundations of Heterogeneous Specifications Using State Machines and Temporal Logic

该项目将显著增强并发理论规范形式化的基础和实际效用，特别是接口理论，它用逻辑连接词丰富了状态机符号，从而有望实现更简洁的规范。该项目之前的工作已经看到MIA（模态界面自动机）界面理论的发展，该理论将de Alfaro和Henzinger的界面自动机与Larsen等人的模态转换系统相结合。与相关工作相比，MIA是不确定的，可以正确处理连接和内部行为，并允许完全的组合接口改进，同时保持组件兼容性的乐观观点。到目前为止，该项目还添加了时间逻辑运算符，用于表示接口内的安全属性，从而产生了真正的异构规范理论。本文提出的后续项目将在三个维度上进一步丰富MIA的异质性和实用性。首先，需要对MIA框架进行阐述，使其能够对活动性和公平性属性进行推理，并具备更合理、更成熟的接口细化概念。其次，扩展MIA的通信机制以处理值传递，并辅以共享变量通信机制；两者都是充分捕捉现代并行编程语言特性所必需的。第三，将MIA转化为行为类型理论，使其不仅适用于基于模型的设计，也适用于复杂并发系统的编程。这个项目的成果应该是新颖而富有表现力的界面和行为类型理论，以及围绕b谷歌的并行编程语言Go的原型工具，以及基于案例研究的演示和评估。

This project shall significantly enhance the foundations and practical utility of concurrency-theoretic specification formalisms, and in particular interface theories, that enrich state machine notations with logic connectives, thus promising more concise specifications. Prior work in this project has seen the development of the MIA (Modal Interface Automata) interface theory that combines de Alfaro and Henzinger´s Interface Automata with Larsen et al.´s Modal Transition Systems. In contrast to related work, MIA is nondeterministic, properly handles conjunction and internal behaviour, and allows for fully compositional interface refinement, all while preserving an optimistic view of component compatibility. The project so far has also added temporal-logic operators for expressing safety properties within interfaces, thereby yielding a truly heterogeneous specification theory.The follow-up project proposed here shall further enrich MIA´s heterogeneity and practicality along three dimensions. Firstly, the MIA framework shall be elaborated so as to be able to reason also about liveness and fairness properties, and equipped with an according and more sophisticated notion of interface refinement. Secondly, MIA´s communication mechanism shall be extended to handle value-passing and complemented by a mechanism for shared-variable communication; both are necessary to adequately capture features of modern parallel programming languages. Thirdly, MIA shall be cast into a behavioural type theory, thereby making it not only useful for the model-based design but also for the programming of complex concurrent systems. The outcome of this project shall be novel and expressive interface and behavioural type theories as well as accompanying prototypic tools centered around Google´s parallel programming language Go, together with demonstrators and evaluations on the basis of case studies.