基于OOPN的嵌入式系统的建模研究与实现

本文结合了面向对象和Petri网两种建模方法的优点，提出了一种新的面向对象Petri网的建模方法。主要研究了面向对象Petri网方法在嵌入式系统设计中的具体应用，并通过实验对该方法进行了正确性论证以及资源分配情况的定量分析。该方法为嵌入式系统的设计提出了一种行之有效的形式化分析方法，使得复杂的嵌入式系统描述更加模块化，具有可重用性，大大提高了嵌入式系统建模和分析的效率。     

基于UML-OCPN的嵌入式系统建模

针对统一建模语言（UML）缺乏精确的形式化的语义描述而不能对其所建模型进行分析和验证的难题,提出一种改进的建模方法——UML-OCPN方法。该方法结合UML和对象着色Petri网（OCPN）的优点,使用UML进行建模,将其转换为Petri网模型再进行模型验证。实验结果证明,该方法能较好地解决单一使用UML或Petri网建模时出现的无法进行验证、需要开发人员具备较高数学水平等问题。     

分布式嵌入式系统实时调度的建模

针对RBTPN模型在建模分布式嵌入式系统实时调度时的不足,提出了一种新的扩展时间Petri网模型。该模型通过在需要处理器资源的变迁上引入变迁速率因子,得到具有相同优先级变迁的运行速率函数,从而在分布式嵌入式系统的调度建模中,在单个处理器上结合了固定优先级可抢先调度和轮转调度。随后给出了该模型可达图的构造方法,以便可以得到调度序列的各种性质。     

基于扩展Petri网的系统建模及形式化验证方法*

嵌入式实时系统对时间约束性、安全性和可靠性具有非常高的要求,但是传统的建模和形式化验证方法难以满足对系统的实时性和安全性的模拟和验证需求。通过对有色Petri网的时间属性进行扩展,提出了实时有色Petri网模型,能够对系统的时间属性进行模拟和评估;参考实时有色Petri网模型到时间自动机的语义转换规则对模型进行转换,可以利用时间计算树逻辑对系统的实时性、安全性和可靠性进行形式化验证。以列车通信网络控制器的双线冗余控制模块的建模和形式化验证为例,证明了该方法的有效性。     

基于Petri网的分布式实时嵌入式系统调度的建模

提出了一种基于资源的时间Petri网模型,以便建模分布式实时嵌入式系统中的静态调度,分析系统性能。该模型将处理器资源和通信资源,以及相应的优先级附着到变迁上,从而建模以下的分布式实时嵌入式系统：在单处理器上采用基于固定优先级的抢先式调度,处理器之间的通信采用基于固定优先级的不可抢先式调度。最后分析了该模型的语义、性质以及状态类图的构造方法。     

嵌入式系统建模理论与方法

嵌入式系统建模是目前一个新的研究热点。利用建模的结果可大大减少系统的设计时间,提高系统的设计质量。介绍了嵌入式系统建模的最新理论和方法,对这些方法进行了分类和比较,探讨了嵌入式系统建模的理论和方法发展趋势。     

基于颜色Petri网的交通信息网格系统建模与分析

交通信息网格系统以高性能计算网格环境为支撑平台,综合运用网格及Web服务技术提供交通信息服务。系统请求响应过程复杂且有功能复用,为了确保系统各响应流程设计的正确性,建立了基于颜色Petri网的分层描述模型,在模型基础上利用形式化方法验证了系统设计的正确性。     

基于UML的嵌入式系统建模及模型验证机制研究

统一建模语言UML在嵌入式系统设计建模中已经获得了广泛的认可,并有很多成功的应用,但UML存在时间约束描述能力不强和所建模型形式化复杂、验证难的问题。针对上述问题,本文提出了使用UML扩展机制对UML状态图进行时间扩展,建立系统状态一约束一事件矩阵来对模型进行形式化描述的方法。该方法解决了UML在嵌入式系统建模时存在的问题。应用实例和实验结果验证了该方法的可行性和有效性。     

面向对象的Petri网在嵌入式系统开发中的应用

介绍了面向对象的Petri网,提出了一个完整的、面向对象的、基于Petri网的嵌入式系统设计的建模方法,并给出了一个用OOPN对嵌入式系统建模的示例。     

一类混杂系统的建模与分析

提出一种广义Ｐｅｔｒｉ网，改进原有线性连续时不变ＳＩＳＯ系统的状态方程，并用它为一类混杂系统建模。同时提出一种混合状态，研究了该状态的演变规则、运行轨迹和状态方程。     

Modeling and analysis of scheduling for distributed real-time embedded systems

Aimed at the deficiencies of resources based time Petri nets (RBTPN) in doing scheduling analysis for distributed real-time embedded systems, the assemblage condition of complex scheduling sequences is presented to easily compute scheduling length and simplify scheduling analysis. Based on this, a new hierarchical RBTPN model is proposed. The model introduces the definition of transition border set, and represents it as an abstract transition. The abstract transition possesses all resources of the set, and has the highest priority of each resource; the execution time of abstract transition is the longest time of all possible scheduling sequences. According to the characteristics and assemblage condition of RBTPN, the refinement conditions of transition border set are given, and the conditions ensure the correction of scheduling analysis. As a result, it is easy for us to understand the scheduling model and perform scheduling analysis.     

基于Petri网的数字系统建模和VHDL实现

基于Petri网的数字系统的建模及其硬件实现方法已经得到了广泛的研究,然而现有的方法主要适用于同步电路,由此提出了一种基于Petri网的数字系统建模和VHDL实现的新方法。首先定义了一种广义同步自控网系统,解决了数字系统的Petri网建模问题。基于一种带优先级的多输入多时钟D触发器,设计了对应的软IP核,进而探讨了广义同步自控网系统模型到VHDL代码的具体转换方法。设计的CAD工具支持数字系统的建模、功能分析与代码转换功能。通过设计示例表明了所述方法和相关工具的有效性。     

嵌入式系统软件体系结构动态建模及应用研究

应用π演算方法,结合Petri网中的面向对象Petri网和时间Petri网,建立了嵌入式系统软件体系结构抽象模型ESAM,研究了ESAM模型的动态演化、一致性和死锁。应用ESAM抽象模型,对车站信号联锁控制器进行了建模与分析。     

Modeling and formal verification of embedded systems based on a Petri net representation

In this paper we concentrate on aspects related to modeling and formal verification of embedded systems. First, we define a formal model of computation for embedded systems based on Petri nets that can capture important features of such systems and allows their representation at different levels of granularity. Our modeling formalism has a well-defined semantics so that it supports a precise representation of the system, the use of formal methods to verify its correctness, and the automation of different tasks along the design process. Second, we propose an approach to the problem of formal verification of embedded systems represented in our modeling formalism. We make use of model checking to prove whether certain properties, expressed as temporal logic formulas, hold with respect to the system model. We introduce a systematic procedure to translate our model into timed automata so that it is possible to use available model checking tools. We propose two strategies for improving the verification efficiency, the first by applying correctness-preserving transformations and the second by exploring the degree of parallelism characteristic to the system. Some examples, including a realistic industrial case, demonstrate the efficiency of our approach on practical applications.     

基于Petri网的实时多智能体系统建模

给出基于Petri网的实时多Agent系统建模方法,它通过Petri网建立由接口模块、目标模块、计划模块、调度模块、知识库模块、环境模块、内部模块和控制模块组成的实时Agent模型,抽象和清晰地描述出实时Agent内部和外部特征。     

基于FPGA嵌入式系统的研究与应用

针对FPGA自身用户可编程的特性,分析了FPGA嵌入式系统的优势和应用领域,研究了利用FPGA实现嵌入式系统的基本原理和设计方法,重点探讨了其结构的转换难点.通过具体应用,分析了乘法累加驱动滤波器的实现原理和处理过程,设计了FPGA嵌入式系统的具体实现方式.     

Automating test generation for discrete event oriented embedded systems

A method for the automatic generation of test scenarios from the behavioral requirements of a system is presented in this paper. The generated suite of test scenarios validates the system design or implementation against the requirements. The approach proposed here uses a requirements model and a set of four algorithms. The requirements model is an executable model of the proposed system defined in a deterministic state-based modeling formalism. Each action in the requirements model that changes the state of the model is identified with a unique requirement identifier. The scenario generation algorithms perform controlled simulations of the requirements model in order to generate a suite of test scenarios applicable for black box testing. Measurements of several metrics on the scenario generation algorithms have been collected using prototype tools.     

基于层次颜色Petri网的交通紧急调度算法与建模

针对城市交通网络中紧急车辆在行驶区段中如何较快地到达终点的问题,提出了一种基于Petri网的交通紧急控制策略模型。利用Davidson函数中行驶时间与交通流之间的对应关系,得出紧急车辆在道路上的最短行驶时间,并将其作为权重,运用Dijkstrsa算法进行最短路径寻优;采用紧急信号灯控制策略对最短路径上的交叉口信号灯进行了调整,减少紧急车辆在交叉口的延滞时间,并运用Petri网理论,建立紧急车辆在交叉口的紧急信号灯控制模型。为了描述紧急信号灯控制策略的动态行为特性,将其各部分关键要素分别设计为相应的Petri网子模型。通过模型的一个仿真实例,进行了紧急控制策略与普通策略的实验对比,实验结果表明前者可以对紧急车辆的到达时间进行优化。