基于实时发布订阅模式的数控总线通信机制研究

在研究传统通信机制基础上,针对数控总线特点,本文提出一种新型基于实时发布订阅模式的数控总线通信机制.详细阐述该机制的核心部件消息中间件的设计过程,采用形式化方法对这种机制进行分析,构建出基于概率时间自动机的系统状态转换模型,最后通过模型验证器PRISM时该机制的稳定性与实时性进行了验证.结果表明该机制满足数控总线通信要求.     

基于扩展RED图的概率时间自动机可达性分析

RED图可以表示一个完整的时间自动机上的状态集,包括其连续时间部分和离散部分.在它基础上实现的模型检测工具RED,在时间自动机模型检测中表现出了优良的性能.另一方面,现有的概率时间自动机模型检测工具仍然使用不同的方法来分别表示概率时间自动机状态的连续时间和离散部分.我们在复用原始RED图的数据结构的基础上,对其做出了扩展,以令其支持概率状态的表达,同时保持其性能方面的优势.我们又为此实现了一个概率时间自动机可达性分析工具原型,并将其与两个概率模型检测工具（PRISM和Modest）就概率时间自动机可达性分析作实验对比,来评估该工具原型的性能.实验结果显示,我们的集成表示概率状态空间的方式,确实提高了概率时间自动机模型检测的时间效率和延展性.     

OWL-S过程模型的形式化描述与相容性分析

构建组合服务的形式化模型是对其进行验证的前提与基础,然而缺乏统一的构建框架使得建模过程变得难以把握且无法实现自动化。通过对确定型有限自动机的扩展,建立了用于描述OWL-S过程模型的有限迁移系统——服务过程自动机,为组合服务的形式化建模提供了统一框架和自动化基础。同时,通过分析服务过程自动机的可接受位置及其在组合过程中可能产生的约束,将相容性划分为三个等级,从而能够在不同强度的可靠性要求下进行组合服务的验证工作。     

概率时段演算的模型检验概述

在实际工程应用中,越来越多的系统表现出具有概率性等特征。作为对于此类实时系统的建模,概率时间自动机因为其能同时表示概率性、随机性和不确定性而被广泛采用。在对此类带概率性质的实时系统进行描述时,作为时段演算的一种扩展,概率时段演算被用来计算此类系统满足需求的概率。该文主要概述基于概率时间自动机的概率时段演算的模型检验主要步骤及其核心算法,其中模型检验的核心算法通过分别将前两者转换为区域图和概率分支时间逻辑来达成。     

物联网系统时间自动机建模的研究与应用

探讨基于时间自动机理论进行物联网系统建模和模型检测的理论、方法、工具和实践.对时间自动机的基础理论进行比较全面和精确的论述,完善部分概念及其精确的形式化定义.提出基于时间自动机理论进行建模的方法,并指出时间自动机理论研究对物联网系统建模的指导意义.介绍时间自动机的建模工具UPPAAL,说明基于UPPAAL建立时间自动机模型的建模、仿真和检测方法.结合物联网系统中一个经典的温度感知服务的系统需求、理论与实践相结合,进行温度感知管理系统时间自动机建模,并进行模型仿真与模型检测.实验结果表明,该系统能够正确感知温度,具有容错性且不会陷入死锁.     

概率时段演算的模型检验概述

在实际工程应用中,越来越多的系统表现出具有概率性等特征。作为对于此类实时系统的建模,概率时间自动机因为其能同时表示概率性、随机性和不确定性而被广泛采用。在对此类带概率性质的实时系统进行描述时,作为时段演算的一种扩展,概率时段演算被用来计算此类系统满足需求的概率。该文主要概述基于概率时间自动机的概率时段演算的模型检验主要步骤及其核心算法,其中模型检验的核心算法通过分别将前两者转换为区域图和概率分支时间逻辑来达成。     

使用时间化自动机形式化带有时间扩展的UML状态图

严格建模是嵌入式实时系统设计的核心技术，通过UMI。方法与形式化方法结合可以给严格建模提供很好的工具支持。时间化自动机(Timed Automata)是一种用于描述、验证实时系统的理论模型。文中提出了一种通过时间化自动机来形式化带有时间扩展的UML状态图的方法，这种方法为UMI。与形式化方法的结合构造了桥梁作用。带有时间扩展的UML状态图用于嵌入式系统动态模型的建模，从时间化自动机模型得到形式化规范将更容易。UML状态图的形式化分为两部分完成；层次状态图的平面化以及时间化自动机的构造。     

基于SMT的PTACTL限界模型检测方法

概率时间自动机是在时间自动机的基础上加上各个状态迁移的概率以后形成的一种扩展的时间自动机,能用来对基于时间的随机协议、容错系统等进行建模,具有很强的实用性。本文针对概率时间自动机给出一种基于SMT的限界模型检测方法来验证该模型下的PTACTL性质,该方法由基于SMT的限界模型检测算法演变而来,通过将迁移时间和迁移概率融入ACTL性质中,改变模型的编码以及待验证性质的编码方式来实现对性质的验证。通过2个实例说明检测过程的有效性和高效性。     

轨道交通联锁领域特定语言的形式化

作为轨道交通系统的核心子系统之一，对联锁系统进行形式化建模与分析，是保证其安全性的重要手段.形式化建模需要领域知识和形式化知识的结合，由于形式化知识难以掌握，领域专家在建模整个过程中都需要形式化专家的帮助.为了解决这个问题，针对联锁系统的故障随机性、行为实时性、构件可重用的特点，提出设计联锁领域特定语言IS-SDL描述具体的联锁系统的参数，并基于随机混成自动机模板自动生成联锁系统的形式化模型，以进一步在此基础上进行安全分析.首先对联锁系统模型进行分析，根据不同案例设计其领域特定语言；其次，确定联锁系统的系统模型的模板，包括环境构件模板和控制器模板，并举例抽取其随机混成自动机模板；在模板基础上定义系统模型生成过程，让领域专家可以通过领域特定语言，输入参数自动生成具体的随机混成自动机系统模型；最后以某站联锁系统为例，展示了基于模板的具体系统模型的生成过程，并通过基于系统模型的事故预测分析，证明了该方法的可行性与有效性.     

系统架构描述语言AADL的功能行为建模扩展

架构分析与设计语言(AADL)是一种用于描述复杂嵌入式系统体系架构的建模语言,被广泛用于安全关键系统建模与验证。AADL通过行为附件以状态机的形式对组件的内部行为建模。工业界中的复杂系统常使用层次自动机描述组件的功能行为,而行为附件中没有表达层次自动机的机制。针对这一问题,提出了AADL行为附件的层次化扩展——HBA。首先给出了HBA的形式语法,然后定义了HBA的操作语义。提出了HBA的元模型,并在OSATE环境中实现其文本和图形化编辑器。为了便于形式化验证,给出了HBA到时间自动机(TA)的转换规则,并基于模型检测工具UPPAAL进行形式化验证。最后,给出一个案例研究来验证所提方法的有效性。     

Web Service Composition Using a Deductive XML Rule Language

This paper describes a knowledge-based Web Service composition system, called SWIM, which is based on the Service Domain model. Service Domains are communities of related Web Services that are mediated by a single Web Service, called the Mediator Service, which functions as a proxy for them. When a requestor sends a message to the Mediator Service one or more of the related Web Services are selected to dispatch the message and the results returned are aggregated to a single answer to the requestor. Mediator Services can be further composed to more complex Mediator Services that combine several selection and aggregation algorithms among many heterogeneous web services. The system utilizes the X-DEVICE deductive XML rule language for defining complex algorithms for selecting registered web services, combining the results, and synchronizing the workflow of information among the combined web services in a declarative way. In the paper, we demonstrate the flexibility and expressibility of our approach for composing Web Services using several e-business examples, covering most of the workflow patterns found in a comprehensive workflow management system (van der Aalst et al., Distributed and Parallel Databases, vol. 14, no, 1, pp. 5–15, 2003).     

Mediator模型的SystemC代码自动生成

Mediator是一种基于组件的建模语言,该语言主要通过自动机和系统对模型进行描述。将Mediator语言描述的模型自动生成为可执行代码,可以避免编码过程中由于人为疏忽而造成的错误,从而提高编码的可靠性,同时缩短模型开发周期。介绍一种从Mediator模型到SystemC代码的自动生成工具,该工具旨在将基于特定平台的模型转换为能直接仿真运行的代码。首先对Mediator语言的语法语义进行分析,选择合适的SystemC代码组织形式,然后针对Mediator模型的每一个组成部分 设计生成规则,其中重点对类型生成、状态转移语句生成、同步语句的生成进行分析。最后,通过一个机器掉电检测系统说明该工具运行结果的正确性。     

Quantitative Analysis With the Probabilistic Model Checker PRISM

Probabilistic model checking is a formal verification technique for establishing the correctness, performance and reliability of systems which exhibit stochastic behaviour. As in conventional verification, a precise mathematical model of a real-life system is constructed first, and, given formal specifications of one or more properties of this system, an analysis of these properties is performed. The exploration of the system model is exhaustive and involves a combination of graph-theoretic algorithms and numerical methods. In this paper, we give a brief overview of the probabilistic model checker PRISM (www.cs.bham.ac.uk/~dxp/prism) implemented at the University of Birmingham. PRISM supports a range of probabilistic models and specification languages based on temporal logic, and has been recently extended with costs and rewards. We describe our experience with using PRISM to analyse a number of case studies from a wide range of application domains. We demonstrate the usefulness of probabilistic model checking techniques in detecting flaws and unusual trends, focusing mainly on the quantitative analysis of a range of best, worst and average-case system characteristics.     

Multi-agent Mediator architecture for distributed manufacturing

A generic Mediator architecture for distributed task planning and coordination has been developed using multi-agent paradigms. In this approach, agents function autonomously as independent computing processes, and dynamic virtual clusters coordinate the agent's activities and decision making. This coordination involves dynamically created coordination agents and resource agents concurrently. The Mediator architecture contains three levels of these coordination agents: the template mediator, the data-agent manager, and the active mediator. The template mediator is the top-level global coordinator. This agent contains both the templates and the cloning mechanism to create the successively lower-level agents. Task plans are decomposed successively into subtasks, which are allocated to dynamically created agent clusters coordinated through data-agent managers and active mediators. Coordination of agent activity takes place both among the clusters and within each cluster. The system dynamically adapts to evolving manufacturing tasks, with virtual agent clusters being created as needed, and destroyed when their tasks are completed. The mediator architecture and related mechanisms are demonstrated using an intelligent manufacturing scheduling application. Both the machines and the parts involved in this production system are considered as intelligent agents. These agents use a common language protocol based on the Knowledge Query Manipulation Language (KQML). The generic Mediator approach can be used for other distributed organizational systems beyond the intelligent manufacturing application it was originally developed for.     

Constructive model-based analysis for safety assessment

The aerospace industry still uses fault trees to perform reliability analysis. This is because fault-tree modeling and analysis (FTA) seems easier to practical engineers when compared with Markov models, even though FTA provides a weaker form of analysis. In this paper, we propose an automatic strategy for generating Markov-based models and corresponding analysis formulations, according to ARP 4761, directly from Simulink diagrams annotated with failure information. The generated Markov-based models are expressed in the formal language PRISM, and the analysis is carried out by the PRISM model checker. The strategy is compositional and based on a comprehensive set of translation rules from Simulink to PRISM. We briefly address soundness and completeness of the rules and, to illustrate the application of the strategy, we apply it to a classical avionics case study: an actuator control system.     

The development of OCPL, object conceptual prototyping language

This paper describes the development of OCPL (object conceptual prototyping language), an object–knowledge representation language. The language is based on CPL, conceptual prototyping language, developed at the Free University of Amsterdam. CPL has been extended to allow for the explicit representation of object-oriented constructs. These constructs include facilities for application system definition, generation and usage. A restricted use of the constraint model of CPL allows for systematic representation of events from which appropriate user interfaces can be generated. The paper describes OCPL and its relationship to CPL and related work. It also illustrates how the constraint model can be used to represent dynamics and provide intelligent user support.     

Model checking probabilistic social commitments for intelligent agent communication

Interaction among autonomous agents in Multi-Agent Systems (MASs) is a key aspect for agents to coordinate with one another. Social approaches, as opposed to the mental approaches, have recently received a considerable attention in the area of agent communication. They exploit observable social commitments to develop a verifiable formal semantics through which communication protocols can be specified. Developing and implementing algorithmic model checking for social commitments have been recently addressed. However, model checking social commitments in the presence of uncertainty is yet to be investigated.In this paper, we propose a model checking technique for verifying social commitments in uncertain settings. Social commitments are specified in a modal logical language called Probabilistic Computation Tree Logic of Commitments (PCTLC). The modal logic PCTLC extends PCTL, the probabilistic extension of CTL, with modalities for commitments and their fulfillments. The proposed verification method is a reduction-based model checking technique to the model checking of PCTL. The technique is based upon a set of reduction rules that translate PCTLC formulae to PCTL formulae to take benefit of existing model checkers such as PRISM. Proofs that confirm the soundness of the reduction technique are presented. We also present rules that transform our new version of interpreted systems into models of Markov Decision Processes (MDPs) to be suitable for the PRISM tool. We implemented our approach on top of the PRISM model checker and verified some given properties for the Oblivious Transfer Protocol from the cryptography domain. Our simulation demonstrates the effectiveness of our approach in verifying and model checking social commitments in the presence of uncertainty. We believe that the proposed formal verification technique will advance the literature of social commitments in such a way that not only representing social commitments in uncertain settings is doable, but also verifying them in such settings becomes achievable.     

基于OIM数据对象模型的数据交换系统研究

扩展了OIM对象代数,提出一种基于Java的OIM数据交换系统模型,充分利用OIM对象模型与面向对象语言的配合优势,使系统性能得到保证。系统采用面向服务的设计思想,数据交换流程遵从数据流管道模型,具有良好的可扩展特性。在某数字校园系统的具体应用证明了该数据交换系统的良好性能。