一种形式化的工作流网模型

提出基于Petri网的形式化的工作流网模型,用Petri分析技术对工作流业务流程的动态行为进行了描述和分析,并给出了详细的建模算法。     

基于带抑制弧的时延着色Petri网的嵌入式系统建模与验证

结合着色Petri网和时延Petri网,提出了一种适合于复杂嵌入式系统建模方法。该方法在库所中表示数据、控制信息和时间戳,在变迁中引入时延、控制函数与变迁函数,利用抑制弧简化模型。该方法可以对复杂的嵌入式系统进行建模,还可以利用现有的Petri网技术分析系统性质。通过实际案例展示了该方法的应用和可行性。     

基于价格时间Petri网的Web服务组合研究

Web服务以及其组合的服务质量是Web服务中的一个重要研究方向。采用价格时间Petri网为Web服务组合建模,利用计价状态类方法对模型的成本进行分析,得到最小成本。最后通过实例验证,用价格时间Petri网对Web服务组合的最小成本问题研究是可行的。     

混合状态Petri网及其在过程控制混杂系统中的应用

为了处理混杂系统的建模问题，提出了一种称为混合状态Petri网(HSPN)的混合Petri网，给出了HSPN的定义及其变迁规则。采用一个实际化工过程为例建立了HSPN模型，该模型可以用于混合控制器的设计，仿真结果表明了其有效性。本文还简要地讨论了HSPN的一些性质。     

一种基于Petri的服务组合测试模型和分析方法

测试用例选择是服务组合测试的重要内容,将直接影响服务测试的效率和正确性。采用Petri网分别对基本服务、组件和测试用例等组成部分建立形式化模型,进行形成整个服务组合的测试模型。基于模型的状态空间 分析测试 用例的选择和实施。借助Petri网的操作语义及相关理论,分析了该方法的有效性及正确性。具体实例结果表明：该方法能有效地简化服务组合的测试过程,有助于提高测试的质量和效率。     

分布式实时嵌入式系统的能耗建模与分析

为支持分布式实时嵌入式（DRE）系统的能耗分析,提出了一种能耗时延Petri网（ECTPN）对系统的模块、任务、任务间关系、通信协议等进行建模。基于所建DRE的ECTPN模型,分析系统的可调度性和能耗约束,并给出启发式算法来计算满足时间约束和能耗约束的可行调度。最后应用一个实例模拟系统的建模和分析过程,从而直观地展示了该方法的可行性。     

基于Petri网的嵌入式系统失效模型与分析

针对嵌入式系统的特点,提出一种基于Petri网的嵌入式系统失效模型与分析方法。依据嵌入式系统失效需求,采用Petri网建立嵌入式系统的形式化描述语言,并对嵌入式系统中的基本元素,如任务、资源、传感器、执行器等进行描述。构造任务间基本关系、任务与设备间交互的模型,并利用组合规则将这些模型动态地集成为一个完整的嵌入式系统失效模型。基于模型的运行特征和状态空间,分析模型的正确性。最后,应用具体实例模拟嵌入式系统失效模型与分析过程,验证了该方法的有效性。     

一种基于UML的面向方面模块动态特性编织方法

在面向方面软件开发Theme方法的基础上引入用例驱动技术,其中用例技术实现软件模块化,面向方面技术封装横切关注点,从而形成一种用例驱动的面向方面软件开发(UCD/Theme)方法。通过分析面向方面模块的动态特性在编织过程中可能产生的冲突,提出了一种扩展UML的面向方面模块动态特性编织时的冲突解决方法。通过ATM案例说明了该方法的应用。     

一种基于Object-Z的面向方面建模方法

提出一种基于Object-Z的形式化面向方面建模语言及其建模方法。方面规范提供了观察基本模块和方面模块的行为、描述它们相互关系的手段,编织机制将两类模块系统地集成为一个完整的系统模型。该方法能有效地简化系统建模,提高系统模型的可复用性,也为进一步验证系统性质提供了理论基础。     

电子商务系统主体行为的描述与分析

电子商务系统的主体行为对整个交易的安全非常重要。本文应用标注Petri网模拟技术,建立了电子商务系统中主体行为模型,解决了主体的责任分析、证据收集等与安全性有关的问题。     

基于扩展ITCPN的UML状态图建模

在ITCPN (Interval Timed Colored Petri Nets) 模型的基础上引入变迁条件函数和变迁数据操作函数,实现对UML状态图中数据计算的建模;利用抑止弧对迁移的优先级进行建模;同时借助抑止弧实现了对UML状态图中子状态之间“或”语义的建模。     

A Meta-Composite Software Development Approach for Translational Research

Translational researchers conduct research in a highly data-intensive and continuously changing environment and need to use multiple, disparate tools to achieve their goals. These researchers would greatly benefit from meta-composite software development or the ability to continuously compose and recompose tools together in response to their ever-changing needs. However, the available tools are largely disconnected, and current software approaches are inefficient and ineffective in their support for meta-composite software development. Building on the composite services development approach, the de facto standard for developing integrated software systems, we propose a concept-map and agent-based meta-composite software development approach. A crucial step in composite services development is the modeling of users’ needs as processes, which can then be specified in an executable format for system composition. We have two key innovations. First, our approach allows researchers (who understand their needs best) instead of technicians to take a leadership role in the development of process models, reducing inefficiencies and errors. A second innovation is that our approach also allows for modeling of complex user interactions as part of the process, overcoming the technical limitations of current tools. We demonstrate the feasibility of our approach using a real-world translational research use case. We also present results of usability studies evaluating our approach for future refinements.     

一种改进的基于案例推理的建模算法

基于案例推理的方法是一种基于知识获取的方法,也是一种新型的基于数据驱动的建模方法。基于案例推理的核心是案例检索。针对基于案例推理系统中案例检索工作,本文提出了一种改进的K最近邻回归建模算法。首先,基于聚类思想的最近邻回归算法可以实现对案例库的有效划分,从而提高案例检索质量;其次,针对K最近邻算法中邻居个数的选取问题,采用粒子群算法确定需要的邻居个数,取代传统的依靠经验确定邻居个数K的做法。通过对Mackey Glass混沌时间序列数据进行仿真预测,验证了该方法的可行性。     

LEMMA: A Language for Easy Medical Models Analysis

The quality of health care systems and processes is becoming a prominent problem and more and more efforts are devoted to define methodologies and tools to measure and assure quality of care. New methods are required to optimize health care processes to guarantee high quality standards within (limited) available resources. Resource optimizations able to preserve the quality of treatments require good models of medical processes. This paper presents LEMMA, a new notation to model medical processes. LEMMA provides physicians with intuitive graphical elements to design their models. At the same time a high level timed Petri net corresponding to the designed model is built automatically. In this way, LEMMA models are ascribed formal semantics and can be executed and analyzed automatically. The dual language approach followed in this paper allows physicians to gain all the benefits of formal methods without being proficient in them. Medical users manage simple graphical elements, while Petri nets ensure formality and validation capabilities. In this way LEMMA mixes formal and informal notations, overcoming the problems of both the approaches. The definition of the notation has been supported by the development of an environment to design LEMMA models. The environment, besides letting us experiment with the notation, has been employed to define and analyze real case studies.