基于OOTCPN模型的嵌入式系统设计方法研究

发布时间：2020-12-09 06:27

　　嵌入式系统,作为计算机技术中的一项重要研究方向,已经被广泛地应用到各个领域。随着嵌入式产品在不同领域的应用,用户需求的不断增加,嵌入式系统功能越来越强大,设计难度也越来越大,导致传统的设计方法难以满足复杂嵌入式系统的设计需求,因此研究系统级的设计方法已成为嵌入式系统设计的主要研究方向。本文通过对现有嵌入式系统建模方法的研究,分析其特点和不足,引出形式化建模是嵌入式系统建模研究的主要方向。针对基本Petri网在嵌入式系统建模中处理数据能力弱、没有考虑时间因素和没有层次结构的问题,通过引入面向对象技术、时延网和有色网,扩展了基本Petri网,给出了面向对象的时延有色Petri网(OOTCPN)模型的形式化定义。与其他模型相比,本文模型在数据描述能力、实时性、层次性等方面有了较大的提高,适合复杂的嵌入式系统建模。在模型验证方面,通过对基本Petri网模型的验证技术研究,分别阐述了仿真分析和模型检验方法的原理和特点,探讨了Petri网模型的电路仿真分析方法,给出了利用硬件描述语言描述OOTCPN模型的方法,并通过实例说明。与传统的Petri网仿真分析软件相比,此方法适用范围更广,可移植性强,使... 

【文章来源】：西华大学四川省

【文章页数】：70 页

【学位级别】：硕士

【部分图文】：

面向对象模型

图 4.8 仿真图Fig. 4.8 Simulation diagram4.3 模型检验技术模型检验是关于系统性质验证的算法和方法[43]。在完整的系统属性的验证框架下，通常采用状态空间搜索的方法来检测模型是否满足用时序逻辑公式表示的特定性质。由于模型检验的方法在许多方面如电信系统和硬件系统的验证等取得了成功，得到了越来越多的人关注；并且，随着计算机不断的发展和软件算法的不断优化，该方法展示出广泛的应用前景。与模型检验相关的是时态逻辑，时态逻辑是模型检验的基础，是对系统属性的形式化表示。在时态逻辑中，时间特性并没有显示的表现出来，相反，在公式中可能会描述某一个特定状态最终会到达，或者描述某一个错误状态从不会到达。通过分支时间的观点和线性时间方法可以把时态逻辑分为两个主要部分：CTL(计算树逻辑)和 LTL(线性时态逻辑)。4.3.1 计算树逻辑

解电梯的运行情况以后，根据电梯的运行策略，建立电梯的模型。在 OOT，包含若干个对象类，一个对象类就是一个 Petri 网的子系统，而对象类的颜色集和托肯集综合表示；操作可以用变迁来表示。为了以后电梯控制系统方便，在这里首先按照面向对象的技术对系统进行分类。电梯控制系统按照为三大类，类及类之间关系的结构图如图 5.2 所示。


本文编号：2906442