【作者】 苏雯；

【导师】 朱惠彪；

【作者基本信息】 华东师范大学 ， 计算机应用技术， 2013， 博士

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

【Abstract】 Nowadays, hybrid systems are very important in the development of embedded systems. In such systems, a piece of software, the controller, is supposed to manage an external situation, the environment. The controller works in a discrete fashion in that it is triggered regularly by detecting the status of the environment (using some sensors), and then reacts by sending some information to the environment (using some actuators). Between two successive controller detections and actions, the environment is evolving in a continuous way. The design of a controller that correctly matches the physical environment has become a challenge.Various scientific community have contributed with their own approaches to this area:computer science, control, and modeling and simulation communities. We mainly place ourselves in the computer science community, but we also have some connections with the control community, and the modeling and simulation community.Other works in computer science community mainly focus on software verifica-tion, here we would like to propose an approach that certainly focus on verification, but also on modeling, simulation, and proof. Our purpose is to construct hybrid systems in a correct fashion. More precisely, based on Event-B, we propose a top-down approach that supports the development of hybrid systems from requirements down to final development. For this, our con-struction is based on successive refinements, allowing the development to be done in a gradual fashion. In the development of hybrid system, we concentrate on the following key issues:well-defined requirement document and refinement strategy, modeling, refinement, proving, and simulation.Here are the main contributions of this thesis:(i) Methodology Contribution Based on Event-B, requirement document and refinement strategy need to be first defined before formal modelling. We insist a lot on the importance of writing a well defined requirement document and a careful refinement strategy. Before modeling, the refinement strategy is used to define clearly how the requirements can be gradually taken into account in successive refinements. It also helps us to trace the formal development back to the requirement document, and check whether we have taken all requirements into account. To achieve this, we propose some rules for defining the requirement document and the refinement strategy,(ii) Theoretic Contribution We explain how hybrid systems with time function can be developed in Event-B and we show how we can transform a discrete approach to a continuous one. This is based on the usage of refinement. In order to support complex physical system, we extend the approach of model-ing hybrid systems with a new one called "Click":this constitutes a systematic design pattern for the time feature of hybrid systems. For those hybrid systems where the continuous parts are defined by differential equations, we try to give a theoretical approach on how to prove properties of differential equations without solving them. This work is based on solid mathematic foundations:the usage of Euler approximations and that of non standard analysis,(iii) Practical Contribution This study contains many practical examples whose role is to explain our approach. Such examples cover nuclear cooling control, train control, aircraft collision avoidance, water tank, etc. We believe that examples are important to show that this approach to hybrid systems can be made practical. In order to improve the confidence in formal modeling, we also propose some complementary approaches for hybrid system development. This includes the usage Simulink and animation, the introduction of sensor and actuator pat-terns, and an implicit invariant discovery approach as well.(iv) Software Contribution In order to complement formal development and translate Event-B model to Simulink model, we developed a plug-in for the Rodin platform. This plug-in can perform this translation automatically.更多还原