基于事件的形式化模型的表达能力与工程方法研究

All kinds of life-critical and safety-critical systems are usually complex cyber-physical systems. To ensure their correctness and reliability, they are required to adopt formal analysis and verification. However, since existing formal models have not enough expressive powers and sound engineering methods, they cannot directly analyze and verify the complex systems. This proposal is to investigate the expressive power and engineering method of event-based formal models and explore the mechanism of extending the formal models so that the formal models can represent complex cyber-physical systems. We will adopt the method that is different from traditional ones, which directly neither extends the mechanisms and constituent parts of formal models nor compares event-based formal models with other ones, but do research on the fields of communication, mobility , scheduling and so on. This method will explore how to use event-base formal models to simply, directly specify the communication, mobility, scheduling of complex systems. Based on these investigations, we explore the method of improving the expressive power of event-based formal models. On the other hand, during the efforts of modeling, we will investigate how event-based formal methods are incorporated into software development methods, develop the corresponding tools and realize the event-based formally engineering method.

各种安全、生命攸关的系统常常是复杂的信息物理融合系统，为保证其正确、可靠，必须采用形式化模型分析与验证。然而，现有的形式化模型的表达能力有限，而且没有完善的工程方法，无法直接分析和验证这些复杂的系统。本项目研究基于事件的形式化模型的表达能力和工程方法，探索扩展基于事件的形式化模型的机理，以期能建模复杂的信息物理融合系统。本项目采用不同于传统的方法进行研究，既不直接扩展形式化模型的机制和组成部分，也不从理论上比较基于事件的形式化模型与其它形式化模型的表达能力的差别，而是从通信、移动性、调度等关键领域进行具体研究，探究基于事件的形式化模型能否简单、直接地对复杂系统的通信、移动性、调度等问题建模。在这些具体领域建模的基础上，研究提高基于事件的形式化模型建模（表达）能力的方法。与此同时，考察如何将基于事件的形式化模型嵌入到软件开发方法中，开发相应的工具，实现基于事件的形式化工程方法。

生命攸关的系统常常是复杂的信息物理融合系统，为保证其正确、可靠，必须采用形式化模型分析与验证。现有的形式化模型的表达能力有限，而且没有完善的工程方法，无法直接分析和验证这些复杂的系统。本项目研究基于事件的形式化模型的表达能力和工程方法，探索扩展基于事件的形式化模型的机理，以期能建模复杂的信息物理融合系统。项目采用不同于传统的方法进行研究，既不直接扩展形式化模型的机制和组成部分，也不从理论上比较基于事件的形式化模型与其它形式化模型的表达能力的差别，而是从通信、移动性、调度等关键领域进行具体研究，探究基于事件的形式化模型能否简单、直接地对复杂系统的通信、移动性、调度等问题建模。一方面，在这些具体领域建模的基础上，研究提高基于事件的形式化模型建模（表达）能力的方法。而另一方面则考察如何将基于事件的形式化模型嵌入到软件开发方法中，开发相应的工具，实现基于事件的形式化工程方法。..经过四年的研究，项目组取得了以下成果:.（1）在理论上，a）建立起用基于事件的形式化模型——依赖结构建模和分析复杂信息物理融合系统的方法； b）提出复杂系统的功能自动分解方法； c）初步建立起基于事件的模型的形式化工程方法。.（2）在国内外刊物和会议上发表了12篇论文，其中一篇为理论计算机科学国际顶级刊物Information and Computation的论文，另一篇则为软件工程国际顶级刊物ACM Transactions on Software Engineering and Methodology的论文。.（3）在人才培养方面，培养了6名硕士毕业生，其中一名已经成为了一名博士研究生。.（4）在应用方面，利用依赖结构建模和分析复杂信息物理融合系统的理论，正在用于真实的产业项目——多机器人运动安全验证，获得了2021年CCF-华为创新项目产业项目（编号CCF-Huawei FM2021003）的支持，初步实验表明，该理论能够初步解决多机器人间碰撞或机器人同工作对象的碰撞等运动安全问题。. 总之，项目组严格按计划进行研究，圆满完成了在计划书中要求达到的目标。