基于组件的异构规范的进程演算研究

We will propose a heterogeneous specification CAIA in a process algebraic style, which allows ones to freely mix usual operational operators (parallel, choice, hiding, etc.), logic operators (conjunction and disjunction) and quotient. This calculus supports compositional constructions and reasoning, component's reusability and incremental development, description of temporal properties. Main researches of this project include: 1) Provide the syntax and SOS rules of CAIA, prove that the refinement is precongruent; 2) Propose an axiomatic system for CAIA, prove its soundness and ground-completeness; 3) study equations and solutions in CAIA; 4) Give a graph representation of a temporal logic which could describe safety and liveness in CAIA, moreover, give a general theory of graph representation. This project gives us new insights into component-based heterogeneous specifications, and helps to understand deeply about relationships between operational specifications and logic specifications.

本项目拟发展一套进程演算风格的异构系统CAIA，允许进程算子（并发、选择、隐藏等）、逻辑算子（合取和析取）和商算自由地混合使用。这一系统同时具有操作规范组合性和逻辑规范抽象性的优点，支持组件的复用和增量式设计，且能够方便的刻画时序性质。研究的主要内容：1）给出CAIA语法和SOS语义，证明精化关系的前同余性；2）提出CAIA的公理系统，证明它的可靠性和基完备性；3）研究CAIA中方程和解的性质；4）研究能刻画活性和安全性的逻辑语言在CAIA中的图表示问题，进而给出逻辑规范在操作规范中图表示的一般方法。该项目将为基于组件的规范设计理论提供新的研究视角和技术手段，为逻辑规范和操作规范之间的联系提供新的见解，使之能更深入理解异构规范理论。

研究反应式并发系统有两个主流的路线：逻辑规范和操作规范，两者各有不同的研究角度及相应的优缺点，之间也有紧密的联系。本项目尝试为基于组件的规范设计提供一个异构规范理论，并为逻辑规范和操作规范之间的联系提供新的见解。按照项目计划，研究了能刻画安全性的逻辑语言ACTL的一个片段的图表示，并证明了进程p满足公式ϕ当且仅当p精化ϕ被编码后的进程，此项结果加深了对逻辑规范和操作规范的典型联系图表示的理解，为下一步研究图表示的一般理论打下了基础；针对共变-异变模拟探讨了确保其具有前同余的充分条件及其公理化，提出了CC-GSOS及CC-ntyft/ntyxt规则类型，证明了共变-异变模拟相对于CC-GSOS及CC-ntyft/ntyxt算子具有前同余性，另外基于CC-GSOS规则，提出了CC-模拟的可靠完备公理系统的一般性构造方法，这一结果加深了对共变-异变模拟的理解；项目组针对基于时间和空间分区的实时操作系统标准ARINC 653，使用能同时规范系统行为和状态的Circus语言，完成对分区实时操作系统框架及内核的设计和应用编程接口的实现，从时间和空间两个角度，展现出分区实时操作系统的优点和特色。项目组的规范的工作包括了ARINC 653协议中有的分区管理、进程管理和时间管理，及其没有的内存管理。