基于Petri网的嵌入式系统建模与验证研究

发布时间：2021-07-01 12:54

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

【文章来源】：江南大学江苏省 211工程院校 教育部直属院校

【文章页数】：72 页

【学位级别】：硕士

【文章目录】：
摘要
ABSTRACT
第一章 绪论
    1.1 研究背景
    1.2 研究现状
    1.3 本文的研究工作及其意义
    1.4 本文的基本结构
第二章 嵌入式系统的模型概述
    2.1 嵌入式系统的特点
    2.2 嵌入式系统的设计流程
    2.3 嵌入式系统建模的常用方法
        2.3.1 有限状态机
        2.3.2 状态图表
        2.3.3 数据流图
        2.3.4 Petri 网
    2.4 本章小结
第三章 基于PRES+的实时嵌入式系统建模
    3.1 基本 Petri 网
    3.2 基本PRES+模型
        3.2.1 PRES+的基本定义
        3.2.2 PRES+的功能性描述
        3.2.3 PRES+的动态行为描述
    3.3 PRES+的等价和分层概念
        3.3.1 PRES+的等价概念
        3.3.2 等级 PRES+模型
        3.3.3 建模实例
    3.4 PRES+的组合与修改操作
        3.4.1 网加和网减运算
        3.4.2 组合与修改的建模实例
    3.5 本章小结
第四章 PRES+模型的分析与验证
    4.1 PRES+模型的分析
    4.2 形式化验证方法
        4.2.1 时间自动机
        4.2.2 验证工具 UPPAAL
        4.2.3 PRES+模型到TA 模型的转换
        4.2.4 铁路岔口问题
    4.3 动态行为的模拟
        4.3.1 普通Petri 网动态行为的模拟
        4.3.2 PRES+动态行为的模拟
    4.4 简化PRES+模型
    4.5 本章小结
总结与展望
致谢
参考文献
附录：作者在攻读硕士学位期间发表的论文


【参考文献】：
期刊论文
[1]基于Petri网的分布式实时嵌入式系统调度的建模[J]. 张海涛,艾云峰.  计算机工程. 2006(18)
[2]面向对象的Petri网在嵌入式系统开发中的应用[J]. 廖晓文,吴永明.  微型机与应用. 2005(04)

博士论文
[1]基于Petri网的嵌入式系统高层级设计方法与技术研究[D]. 郭军.西北大学 2007

硕士论文
[1]基于UML与Petri网的嵌入式系统建模方法的研究[D]. 廖晓文.广东工业大学 2005



本文编号：3259171