论文部分内容阅读
当今社会,混合系统在嵌入式系统开发中起着至关重要的作用。混合系统中,软件控制器控制外部环境的变化,以离散的方式由传感器规律地触发来检测环境状态,控制环境。相邻的控制器行为之间,环境以连续的方式变化。如何设计出与物理环境正确匹配的控制器已成为一大挑战。众多学科都不断贡献于该领域,包括计算机、系统控制、模拟仿真等学科。在这些学科中,我们主要从事计算机学科的研究,但也与系统控制、模拟仿真等学科紧密相连。计算机学科对混合系统的研究主要为系统验证,相比于其它研究,我们的研究不仅仅着重于系统验证,也同时着重于建模、证明、仿真。我们的研究目如何构建正确的混合系统。确切地说,基于Event-B方法,我们研究自顶向下的混合系统开发方法:从需求文档,得到精化策略,而后建立系列的形式化模型,最终开发实现。模型开发基于系列的精化模型,使得系统能够以渐进的方式实现开发。在离散连续混合系统开发中,我们主要关注以下问题:定义良好的需求文档与精化策略、建立混合系统模型、实现模型精化、证明模型及精化的正确性、证明系统安全性质、实现系统仿真等。本文所展开的工作均围绕上述问题。本论文的主要贡献如下:(i)方法学贡献基于Event-B方法,在形式化建模之前,首先要定义需求文档及精化策略。精化策略用于定义精化模型中对需求的考虑顺序,实现从形式化模型到需求文档的可追踪性,并用于检查形式化模型是否已完整考虑需求。本文提出制定需求文档与精化策略所应遵循的规则。(ii)理论贡献提出Event-B含时间函数的混合系统的建模方法,并提出离散模型至连续模型的精化方法,以及该混合模型的分析验证方法。为支持复杂物理系统,我们扩展混合系统建模方法,引入一个新的方法,称为"Click",并基于该方法为混合系统的时间特性提出系统化的设计模式。对连续行为由微分方程定义的混合系统,在不解微分方程的前提下,我们研究微分方程性质的定理证明方法。该研究基于欧拉近似方法和非标准分析。(iii)实践贡献该研究包含众多案例,用于分析所提出的理论及方法。案例涵盖核反应冷却控制、列车控制、飞机防碰撞系统、水箱控制等。这些案例不仅用于分析所提出的理论,也在一定程度上证明了理论的应用性。提出混合系统形式化开发的互补方法,包括模型仿真、传感器和执行器设计模式、隐式不变式发现方法等。(iv)软件贡献为了互补Event-B形式化开发方法,将Event-B模型转化至Simulink模型,我们为Event-B言语的相应工具Rodin平台开发了插件,可以自动实现模型转化。