【作者】 周青；

【导师】 张伟；

【作者基本信息】 江南大学 ， 计算机应用技术， 2009， 硕士

【摘要】 随着嵌入式系统在各个领域的广泛应用,嵌入式系统变得越来越复杂。在嵌入式系统设计中采用模型的方法,有利于确保系统的正确性,缩短开发周期,降低开发费用。本文以Perti网为建模工具,对嵌入式系统的建模和分析验证进行了一些研究。嵌入式系统具有实时性、并发性等特点,并要求高可靠性和正确性。为了设计具有这样特点的系统,设计过程必须基于一个形式化描述,以捕获嵌入式系统的这些特点。Petri网对这类系统是一个很好的描述方法:可以表示并行和连续活动,并且很容易捕捉不确定性行为。但传统的Petri网缺乏时间概念和数据表达力,不能很好的描述嵌入式系统的实时性要求和数据流。针对传统Petri网的这些缺点,本文提出基于PRES+的嵌入式系统的建模与分析验证研究。首先,介绍嵌入式系统的一个形式化计算模型PRES+,可以描述嵌入式系统的一些重要特征,其中,托肯携带数据信息,变迁执行数据的转换,时间通过与变迁相连的活动期限来捕获。同时,引入PRES+模型的分层机制和组合修改操作。分层机制使模型能够有条理的构建,由简单的单元组件构成,使得设计师在每个描述级上都可以很容易理解;组合修改操作,通过增加或减少模块来改变其功能或状态,从而以最小的影响,实现了网模型的修改,并有效保存了系统的性质,使系统在修改后不需要再重新验证其性质。其次,介绍了系统模型的分析与验证,对基于PRES+建模的嵌入式系统,分别提出两种方法,对它进行分析验证。第一种为形式化验证方法,利用模型检测来验证系统的一些性质,将其表示成时序逻辑公式。介绍了一个转换程序,把PRES+模型转换成时间自动机TA,并使用模型验证工具UPPAAL对其进行分析验证;第二种方法,通过程序模拟Petri网中各个库所中托肯的变化情况,模拟Petri网的动态行为,从而达到分析验证的目的。最后,提出一种策略,使用正确性保留等价转换,对PRES+模型进行简化,从而提高其验证效率。更多还原

【Abstract】 Embedded systems becomes more and more complicated with its widespread use in a variety of domains. Modeling approach could improve the correctness,shorten the period of design,and reduce the cost in embedded system development.Base on Petri Net,we did some research on embedded system modeling and verification.Embedded sytems are characterized by their dedicated function,real-time and concurrent behavior,and high requirements on reliability and correctness.In order to devise systems with such features,the design process must be based upon a formal representation that captures the characteristics of embedded systems. Petri nets are an good represnetation for this sort of systems: it can represent parallel as well as sequential activities and easily capture non-deterministic behaviors.However,the traditional Petri net model lacks the notion of time and data expression,it can not represent the real-time requirement and data flow.To meet these problems,this paper proposed the research on embedded system modeling and analysis base on PRES+.First ,we present a formal computation model PRES+ for embedded system .The model can capture some important features of embedded sytems,in which tokens hold information,transitons perform transformation of data,and timing is captured by associating lower and upper limits to the duration of activities related to transitions.Furthermore,introduce the Hierarchy mechanism as well as the compositon and modification operation.Hierarchy is a useful tool that allows the system to be constructed in a structured way by composing a number of fully understandble entities;The composition and modificaion operation can change the functions or statesadd by adding or reducing the module,thus,it changes the net model in a lower effect,and perserves the system properties,so that we need not to verify its properties after changed again.Sencond ,we presnet the analysis and verification of the system model, propose two methods to analyze and verify the systems represented in PRES+,the first method is the formal verification,in which model checking is used to prove whether the system model satisfies its required properties expressed as temproal logic formulas.Introduce a translation procedure that translate the PRES+ model to time automata,and then analyze and verify the TA model using the Uppaal;the second method,through the program to simulate the changes of the token in every places,simulate the dynamic behavior of Petri net to achieve the analysis and testing purposes. Besides,propose a strategy, simplify the PRES+ model through the correctness-perservation equivalent translation,in order to improve the verification efficiency.更多还原