一种基于SysML/MARTE/pCCSL的信息物理融合系统协同建模方法

信息物理融合系统(Cyber-Physical Systems, CPS)是一个综合计算、网络和物理环境的多维复杂系统.针对这种异构系统的建模问题一直是人们研究的重点,但是,缺乏系统性的方法来建模CPS的特性,如异构性、不确定性、软硬协同和非功能属性(Non-Functional Properties, NFP)等.提出了一种基于SysML (System Modeling Language)/MARTE (Modeling and Analysis of Real-Time and Embedded Systems)/pCCSL (p Clock Constraint Specification Language)的协同建模方法,实现了从不同视角建模CPS的不同特征,包括系统的结构、行为、时钟约束和NFP.该方法的新颖性在于使用pCCSL规约各模型之间的交互和同步,显式地建模模型之间的逻辑一致性.同时,为了捕捉CPS的特性如随机行为和连续行为,扩展了一些SysML/MARTE的元模型.最后,给出了一个智能建筑的案例以展示所提出的协同建模方法的可用性.     

基于混成自动机的CPS行为建模与属性验证

系统实时性、安全性和可靠性等非功能属性是信息物理系统在诸多领域应用的关键因素。论文在分析CPS模型构建与分析验证中面临的挑战的基础上,提出了一种CPS行为建模与属性验证方法。该方法首先基于混成自动机对CPS的行为进行建模,然后将此模型转换为混合程序模型,最后在定理证明器KeYmaera中对HP模型的属性进行形式化验证。文中论述了行为模型描述语言的结构,建立了混成自动机模型与HP模型之间的转换规则,分析了模型转换的一致性。应用实例表明:该方法既能简单直观地描述CPS动态行为,又能对CPS的属性进行严格的形式化验证,且有效避免了形式化验证中的状态空间爆炸问题。     

基于模型组件技术的通用离散事件动态系统仿真模型

针对传统离散事件动态仿真软件可重用性差的缺陷，提出了基于组件技术的设计方法，给出了基于组件技术的离散事件动态系统通用的模型接口及原型实现，开发了类似Matlab的离散事件动态系统仿真环境，该仿真工具通过拖放创建模型，联线建立模型间逻辑联系，并在炼钢连铸车间物流仿真中得到了运用。该设计方法还可以推广到其他柔性制造系统的仿真应用中。     

一种验证软件演化过程行为的代数推导方法

针对现有软件过程验证主要以结构验证和性质验证为主,缺乏行为验证的不足,提出了一种验证软件演化过程行为的代数方法.该方法使用通信进程代数ACP对软件演化过程元模型EPMM进行扩展,提出软件演化过程元模型代数EPMM-A.针对EPMM建模产生的软件演化过程模型,一方面使用EPMM-A形式定义软件演化过程模型的行为规约,另一方面在其公理系统的支持下,基于等式推导验证软件演化过程模型的行为与行为规约是否一致,使行为验证方式从模型推导(非形式化)变为代数推导(形式化).为了说明代数推导的正确性,证明了软件演化过程元模型代数的公理系统具有可靠性.     

离散事件系统的一种分布式仿真算法

本文针对串行同步仿真方法及Chandy-Misra异步分布式仿真方法所存在的优缺点,采用折衷方案,提出了一种新的离散事件系统分布式仿真方法。这种方法首先将系统分解为N个子系统,它们分别在N个微处理机上基于串行事件驱动仿真方法进行仿真,而在各微处理机间存在着异步性。为了避免仿真死锁,引入了一中央控制器来协调子系统间的异步仿真。最后,建立了0-1整数规划模型以实现系统的最优分解。     

一种基于AOcontPN的信息物理系统建模方法

信息物理系统(CPS)是计算、控制和通信相融合的系统。现有的建模方法不能很好地实现其离散和连续混合的复杂行为。对此提出了一种基于面向方面连续Petri网的AOcontPN建模方法。依据CPS需求分析,将一些普遍存在的物理连续过程抽取出来,作为一个功能性的方面连续Petri网,织入到基本Petri网中。这样不仅解决了CPS系统中连续过程的行为分析、复用等问题,也使得整个系统可以使用离散系统的形式化方法来验证。     

基于CSP的进程行为取证方法研究

针对取证过程中所获取的进程异常行为,提出进程行为事件重建犯罪过程的方法.该方法使用CSP(通信顺序进程)理论来形式化描述具有威胁乃至破坏性的进程操作及进程间的通信,根据系统保存的进程行为记录建立进程通信状态模型,使用基于路径搜索的进程行为解释算法分析模型内所有可能的进程通信序列,形成进程通信行为规则,在排除不符合规则的通信序列的基础上,找到能够形成合理证据链的通信序列.通过案例分析进行了证据的形式化及CSP建模,给出了进程行为的具体分析解释和原型系统,验证该方法的可行性和有效性.     

基于混成自动机的车联网服务建模方法

针对汽车信息物理融合系统（CPS）软件的异构性、分布式等特点,提出一种车联网服务建膜方法.对混成自动机进行通信端口扩展,采用扩展的混成自动机作为形式化建模工具,从服务提供的角度,分别将待监测和控制的设备实体抽象为服务作为系统的基本组成单元.以汽车速度控制系统为例,说明该建模方法的有效性.     

离散事件模型的代数方法及其监控理论

有限状态机（ＦＳＭ）、Ｐｅｔｒｉ网、通信顺序进程（ＣＳＰ）和有限递归进程（ＦＲＰ）都是用来描述离散事件动态系统逻辑行为的，都可以化为一种代数形式。本文首先描述了构造离散事件模型的一般方法，然后讨论了在其上发展的监控理论。     

DoS攻击下CPS双重安全控制与通讯的协同设计

针对一类具有执行器故障与DoS攻击的CPS,基于边缘计算理念,并结合事件触发通讯机制,研究了CPS双重安全控制与通讯的协同设计问题.首先,基于边缘计算的资源分配,提出DETCS下的CPS双重安全控制架构,并把有限能量的DoS攻击转化为一种特殊的时延,在DETCS下建立了具有故障与攻击的闭环CPS模型;其次,借助时滞系统理论,通过构造适当的Lyapunov-Krasovskii泛函,利用仿射Bessel-Legendre等不等式,分别给出了DoS攻击下状态与故障估计鲁棒观测器、执行器故障和DoS攻击双重安全控制与通讯协同设计的方法;最后,通过对四容水箱系统的仿真验证了文中理论结果的有效性与可行性.     

一种形式化的构件模型框架

构件理论在软件工程领域正扮演着越来越重要的角色。为了规范化地描述和设计构件 ,提出了一种形式化的构件模型框架 ,利用偏序事件多集来表示构件的行为模式 ,取代了常用的形式语言表示法 ,使顺序进程控制的构件和并发控制的构件能够在该框架下得到一致的处理。论文关于构件模型、任务合同及系统模型的概念 ,结合构件完备性、服务可满足性和系统一致性的检验方法 ,可以直接被用于设计构件支撑环境的仿真算法。     

Mining Sensor Data in Cyber-Physical Systems

A Cyber-Physical System （CPS） integrates physical devices （i.e.,sensors） with cyber （i.e.,informational） components to form a context sensitive system that responds intelligently to dynamic changes in real-world situations.Such a system has wide applications in the scenarios of traffic control,battlefield surveillance,environmental monitoring,and so on.A core element of CPS is the collection and assessment of information from noisy,dynamic,and uncertain physical environments integrated with many types of cyber-space resources.The potential of this integration is unbounded.To achieve this potential the raw data acquired from the physical world must be transformed into useable knowledge in real-time.Therefore,CPS brings a new dimension to knowledge discovery because of the emerging synergism of the physical and the cyber.The various properties of the physical world must be addressed in information management and knowledge discovery.This paper discusses the problems of mining sensor data in CPS：With a large number of wireless sensors deployed in a designated area,the task is real time detection of intruders that enter the area based on noisy sensor data.The framework of IntruMine is introduced to discover intruders from untrustworthy sensor data.IntruMine first analyzes the trustworthiness of sensor data,then detects the intruders＇ locations,and verifies the detections based on a graph model of the relationships between sensors and intruders.     

社团生成结构的电力信息物理系统鲁棒性分析

随着传感器技术的快速发展,信息网与电网的深度融合,电力系统的智能化水平越来越高,但也面临着安全性、脆弱性等一系列问题.结合相互依存网络与介数负荷-容量级联故障模型,提出了包含电网、信息网孤岛运行的连锁故障仿真算法,主要研究了具有社团结构的电力信息物理系统(cyber physical system,CPS)鲁棒性,修正了传统的社团结构生成算法,使其能够生成不同规模社团且社团连接概率可调的无标度网络.采用提出的算法生成信息网和电网社团内部同配耦合的电力CPS模型,使用电网剩余节点比例为评估指标.研究了调度中心处于不同社团时全局连接概率、社团连接概率以及多个调度中心对电力CPS鲁棒性的影响.     

嵌入式软件组件模型的研究与设计

根据嵌入式系统及其应用的需求，分析了当前嵌入式软件组件技术的发展现状，设计一种新的嵌入式组件模型SECOM，给出了模型的组成元素及其形式化定义，并对组件组合进行详细的描述，同时，通过分析，总结了SECOM模型的多样性、语言无关性和可扩展性等优点，且指出下一步的工作目标。     

机床组件有限元分析前处理专家系统研究

根据机床组件有限元分析特点,结合人工智能和有限元商业软件ANSYS,建立了针对机床组件有限元前处理过程的专家系统.首先根据有限元软件的操作流程对专家系统的运行流程进行了设计.通过对专家经验、理论知识、设计手册等知识的搜集和分类,运用基于逻辑的规则知识表达模型,将其转换为专家系统知识库中的知识,对有限元前处理知识和结构化知识做了较为详细的描述.同时也对专家系统中知识的推理和计算过程以及知识库的动态更新过程进行了讨论.最后利用机床主轴挠度分析作为实例,进一步讨论和证明了该系统的适应性和可靠性.     

一种研究组件引用语义的动力系统方法

在组件和引用形式模型的基础上给出了组件集的拓扑空间结构，从而在组件并行递归引用形式语义的研究中引入一种新的基于拓扑动力系统的观点和方法，将其指称对象的存在性归结于一个动力系统的吸引子和泛函不动点，同时将引用过程描述为系统的轨迹．最后，用这种动态方法分析了一个非单调对称工作流模型的工作过程，得到了工作流的轨迹和终止状态集。     

考虑节点异质性和故障函数的电力信息物理系统风险传播模型

由于电力信息物理系统的耦合建模方法大多数依赖网络拓扑结构划分节点类型,未考虑节点信息的属性,同时也忽略了不同节点类型对风险传播的影响,削弱了对风险预测的能力。因此,提出了一种考虑节点异质性和故障函数的电力信息系统风险传播模型。首先对实际电力网络节点特性以及耦合性特点进行分析,结合节点异质性提出双网节点的表征方法,基于双网物理和逻辑依赖关系,设计了电力信息物理融合系统(cyber physical systems, CPS)表征模型。在此基础上,考虑双网状态交互影响的方向性及节点的依赖性,分析影响风险传播的因素,通过定义基于节点度的故障概率函数,构建了电力CPS风险传播模型。以合成网络和意大利真实数据所建立的耦合网络进行实验分析,证明模型的有效性。     

Optimal Component Types for the Design of Construction Processes

Within the project preparation phase, experienced professionals manually map design information onto process information with the aim to develop realistic and practical schedules. Unfortunately, the mapping itself is neither part of any underlying data model nor is it supported by current scheduling tools. As a consequence the process of setting up the data model for a schedule is still not supported formally. Huhnt and Enge described a modelling technique that addresses the missing linkage between design and process information[1]. The approach makes use of so called component types. These are template sub-processes that describe the fabrication procedure of typical building components. Decomposing the building into com-ponents and assigning a component type to each component allows for formal support while scheduling. Depending on the decomposition of the building into components and the complexity of the involved component types the specification effort differs. The question about optimal component types arises: Which layout of building components and component types results in minimal specification effort? This paper presents a branch and bound algorithm to determine optimal component types. For a given schedule, which has been modelled based on component types, all possible decompositions into sub-processes are determined. During the decomposition process the encountered configurations are compared. Those with minimal specifica-tion effort are registered. Theoretical and practical examples are examined and discussed.     

混合系统的形式化模型

混合系统是一种离散和连续构件融合在一起的反应系统,通常以微分方程为连续模型,以离散事件系统或自动机为离散模型。本文概述了目前几个重要的混合计算模型,并通过扩充公平转换系统ＦＴＳ,提出混合系统的一种新的计算模型－混合转换系统ＨＴＳ。