论文部分内容阅读
信息物理融合系统是一种融合了感知、计算、通信、控制能力的物理设备系统,通过系统内物理进程与计算进程相互影响的反馈循环从而实现自治。随着信息技术的更新换代与不断发展,信息物理融合系统的应用领域也不断扩展,大到核工业复杂控制系统、国家智能电网等涉及国家乃至世界的复杂系统,小到自主感控与计算的植入式家庭医生设备、自动巡航系统。这些系统与我们的正常生产与生活密切相关,一旦出现问题可能会带来不可估量的损失。一般来说,这类系统的构成比较复杂,它的正确性不仅仅对某单一组件有要求,也与同一类组件之间、不同类组件之间的交互是否正确有关。相对于一般的软件系统,信息物理融合系统的异构性、交互的复杂性、一定的可预测性以及更高的安全性需求给这类系统的描述、设计、分析和验证带来了更大的挑战。如何保证信息物理融合系统的正确性成为国内外工业界和学术界的难题之一。在计算机科学领域里,程序理论和代数方法可以用来保证软件产品的正确性,在其理论指导下,有很多成功的开发实例。但是基于程序理论的开发或者验证方法多数针对离散系统,由于物理设备连续状态的引入,传统的方法不再奏效。控制领域有多年借用数学建模的方法去仿真模拟物理系统的经验,但是其对信息系统的关注研究较少。对于这类系统来说,只是单就某一类组件进行分析,即使这一类组件本身的研究已经很到位,但也极有可能是不安全的。要保证信息物理融合系统系统的正确性首先要解决的是如何将以一定方式交互的物理设备和信息系统融合在同一框架下做分析推理。本文提出了一种针对信息物理融合系统的基于事件交互机制的新型建模语言HyML,使得信息物理融合系统中的各个元素能够在同一个框架内进行分析推理。在程序统一理论的指导下,我们研究了混成建模语言HyML的指称语义以及代数语义,帮助程序开发人员从不同的角度认识理解语言,并且证明了代数语义相对于指称语义的一致性。然后给出了混成程序的规范型,并支持利用可证代数规则对程序进行简化。最后研究了利用可证代数规则进行程序分解的方法。本文针对信息物理融合系统的描述语言的研究为复杂系统语言研究及语义探索奠定了理论基础,并且展示了代数方法在语言理论研究中的重要性。本文的主要内容包括:·从信息物理融合系统的建模需求出发,提出了一种基于事件的新型建模语言HyML,该语言不仅可以刻画信息物理融合系统的异构功能性组件,而且实现了信息系统与物理系统交互模式的融合。新型的卫兵结构不仅继承了离散部分的交互模式即事件卫兵,还引入了混合卫兵支持连续部分与其他部分之间的交互。·给出了HyML语言面向观察的指称语义模型,研究了HyML的代数语义模型,并且证明了代数语义相对于指称语义的一致性,从而增强了我们运用代数规则完成程序转化的可靠性。·探索了在HyML框架内利用代数语义理论辅助可信系统开发的具体方案。提出了混成程序的规范型,并证明了所有混成程序都可以转化为规范型。提出了一种粗粒度的程序分解框架,利用可证代数规则将初始规范转换为物理程序与控制程序的并发组合,控制程序部分可进一步应用于后续的开发过程。