近似形式化方法—实微分多项式进程代数研究

Traditional formal specification language e.g. process algebra is normally built on a set of discrete and abstract actions. Data flow and continuous state transfers are therefore not able to be specified, and the more important, it makes impossible for the formal mothods to carry on approximate analysis and computation with errors in this traditional process algebra framework. However, errors and approximation are unavoidable and necessary in engineerings. On the other hand, engineering problems are always involved in the computations of real differential polynomials. In this research project, a process algebra is constructed on differential polynomial rings over the field of reals. Concretely, At the specification level, (1) the syntax and its structural operational semantics，and (2) the notions of approximate behaviour equivalence relations and their computing approaches are realized. At the level of design and verification methods, (3) approximate variable refinement and abstraction methods, and (4) approximate model checking method are proposed. The key feature of the specification and methods is that not only are data flow and continuous state transfers able to be specified, but also errors are allowed and, the errors are controllable. At the level of applications, a tool prototype is developed based on the process algebra constructed over real differential polynomials, and is applied to the design and analysis of railway train control software systems.

传统的并发系统形式刻画语言，例如进程代数，建立在离散的抽象动作集合之上，因而无法表示数据流和连续的状态变化。更为关键的是，基于传统进程代数架构的形式化方法无法进行带误差的近似分析和计算，而误差和近似是工程计算不可避免的重要特征。另一方面，工程问题大多涉及实微分多项式的计算。为此，本项目在实数域上的微分多项式环上构建进程代数理论和方法。具体包括：在刻画语言基础理论层面，构造（1）语法定义及其结构性操作语义、（2）近似行为等价概念及其计算方法；在设计和验证方法层面，通过实数域上微分多项式环上的符号与数值混杂计算，构建（3）近似变元细化和抽象方法、（4）近似模型检测方法。特点是不但可以刻画数据流和连续的状态变化，而且允许带误差，但误差可控。在实际应用层面，基于所构建的实微分多项式进程代数理论和方法，开发原型平台工具系统，并应用于轨道列车运行控制软件系统的设计和分析。

并发系统大量存在于现实生活当中，形式化方法是并发系统设计和分析的有效途径，而进程代数是刻画和分析并发系统的主流形式语言和工具之一。传统的进程代数不能刻画数据流，也不能刻画连续的状态变化，而连续的状态变化在现实并发系统中大量存在。为解决这些不足，人们定义了一些混杂系统模型。已有的进程代数混杂系统模型，多是从具体的控制工程应用出发，还没有形成系统、完整的形式化理论和方法，同时缺乏带误差的近似分析和计算的能力。为了能够描述数据流和连续的状态变化采用状态上带实微分多项式系统标记的微分多项式变迁系统，构建了完整的实微分多项式进程代数理论和方法,解决或部分解决了以下三个问题：（1）在刻画语言基础理论层面，构造了语法定义及其结构性操作语义，以及近似行为等价概念及其计算方法；（2）在设计和验证方法层面，构建了近似变元细化和抽象方法和近似模型检测方法, 通过实数域上微分多项式环上的符号与数值混杂计算进行带误差的近似分析和计算，从而满足实际工程需求；（3）在实证示例和实际应用方面，探索所获得的理论和方法在轨道列车运行控制软件系统的设计与验证分析中的应用。科学意义在于所构建的理论和方法是软件等并发系统设计迫切需要的，不仅能表示数据流和连续的状态变化，而且能做到误差可控。