基于Reo的协调理论及其在信息物理系统开发方法中的应用

The project is proposed according to the evolution of coordination theory and new development technologies required by CPS (Cyber-Physical Systems), and will mainly focus on the problems including theoretical models of hybrid connectors based on Reo, quantitative model checking and testing techniques for connectors, and dynamic reconfiguration and self-adaptation patterns of connectors in CPS. We will develop new rigorous methodology and techniques for modeling and verification of connectors that are used to coordinate the interaction among the computing processes and physical processes in CPS. In this project, we mainly concentrate on the following three working packages: (1) develop the theoretical model for hybrid connectors that are proper for describing the interaction protocols in CPS; (2) investigate theories and techniques for automatic verification and dynamic testing of QoS-aware quantitative connectors in CPS; (3) investigate dynamic reconfiguration and self-adaptation patterns of connectors in CPS. The proposed research may offer great benefits to improve the correctness, controllability, confidence, security, scalability and efficiency, simplify the task for system update and maintenance, and promote the development of new technologies for CPS.

本项目根据协调理论的发展和信息物理系统开发方法的需要提出，主要对基于Reo的混成连接件理论模型、连接件的定量模型检查和测试技术以及信息物理系统中连接件的动态重配置及自适应调整模式等重要问题进行研究。本项目将开发对信息物理系统中计算进程和物理进程之间交互进行协调的连接件进行建模和验证的严格方法和技术。研究重点将集中在下面三个方面：（1）设计适于信息物理系统中交互协议描述的混成连接件理论模型；（2）研究信息物理系统中服务质量感知的连接件定量性质的自动验证和动态测试的理论和技术；（3）研究信息物理系统中连接件的动态重配置及自适应调整模式。本项研究对于提高信息物理系统的正确性、可控性、可信性、安全性、可扩展性和效率，简化系统升级及维护的工作，以及推动信息物理系统开发方法学的发展，在理论和实践上都具有重要意义。

协调机制将系统中不同组件的交互与组件内部的计算过程分离开来，使得组件之间的交互不必依赖于组件的具体实现。协调语言已经成功地用于多种类型系统的开发过程之中，并受到了信息物理系统领域研究人员的高度关注。本项目以协调语言Reo作为基础，对混成连接件的形式化模型、连接件定量性质的验证与测试方法、信息物理系统中连接件的动态自适应调整及重配置模式进行研究，在多个方面取得了创新性的成果。主要成果包括：.1) 给出了混成连接件的理论模型，提出了混成约束自动机的概念并成功地将约束自动机用于混成连接件的语义描述，证明了混成约束自动机乘积操作的可组合性。.2) 给出了连接件在定理证明工具Coq中的实现，并利用Coq对连接件的一些性质成功给出了自动证明。在此基础上进行了进一步扩充，在Coq中开发了连接件的线性时态逻辑LTL模型检查工具，并对电子政务领域门禁系统中复杂交互行为的建模和验证进行了研究。.3) 提出了一种实时连接件的离线测试方法，连接件的规范通过时间约束自动机给出，通过对实时连接件和定义生成的测试集进行并发操作，对连接件的行为进行测试，开发了从时间约束自动机到UPPAAL的转换工具，测试过程可在UPPAAL工具中自动完成。.4) 对自适应调整的形式语义进行了研究，将其形式化描述为余代数基调函子之间的自然转换，经过自适应调整的变换后，我们可以通过自然转换上的互模拟关系或者精化关系，来对连接件的性质加以验证。.本项研究对于解决信息物理系统的正确性、可靠性，推动信息物理系统建模、验证技术及其相关方法学的发展，具有重要意义。