复杂行为的语言支持

文中面向复杂行为的虚拟环境应用需求在分析比较当前几种有代表性的建模语言的基础上,提出一个支持复杂行为的语言模型,该模型可以灵活定义行为之间的控制关系及其时间约束,并给出了面向复杂行为的虚拟环境计算算法。     

虚拟实体对象建模语言SCPL

本文给出一种新的虚拟实体对象建模语言ＳＣＰＬ。这种语言以基于控制论的行为模型ＳＣＰ为中心组织虚拟实体对象的建模,具有实现连连续和更复杂行为的能力,适用领域广。     

半张量积理论在网络遥操作系统中的应用

研究了网络遥操作系统的半张量积建模问题.网络遥操作系统中存在人机交互以及大时延事件,这使得系统中既有离散事件动态又有连续动态,当系统的离散事件动态与底层连续动态相互作用耦合强烈时,系统的性能、行为分析变得更为复杂.本文通过引入半张量积给出了一种新的半张量积混杂建模方法,它把一类特定事件系统建模为布尔系统,通过半张量积方法得到类似于离散动态系统的方程.它将系统中离散事件和连续动态相互耦合的地方表达为半张量积的形式,最后经过扩张简化得到完整统一的系统数学模型,它将有利于进一步分析、计算.本文给出的半张量积建模方法和步骤具有一定的通用性和一般性.此外本文还对基于半张量积的混杂网络遥操作系统模型进行了基于事件控制和时间控制的仿真.仿真结果表明,半张量积建模方法完全可信、可行,基于事件控制的方法在网络遥操作控制中明显优于基于时间控制的方法.     

神光III控制系统的故障建模与分析

应用混合随机Petri网对神光III控制系统的故障进行了建模,并应用Visobj Net对建立的故障模型进行了仿真分析。网络化控制系统是一个离散和连续相结合的混合动态系统,具有动态、并发及同步等特征;神光III控制系统就是网络化控制技术在武器装备上的一个典型应用;对于复杂系统的建模和分析,Petri网是一个非常有效的工具。Petri网已经被证明是离散事件或异步系统很好的建模和分析工具,混合随机Petri网是Petri网的一个扩展,具有强大的建模功能。仿真结果表明,所建立的模型是正确的。     

不完备离散事件系统的可诊断性

在离散事件系统的建模过程中,由于系统行为的复杂,存在物理系统向逻辑系统映射的不完全性,因此产生了不完备模型的概念.提出在模型不完备的前提下,判断模型可诊断性的方法.提出可诊断性的在线判定方法,同时将不完备的行为加入模型,使模型完备.用经典的双树方法判断离线可诊断性,根据观测序列的时序及语言的前缀判断并处理不完备行为.提出判定不完备行为的方法,向模型中添加不完备行为,并根据不完备行为增量地在双树中判定在线可诊断性.通过在线的可诊断性判定,当前系统能够得到在有限观测内唯一判定故障发生与否的结论.该方法适用于具有离散性质的系统.     

AADL+: a simulation-based methodology for cyber-physical systems

AADL (architecture analysis and design language) concentrates on the modeling and analysis of application system architectures. It is quite popular for its simple syntax, powerful functionality and extensibility and has been widely applied in embedded systems for its advantage. However, it is not enough for AADL to model cyber-physical systems (CPS) mainly because it cannot be used to model the continuous dynamic behaviors. This paper proposes an approach to construct a new sublanguage of AADL called AADL+, to facilitate the modeling of not only the discrete and continuous behavior of CPS, but also interaction between cyber components and physical components. The syntax and semantics of the sublanguage are provided to describe the behaviors of the systems. What’s more, we develop a plug-in to OSATE (open-source AADL tool environment) for the modeling of CPS. And the plug-in supports syntax checking and simulation of the system model through linking with modelica. Finally, the AADL+ annex is successfully applied to model a lunar rover control system.     

Template languages for fault monitoring of timed discrete eventprocesses

This paper introduces a new framework for modeling discrete event processes. This framework, called condition templates, allows the modeling of processes in which both single-instance and multiple-instance behaviors are exhibited concurrently. A single-instance behavior corresponds to a trace from a single finite-state process, and a multiple-instance behavior corresponds to the timed interleavings of an unspecified number of identical processes operating at the same time. The template framework allows the modeling of correct operation for systems consisting of concurrent mixtures of both single and multiple-instance behaviors. This representation can then be used in online fault monitoring for confirming the correct operation of a system. We compare the class of timed languages representable by template models with classes of timed languages from timed automata models. It is shown that templates are able to model timed languages corresponding to single and multiple-instance behaviors and combinations thereof. Templates can thus represent languages that could not be represented or monitored using timed automata alone     

ASM-based formal design of an adaptivity component for a Cloud system

The request of formal methods for the specification and analysis of distributed systems is nowadays increasing, especially when considering the development of Cloud systems and Web applications. This is due to the fact that modeling languages currently used in these areas have informal definitions and ambiguous semantics, and therefore their use may be unreliable. Thanks to their mathematical foundation, formal methods can guarantee rigorous system design, leading to precise models where requirements can be validated and properties can be assured, already at the early stages of the system development. In this paper, we present a rigorous engineering process for distributed systems, based on the Abstract State Machines (ASM) formal method. We rely on the foundational notions of ASM ground model and model refinement to obtain a precise model for a client-server application for Cloud systems. This application has been proposed to tackle the problem of making Cloud services usable to different end-devices by adapting on-the-fly the content coming from the Cloud to the different devices contexts. The ASM-based modeling process is supported by a number of validation and verification activities that have been exploited on the component under development to guarantee consistency, correctness, and reliability properties.     

An experimental evaluation of a higher-ordered-typed-functional specification-based test-generation technique

HOTTest is a model based test automation technique of software systems based on models of the system described using HaskellDB. HaskellDB is an embedded domain specific language derived from Haskell. HOTTest enforces a systematic abstraction process and exploits system invariants for automatically producing test cases for domain specific requirements. Use of functional languages for system modeling is a new concept and hence HOTTest is subject to concerns of usability, like any other new technique. Also, the syntax and the declarative style of Haskell based languages make them difficult to learn. Similar concerns can be raised for HOTTest as it shares the same syntax with Haskell. In this paper we describe an experiment designed to study the usability of HOTTest and to compare it with existing model based test design techniques. The results show that HOTTest is more usable than the traditional technique and demonstrate that the test suites produced by HOTTest are more effective and efficient than those generated using the traditional model based test design technique. Editor: James Miller     

一种多机器人系统仿真平台的框架结构研究

针对多机器人系统实验平台造价高,硬件容易老化、损坏等问题,提出一种仿真平台实现模拟的框架结构。仿真平台基于客户机／服务器结构,利用内核模块管理其他功能模块,引入插件概念构造传感器插件有效的实现了传感器的模拟。实验证明其易用性与实用性。     

基于扩展混成Petri网的CPS无人车系统建模与分析

信息物理融合系统(Cyber-Physical System,CPS)是一个集计算系统、通信系统、感知系统、控制系统和物理系统于一体的复杂系统,其行为是一种由离散计算过程与连续物理过程深度融合并紧密交互的混成行为。针对这种特性,采用混成Petri网对CPS建模,并在此基础上添加时间约束,即对离散变迁关联一个延迟时间,对连续变迁关联一个激发速率函数,同时引入抑止弧和测试弧的概念以提高Petri网的表达能力,由此提出一种新的模型——扩展混成Petri网模型。然后,对CPS应用中无人驾驶车辆系统的躲避障碍物场景进行建模,将建立的模型按照一定的规则转化为与之对应的Simulink模型,并通过Matlab仿真对系统行为及属性进行分析。     

Modelica模型的序列化方法

Modelica是一种基于方程的陈述式建模语言,它具有面向对象、数组化表示、连续离散混合和可重用等多种特征,基于Modelica构建的模型和模型库通常规模庞大且结构复杂。编译Modelica模型的时间开销较大。本文从Modelica模型编译的角度出发,结合现有的序列化方法,提出以模型序列化来取代模型编译的部分工作,从而达到提升Modelica模型编译效率的目的。文中实现的Modelica模型序列化技术已在多领域物理系统建模与仿真平台MWorks中进行了验证与应用。     

混合动态系统中连续状态系统用离散事件系统描述的一致性

混合动态系统起因于离散事件系统用于监控连续状态系统的行。本文用抽象语言方法描述连续状态系统，研究状态离散事件系统描述的一致性。基于输入输出观点简要地 讨论了离散控制器综合。     

Reactive mode handling of flexible manufacturing systems

This paper deals with a new modeling approach for mode handling of flexible manufacturing systems (FMS). Based on a review of the modeling methods and the specification formalisms in the existing approaches, we show that the mutual benefit of functional modeling and synchronous languages is very convenient for mode handling problem. We start by introducing the context of our work and the basic concepts of the proposed modeling approach. Then we present the steps of functional modeling and we illustrate them through an example of a flexible manufacturing cell. Functional modeling is completed by generic behavioral specifications representing the states of a subsystem or the whole system. The specification method is modular, hierarchical and supports reuse concept. The established model is generic and well adapted to our control system context. Mode handling function role within the control system is then studied. This function enables a reactive update of the availability of the resources and functions and the transmission of high level control and reconfiguration orders.     

Simulation of systems with dynamically varying model structure

Hybrid systems are dynamical systems composed of components with discrete and continuous behavior. Some systems change their structure during simulation, or their components behavior is essentially changing. This “structural dynamics” can be described in some modeling languages but the corresponding hybrid simulators have more or less restrictions in handling models with dynamically varying structure. Some basic approaches for the simulation of such systems are discussed in the context of modeling languages and simulators.     

流体随机Petri网与混合Petri网的比较分析

流体随机Petri网和混合Petri网作为传统Petri网的拓展,可以建模离散成分和连续成分并存的混合系统,也可用于解决离散模型的状态空间爆炸问题.由于这两种建模机制远未发展成熟,分析比较它们的异同点有助于机制本身的进一步发展完善,有助于为特定的应用选择合适的建模方法.本文讨论了流体随机Petri网和混合Petri网的定义、连续标识、分析方法、以及相互转换的可能性.结论是这两种建模机制是互补的,各自适合于特定的应用场合.     

Languages and applications in hybrid modelling and simulation: Positioning of Chi

A widely used classification of modelling languages distinguishes the categories continuous time (CT), discrete event (DE), discrete time (DT), and hybrid. For a better insight into the many different hybrid languages, a classification of five categories (CT, CT+, DE, DE+, and CT/DE) is proposed. Each category is explained, together with many of the included languages, simulators, and the associated application fields. Special interest is given to the Chi language used for specification, simulation and real-time control of industrial systems. Its CT part is based on (conditional) DAEs, its DE part on Communicating Sequential Processes. The suitability of the language for DE, CT, and CT/DE modelling is illustrated by two cases.     

Hybrid Petri net based modeling for biological pathway simulation

Hybrid Petri net (HPN) is an extension of the Petri net formalism, which enables us to handle continuous information in addition to discrete information. Firstly, this paper demonstrates how biological pathways can be modeled by the integration of discrete and continuous elements, with an example of the λ phage genetic switch system including induction and retroregulation mechanisms. Although HPN allows intuitive modeling of biological pathways, some fundamental biological processes such as complex formation cannot be represented with HPN. Thus, this paper next provides the formal definition of hybrid functional Petri net with extension (HFPNe), which has high potential for modeling various kinds of biological processes. Cell Illustrator is a software tool developed on the basis of the definition of HFPNe. Hypothesis creation by Cell Illustrator is demonstrated with the example of the cyanobacterial circadian gene clock system. Finally, our ongoing tasks, which include the development of a computational platform for systems biology, are presented.