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