嵌入式周期控制系统的建模与分析

发布时间：2018-01-03 23:01

本文关键词：嵌入式周期控制系统的建模与分析　出处：《华东师范大学》2012年博士论文　论文类型：学位论文

【摘要】：嵌入式周期控制系统广泛应用于汽车电子,航空电子等安全攸关的嵌入式领域.一般来说,这些控制系统都具有周期性行为,它们的共同特点是：(1)以模式为基础.一个周期控制系统由一组模式组成,系统处于一个模式表示系统处于一个特定的状态.每个模式或是包含若干子模式,或是周期性地进行控制计算.(2)面向计算.在一个模式中,周期控制系统会执行包含复杂的计算过程的控制算法.例如,在特点的模式下,一个汽车电子控制系统可以需要处理大量的即时数据,以便确定车辆的位置和姿态.(3)周期性.周期控制系统是一个反应式系统,可能会连续运行很长一段时间.每个模式的行为由其自身的周期决定.因此,大部分的计算任务都是在一个周期内完成的.如果没有发生模式切换,那么这些计算任务还将在下一个周期再次执行.在周期结束时,如果满足特定的条件,系统将从当前模式转入其它模式. 尽管这类系统被广泛地应用于航天／航空,汽车电子等安全攸关的嵌入式领域,但是工业界仍然缺少一种针对这一领域的形式化建模语言.我们曾对现有的建模语言做过广泛的调研,这些语言或是较为复杂,使用门槛较高,或是过于通用,难以处理这类系统的特征.因此,我们根据领域工程师的需求,设计了SPARDL建模框架.该框架主要包括两个部分,第一部分是作为建模标记的模式图(ModeDiagram),第二部分是规范语言SPRL. 模式图是以经典的状态图(Statecharts)[56]为基础,增加了支持周期控制系统建模的特殊领域需求的建模标记.模式图的核心部分是一组模式.每个模式都有特点的周期长度.不同的模式的周期可以不同.在周期结束时,如果满足一定的条件,将发生模式切换.允许模式嵌套,也允许模式-子模式之间发生切换.与其它建模语言相比,SPARDL的特色之一是模式之间的迁移条件是可以涉及历史状态的时序表达式. 模式图的结构是层次化的,分为模式-控制流-模块三个层次.一个模式既可以包含若干子模式,也可以包含一个控制流.控制流是特定的控制算法,计算任务的封装.控制流的细节在控制流层面表述.允许在控制流中调用模块,模块的细节在模式层展示. 为了支持模式图的形式化推理,SPARDL框架还包括基于区段演算[42]的规范语言.该语言适于描述领域工程师关心的时序性质. SPARDL模型的正确性取决于它的模式图是否满足规范.由于SPARDL模型可能涉及到复杂的非线性运算,因此,完整的验证是不可行的.为了解决这个问题,本文利用概率模型检查技术[125,126]验证SPARDL模型.试验结果表明,本文的方法学能够发现真实系统中的设计错误. 本文主要有下列贡献： ●提出了新的形式化建模框架SPARDL,该框架的主要目的是为嵌入式周期控制程序提供一套清晰而准确的建模机制. ●通过两种方式研究了SPARDL的形式化语义,一是将SPARDL模型解释为价格时间自动机(Priced Timed Automata),二是在迁移系统上定义它的操作语义.在操作语义的基础上讨论了SPARDL的类型安全,互模拟,等价等问题. ●在形式化语义的基础上,实现了SPARDL的仿真.并扩展了最初的操作语义,提出了SPARDL的概率语义.根据新的概率语义,开发了以仿真为基础的概率模型检查,用于验证SPARDL模型是否满足各种时序性质. ●在真实的案例中试用了SPARDL眶架,发现了一个控制系统中的两个真实的缺陷.试用结果充分说明了SPARDL的有效性.
[Abstract]:Embedded cycle control system is widely used in automotive electronics, embedded field of aviation electronic safety. In general, these control systems have periodic behavior, their common features are: (1) to pattern based. One cycle control system consists of a set of patterns, the system is in a mode of the system is a particular state. Each mode is or contains a number of sub models, or periodically control calculation. (2) for computing. In one mode, the control algorithm of cycle control system will perform the calculation process includes complex. For example, the characteristics of the model, a vehicle electronic control the system can deal with the immediate needs a large amount of data, in order to determine the position and attitude of the vehicle. (3) a periodic cycle. The control system is a reactive system, may run continuously for a long period of time for each mode. On the grounds of its own cycle decision. Therefore, most computing tasks are completed in a period. If there was no mode switching, so these tasks will be in the next cycle is executed again. At the end of the cycle, if satisfy certain conditions, the system will be transferred to other modes from the current mode.
Although this type of system is widely used in aerospace and aviation, automotive electronics and other fields of embedded security at stake, but the industry still lacks a formal modeling language in this field. We have the existing modeling languages have done extensive research, these languages or more complex, with a higher threshold, or is too general, characteristics of difficult to deal with this kind of system. Therefore, we according to the field engineer needs to design the SPARDL modeling framework. The framework mainly includes two parts, the first part is as a model graph modeling marker (ModeDiagram), the second part is the specification language SPRL.
Model mapping is a state diagram of the classic (Statecharts) [56] based modeling markup special field demand control system modeling support cycle. The core part of the pattern is a set of mode. Each mode has the characteristics of cycle length. Different periodic patterns can not the same. At the end of the cycle, if meet certain conditions, will allow the mode switch. Nested mode also allows, between sub mode switching mode. Compared with other modeling language, one of the features of SPARDL is the migration conditions between the modes is temporal expressions can relates to historical state.
The diagram is hierarchical, divided into model control flow module three levels. A model can contain several sub models, can also include a control flow control flow control algorithm is given. The calculation task package. Details of the control flow in the control flow level allowed in the statement. The control flow in the calling module, display module details in the model layer.
In order to support formal reasoning of schema diagrams, the SPARDL framework also includes a specification language based on section calculus [42]. This language is suitable for describing the timing properties of domain engineers.
Right depends on the mode of the SPARDL map in it whether meet the specifications. The SPARDL model may involve complicated nonlinear operation, therefore, the complete verification is not feasible. In order to solve this problem, this paper using [125126] probability model checking the SPARDL model. The experimental results show that this method can find the design the error in the real system.
The main contributions of this article are as follows:
A new formalized modeling framework (SPARDL) is proposed. The main purpose of the framework is to provide a clear and accurate modeling mechanism for the embedded cycle control program.
The formal semantics of SPARDL is studied by two ways, one is the SPARDL model to explain the price for the automaton (Priced Timed Automata) time, two is the definition of its operational semantics in the migration system. The operational semantics based on discussion of SPARDL type safety, bisimulation equivalence, and other issues.
In the basis of the formal semantics, SPARDL realized the simulation. And expanded the original operational semantics, probabilistic semantic SPARDL. According to the new development of the probabilistic semantics, probability model checking based on simulation, SPARDL model is used to verify whether meet the various temporal properties.
The SPARDL orbital frame was tested in a real case, and two real defects in a control system were found. The trial results fully illustrate the effectiveness of the SPARDL.

【学位授予单位】：华东师范大学
【学位级别】：博士
【学位授予年份】：2012
【分类号】：TP368.1;TP273

【共引文献】