基于可能性混成自动机的CPS建模方法

陈　娜, 耿生玲, 李永明, 张胜礼,4

(1.青海师范大学 计算机学院,青海 西宁810008; 2. 陕西师范大学 网络信息中心,陕西 西安 710069;3. 陕西师范大学 计算机科学学院, 陕西 西安 710069;4.兴义民族师范学院 计算机科学系, 贵州 兴义 562400)

基于可能性混成自动机的CPS建模方法

陈娜1,2, 耿生玲1, 李永明3, 张胜礼3,4

(1.青海师范大学 计算机学院,青海 西宁810008; 2. 陕西师范大学 网络信息中心,陕西 西安 710069;3. 陕西师范大学 计算机科学学院, 陕西 西安 710069;4.兴义民族师范学院 计算机科学系, 贵州 兴义 562400)

摘要:针对环境中存在的不确定性因素对信息物理融合系统的影响，提出一种可能性混成自动机的信息物理融合系统建模方法。该方法以可能性混成自动机为建模工具，通过分析信息物理融合系统的体系结构，讨论衡量不确定性的可能性对信息物理融合系统软件运行时的动态影响。以汽车速度智能控制系统为例，说明该方法的有效性。

关键词:信息物理融合系统；可能性混成自动机；可能性CPS；建模

信息物理融合系统(Cyber-Physical Systems, CPS)是一种融合计算进程与物理进程复杂的嵌入式网络系统[1]。CPS将物理与计算进程相结合, 物理设备通过嵌入式系统和网络进行监测与控制, 利用反馈机制相互影响计算过程与物理过程[2-3], 有效地实现人与现实世界的交互控制，以及实现安全、可靠的反馈控制[4-5]。

CPS由传感器、执行器和控制器等组成, 属于复杂性的嵌入式系统, 系统中各组件具有自治性、异构性、并发性等特点, 且CPS软件具有开放性[6]。常用的CPS软件建模方法主要有Simulink/Stateflow和基于UML的方法，由于这些建模方法具有封闭性，目前仍面临着不确定性建模、管理和优化决策控制等方面的挑战。根据应用的特点与数据形式的多样性，已出现了多种不确定数据模型。基于概率的不确定时态数据模型，通过分析现有的不确定时态信息模型提出概率方法[7]；在概率分布技术和不确定数据聚类方法的基础上，对不确定数据的概率分布在离散域和连续域上建模[8]。但是，现实环境中仍存在许多问题不能满足概率模型的可加性，无法用概率模型进行建模。

考虑环境的不确定性对CPS软件运行动态验证的影响, 本文将可能性概念引入CPS软件系统, 探讨不确定性CPS建模与属性验证的方法。 拟通过一种可能性混成自动机模型用于CPS软件运行动态建模, 并给出该模型属性验证的描述语法。

1基本概念概述

1.1可能性迁移系统结构

可能性迁移系统结构主要用于解决实际生活中的非可加性问题，是研究不确定性问题的主要模型。可能性迁移系统结构定义如下。

定义1[9-10]可能性迁移系统结构为五元组M=(S,P,I,AP,L),其中

(1)S是可数非空状态集。

(4)AP是原子命题之集。

(5)L∶S→SAP是标签函数, 即在每个状态下都有一个赋值(AP的子集)。

若X∈[0,1],分别用∧X和∨X表示X的最小上界和最大下界。

1.2混成自动机

混成自动机结合了基于状态机的离散控制模型和基于经典微分方程表示物理活动的连续变化模型[11]，定义如下。

定义2[12]21-22设混成自动机为一个六元组HA=Loc,E,Var,Lab, act, inv。

(1)Loc为控制模式之集。

(2)E为边的有限之集,表示转换关系,E的元素e具有形式l,g,a,u,l′,其中的l∈Loc为源位置,g为保卫条件,a∈Lab为同步标签,u∈Var×Var为变量的更新关系，l′为更新后的位置。

(3)Var为实值变量的有限集,即Var={x1,x2,…,xn},其变量的个数也称为自动机的维度。

(4)Lab为同步标签之集, 同步标签也叫做事件。

(5) act为活动标记函数, 为混成自动机的每个位置标记一系列的活动, 活动通常用变量对时间的微分方程表示。

(6) inv为不变式标记函数, 赋予每个位置一个不变式。

混成自动机是一个封闭的智能体, 该系统反映了物理动态与离散变迁之间的相互存在关系[13-14]。CPS具有离散变迁与连续动态的行为, 既能描述真实世界的变化状况, 又能刻画系统的状态转移关系。

2可能性CPS软件扩展模型

CPS所处的环境具有不确定性, 而这些不确定性对CPS能否正确运行在一定程度上起着至关重要的作用。CPS中各组件并非完全孤立, 它们是相互联系的一个整体。 传统的嵌入式系统中软件与硬件高度融合, 但却具有封闭性, 因此不能单纯的使用嵌入式系统软件的建模方法对CPS软件进行建模[12]20-21。 本文在嵌入式系统的建模方法基础上, 将可能性概念引入经典的混成自动机表示不确定性, 定义可能性混成自动机网络结构模型。

2.1可能性混成自动机

定义3可能性混成自动机H表示为九元组H=L,E,Po,I,Var,Lab, act,inv,C。

(1)L为H中控制模式之集。

(2)E为边的有限之集,表示转换关系,E的元素e具有形式l,g,a,u,l′,其中的l∈L为源位置,g为保卫条件,a∈Lab为同步标签,u∈Var×Var为变量的更新关系,l′为更新后的位置。

(3)Po∶L×L→[0,1]是可能性转移函数,且对∀l∈L,都有∨l′∈LPo(l,l′)=1。

(4)I∶L→[0,1]是可能性初始分布函数,且对∀l∈L,都有∨l∈LI(l)=1。

(5)Var为实值变量的集合,即Var={x1,x2,…,xn},其中变量的个数n为H的维度。

(6)Lab为同步标签的集合,称为H中的事件。

(7) act为活动标记函数, 为混成自动机的每个位置标记一系列的活动, 活动通常用变量对时间的微分方程表示。

(8) inv为不变式标记函数, 赋予每个位置一个不变式。

(9)C为与H绑定的通信端口的有限集合

C={c1,c2,…,cn}。

此定义中的通信端口起到系统与外界环境进行通信的作用。通信端口的操作方式有两种,即读和写分别用”?”和”!”表示,ci?表示从端口i输入数据;ci!表示将数据输出到端口i。 定义为ci={pidi,datai,domi}, 其中pid、dom和data分别为端口i的唯一标识符、传送的数据和数据类型。数据类型包括integer, boolean, float或用户自定义。

2.2可能性CPS软件体系结构模型

2.2.1基于可能性混成自动机的CPS体系结构模型

CPS软件体系结构由设备服务层(感知层和执行层)、服务接口层和高级应用层3层组成, 如图1所示。服务接口层的功能体现系统通过与环境之间的相互影响, 如系统通过与传感器的交互感知环境状态变化, 及时实现对环境的监控。CPS软件涉及离散过程和连续过程的交互, 通过已定义明确的端口与外界环境进行通信并进行服务组合。

图1　CPS软件体系结构模型

(1) 设备类:DC=dcId, Attr, Dom, 其中dcId为设备类别的唯一标识符; Attr为设备类的相关属性的有限集合; Dom：Attr→DataType表示设备属性到数据类型的映射关系, DataType表示传送的数据类型。

(2) 设备实体:DE=deId,DC,DH, deId表示设备实体的标识符;DC表示与设备实体相关的设备类;DH表示设备实体动态行为的可能性混成自动机。

(3) 原子服务S=sId, dSet,SH表示, 其中sId是CPS软件服务的唯一标识符; dSet为设备实体类的集合;SH是描述服务动态行为的可能性混成自动机。

2.2.2基于可能性混成自动机的CPS体系结构建模

以可能性混成自动机的控制模式进行分析,利用可能线性时序逻辑公式(记为PoLTL)定义可能性CPS软件模型属性的形式化描述语言。

定义4可能性 CPS的PoLTL的语构定义为

φ∷=ture|a|φ1∧φ2,|φ|Oφ|φ1∪φ2,

其中a∈AP。

设可能性CPS软件模型为R,π为模型R的一条执行轨迹,φ为属性描述公式,则用‖φ‖(π)表示R的执行轨迹满足属性φ。其在R上的语义是Paths(R)的可能性,即‖φ‖R:Paths(R)→[0,1]。π表示整条已知的轨迹,π∈Paths(R)即π=s0s1s2…。用πj表示从第j步开始的轨迹的后缀,即πj=sjsj+1。变量y在π中第j步的值表示为V=(π,j,y)。

可能性CPS软件模型的执行轨迹p可表示为一个有穷或无穷的序列

s0,t0|→s1,t1|→…|→sn,tn|→…,

其中si=li,vi表示系统的状态,li表示系统所处的控制模式,vi表示系统当前的变量值。ti表示系统在状态si停留的时间。

定义5可能性CPS软件模型的PoLTL语义可解释为

‖a‖(πi)=L(si)(a)=y～v⟺V(π,i,y)～v;

‖φ∧γ‖(πi)=φ∧γ⟺πi|=φ且πi|=γ;

‖φ‖(πi)=1-‖φ‖(πi)⟺πi≠φ;

‖Oφ‖(πi)=‖φ‖(πi+1)⟺π[i+1,…]|=φ;

‖φ∪γ‖(πi)=φ∪γ⟺∃t>i,t∈N,s.t.πt|=γ,

且对于i

在可能性CPS软件模型R中,无穷路径表示为π=s0s1s2…∈Sω;有穷路径表示为π=s0s1…sn(n∈N)。用Paths(R)表示R中无穷路径之集,Pathsfin(R)表示有穷路径之集。

R中的状态的前驱Pref表示为

Pref(s)={s′∈S|P(s′,s)>0}

Pref*(s)={s′∈S|s∈Post*(s′)}

后继Post表示为

Post(s)={s′∈S|P(s,s′)>0};

Post*(s)={s″∈S|∃π=s0s1…sk,s0=s,sk=s″,

对于状态集B⊆S,

3实例分析

以汽车速度智能控制系统的应用为例, 运用可能性混成自动机建模方法, 对汽车速度控制子系统进行分析建模, 如图2所示。用户给发动机一个油门命令, 发动机得到命令输出转速给传动器后,将转速转化为驱动汽车运动的输出力矩。 传动器需要根据用户发出的油门命令和目前的车速及规则向传动器发出控制命令, 使得汽车的运行速度能够改变。

图2　汽车速度智能控制系统的应用场景

在汽车速度智能控制系统中的设备为执行设备、感知设备和控制设备, 各模块之间通过通信端口与外界环境进行通信。此处的通信端口分别为控制命令、油门和车速。

(1) 执行层建模

创建传动器类和传动服务。控制命令端口建模为cmd=(pcmd,c,c→{UP, DOWN, STOP}),

传动器

trans=(Transmission,{gear, cmd,u,n},

{retateSpeed,cmd},{tout},Dom),n为发动机的转速, gear为加速档,u为传动器的输出力矩，传动器到n、gear和u的映射关系分别表示为

Dom(u)=F+,Dom(n)=F+,Dom(gear)={1,2,3,4}。

传动服务TransService =(transService, {Trans}, TransH), TransH是描述传动器动态行为的可能性混成自动机，如图3(a) 所示。

(2) 感知层建模

a) 油门端口和油门感知服务

油门感知服务将油门状态发送到油门端口throttle=(pthrottle,x,x|→[0, 1]), 其中x∈[0, 1] 表示油门开起的程度。油门感知服务ThrottleService=(throttleSer-vice,{Throttle},ThrottleH) , ThrottleH是描述油门传感器动态行为的可能性混成自动机, 如图3(b)所示。

b) 车速感知服务

SpeedService=(speedService,{Vehicle},SH),SH是描述车速传感器动态行为的可能性混成自动机,如图3(c)所示。

(3) 控制层建模

传动器控制服务TransControllerService=(transControllerService, {Throttle, Trans, Speed},TCSH),TCSH是描述控制器动态行为的可能性混成自动机, 如图3(d) 所示。

考虑环境不确定性对汽车速度智能控制系统的影响,以驾驶员对汽车油门的操作为例, 当汽车在道路上行驶时, 路况是不确定的，驾驶员需要根据路况对汽车油门进行控制。

(4) 驾驶员对油门操作的不确定性操作建模

(a) 传动服务

(b) 油门感知服务

(c) 车速感知服务

(d) 传动器控制服务

(e) 驾驶员对油门的操作

4结束语

通过对CPS软件中的不确定性进行研究，定义了可能性混成自动机为形式化建模工具, 以PoLTL作为CPS软件属性的形式化描述语言, 描述CPS的体系结构模型及动态行为, 结合汽车速度智能控制子系统模型，说明该方法的有效性。下一步可能继续对可能性CPS软件中的属性进行动态验证分析研究。

参考文献

[1]LEE E . Cyber physical systems: design challenges [C]// Proceedings of 11th IEEE International Symposium on Object Oriented Real-Time Distributed Computing(ISORC),May 5-7,2008, Orlando, F L. Washington, D C: IEEE Xplore, 2008: 363-369. DOI: 10.1109/ISORC.2008.25.

[2]徐洪智, 李仁发, 曾理宁. 基于Ptolemy的信息物理融合系统建模与仿真[J]. 系统仿真学报, 2014, 26(8): 1633-1638.

[3]尹玲, 陈小红, 刘静. 信息物理融合系统的时间需求性分析[J]. 软件学报, 2014,25(2)：400-418. DOI: 10.13328/j.cnki.jos.004540.

[4]封飞, 陈名才, 张广泉, 等. 基于混成自动机的车联网服务建模方法[J]. 南通大学学报：自然科学版，2013, 12 (2) : 6-10.

[5]RAJKUMAR R, INSUP L, LUI S. Cyber-physical systems: the next Computing revolution [C]// Proceedings of 47th Design Automation Conference (DAC), June 13-18,2010, Anaheim, C A. New York: ACM, 2010:731-736.

[6]SISTLA A, ZEFRAN M, FENG Y. Runtime monitoring of stochastic cyber-physical systems with hybrid state[C]//2nd International Conference on Runtime Verification (RV 2011). San Francisco, CA, United states: Springer Verlag, 2012:276-293.

[7]任淑霞, 赵政. 基于概率的不确定时态数据建模与挖掘问题的研究[D]. 天津: 天津大学, 2013: 19-25.

[8]王建荣, 权义宁. 基于概率分布相似性的不确定数据聚类算法研究[D]. 西安: 西安电子科技大学, 2014: 7-13.

[9]李丽君, 李永明. 基于可能性测度的LTL模型检测[D]. 西安：陕西师范大学, 2012: 1-6.

[10]LI L J, LI Y M, Model-checking of Linear-time Properities in Possibilistic Kripke Structure[C]// Quantitative Logic and Soft Computing, Proceedings of the QL&SC 2012. Co. Pet. Ltd: World Scientific, 2012: 287-294.

[11]ALUR R. Formal verification of hybrid systems[C]//Proceedings of the Ninth ACM International Conference on Embed-ded Software(EMSOFT), Oct 9-14, 2011, Taipei. New York : ACM, 2011,12: 273-278.

[12]陈名才, 张广泉. 基于统计模型检测的CPS软件可信性验证研究[D]. 苏州: 苏州大学, 2014: 20-22.

[13]HENZINGER T. The theory of hybrid automata[C]//Proceedings of the 11th Annual IEEE Symposium on Logic in Computer Science(LUCS 96). Washington, D C:IEEE Computer Society, 1996: 278-292.

[14]赵文明, 张敏. 基于时空I/O混成自动机的物联网服务验证[J]. 科技通报, 2014, 30(5): 95-101.

[责任编辑：祝剑]

Modeling method of cyber-physical systems based on possibility mixed automaton

CHEN Na1,2,GENG Shengling2,LI Yongming3,ZHANG Shengli3

(1.College of Computer Science, Qinghai Normal University, Xining, Qinghai 810008, China;2. Network Information Center, Shaanxi Normal University, Xi’an, Shanxi 710069, China;3. College of Computer Science, Shaanxi Normal University, Xi’an, Shanxi 710069, China；4. Department of Computer Science, Xingyi Normal University for Nationalities, Xingyi, Guizhou, 562400, China)

Abstract:Due to the influence of uncertainty factors on cyber-physical systems (CPS) in the environment, a typical prototype of CPS architecture and possibility CPS modeling approach based on possibility mixed automaton is given in this paper. The systematic dynamic impaction of non-determined possibility on CPS software is discussed. The case of the vehicle speed control system is presented to show the validity of the modeling method.

Keywords:cyber-physical systems, possibility mixed automaton, possibility CPS, modeling

doi:10.13682/j.issn.2095-6533.2016.01.021

收稿日期：2015-11-10

基金项目：国家自然科学基金资助项目 (61261047); 国家社科基金资助项目 (15XMZ057); 青海省自然科学基金资助项目 (2014-Z-910, 2015-ZJ-718);贵州省教育厅自然科学研究重点资助项目(黔教合KY字[2015]408号)

作者简介：陈娜(1989-), 女,硕士研究生, 从事计算机智能信息处理研究。E-mail: 781698886@qq.com耿生玲(1970-), 女,教授, 博士, CCF会员(E20033713M), 从事计算理论, 数据挖掘, 控制与决策的研究。E-mail: gengsl@qhnu.edu.cn

中图分类号：TP391

文献标识码：A

文章编号：2095-6533(2016)01-0101-05