本发明公开了一种面向周期控制器的以模式为基础的信物融合系统建模及验证方法，所述方法包括：利用信物融合系统建模语言，分别构建抽象层面上的离散模式和连续模式，及具体层面上的离散控制流和连续控制流；结合上述获得的抽象层面和具体层面的建模模型，获得完整的信物融合系统模型，并以图形化方式表示；将上述获得的完整的信物融合系统模型中的变量、离散模式、连续模式、离散模式控制流、连续模式控制流按照翻译规则转换成混合自动机，进行形式化验证和性质分析。本发明方法能以图形化展示界面，方便用户的理解和建立模型，也为模型和高置信的形式化性质验证工具间建立有效的桥梁，节约信物融合系统模型的开发和高置信性质验证的时间和成本。
1.一种面向周期控制器的以模式为基础的信物融合系统建模及验证方法，其特征在于，所述方法包括以下步骤：步骤一、利用信物融合系统建模语言HHML，分别构建抽象层面上表示控制器及交互转移关系的离散模式和表示物理环境及交互转移关系的连续模式；步骤一中，所述抽象层面的建模在模式层进行，抽象地表示控制器和物理环境以及他们之间的交互转移关系，将复杂的系统交互模式宏观地表达出来；所述模式层是指抽象层面的信物融合系统，包含离散模式和连续模式；所述离散模式是指抽象层面的控制器及转移关系；所述连续模式是指抽象层面的物理环境及其转移关系；
步骤二、利用信物融合系统建模语言HHML，分别构建具体层面上表示控制逻辑的离散控制流和表示物理变化规律的连续控制流；步骤二中，所述离散控制流是指离散模式的具体控制逻辑；所述连续控制流是指连续模式的具体物理变化规律；所述控制逻辑包括赋值、采样、函数调用、跳过、发散、顺序执行、条件判断和循环；所述物理变化规律包括显式的微分方程及终止时的条件；所述终止时的条件包括代表控制器状态变化的离散条件和代表物理环境变化的连续条件；所述离散条件具体包括对离散变量的判断；所述连续条件具体包括对连续变量的判断；
步骤三、结合步骤一中获得的抽象层面的建模和步骤二中获得的具体层面的建模，获得完整的信物融合系统模型，并以图形化方式表示；所述信物融合系统模型定义为：HModel：：＝(Dictionary，Modes)，
Dictionary：：＝{var|var＝(name，arrti，type，initval)}，Modes：：＝(dModes，cModes)，
其中，HModel是混合模型，由字典Dictionary和模式Modes构成；所述字典包含变量var，构建模型时在字典中增删变量并初始化；所述变量var是一个四元组，name是变量名，arrti是变量的属性，type是变量的类型，initval是变量的初始值；所述模式由离散模式dModes和连续模式cModes构成，系统只能同时处于一个离散模式和一个连续模式；
步骤四、将步骤三中获得的完整的信物融合系统模型中的变量、离散模式、连续模式、离散模式控制流、连续模式控制流按照翻译规则转换成混合自动机，进行相关高置信的形式化验证和性质分析；步骤四中，所述HHML所建信物融合系统模型中的离散模式转换到混合自动机的规则如下：在HHML中，离散模式支持模式嵌套，在转换之前，离散模式必须被“扁平化”，扁平化的离散模式满足的条件如下：dmodes′＝{dm|dm.dflow≠empty∧dm∈dmodes}，
所述扁平化是指使简化后的离散模式都不包含子模式，除去了包含子模式的离散模式，并在转换过程中保持语义的一致性；其中，dmodes’表示扁平化后的离散模式集合，dm表示任意一个离散模式，dmodes表示原离散模式集合，dm.dflow≠empty表示任意一个离散模式的控制流不为空。
2.如权利要求1所述的方法，其特征在于，步骤三中，所述图形化表示以图形的方式描绘离散模式及其控制逻辑、离散模式间的转移关系、连续模式及其物理变化规律、连续模式间的转移关系。
3.如权利要求2所述的方法，其特征在于，所述离散模式dModes定义为：
dMode：：＝(name，period，(dflow|dModes)，dTrans)，dTran：：＝(dm，priority，dguard，dm′)，
dguard：：＝cond|Duration(cond，c)|After(cond，c)，其中，每个离散模式dMode是一个四元组，name表示离散模式的标签；period表示离散模式的周期，离散模式在一定的时间间隔内处理一系列的周期任务；dfiow和dModes分别表示离散模式的控制流和子模式，如果包含子模式，那么该离散模式就不含控制流，反之包含控制流，这使离散模式之间的控制关系和数据关系可以迭代嵌入；dTrans表示离散模式间转移关系的集合；所述子模式是指离散模式中内嵌的若干个离散模式；
所述转移关系dTran是一个四元组；其中，dm表示转移关系的源离散模式，priority表示转移关系的优先级，dguard表示离散模式转移条件，dm’表示转移关系的目标离散模式；
所述离散模式转移条件dguard，包括条件cond和时间谓词Duration(cond，c)和After(cond，c)；当条件cond连续c个周期被满足时，Duration(cond，c)为真；当条件cond被满足后第c个周期，After(cond，c)为真。
4.如权利要求3所述的方法，其特征在于，所述离散控制流dflow定义为：
dflow：：＝declare|stmts|dflow；dflow，
pstmt：：＝x：＝stmt|x←cv|callfunc|skip|⊥，
cstmt：：＝stmt；stmt|while cond do stmts|if cond then stmts else stmts，其中，dflow表示离散模式的执行任务和计算过程，包括局部声明declare、控制语句stmts和dfiow之间的组合；所述控制语句由原子语句pstmt和复合语句cstmt组成；所述原子语句包括以下类型：赋值x：＝stmt，连续变量抽样x←cv，函数调用call func，空语句skip和发散⊥；所述复合语句cstmt包含三种基本的控制结构，即顺序组合stmt；stmt、循环while cond do stmts和条件if cond then stmts else stmts。
5.如权利要求2所述的方法，其特征在于，所述连续模式cMode定义为：
cMode：：＝(name，cflow，cTrans)，
cTran：：＝(cm，priority，cguard，cm′)，
其中，每个连续模式cMode是一个三元组，name表示连续模式的标签；cflow表示连续模式的变化规律，用微分方程表示；cTrans表示连续模式间转移关系的集合；
所述转移关系cTran是一个四元组；其中，cm表示转移关系的源连续模式，priority表示转移关系的优先级，cguard表示连续模式转移条件，cm’表示转移关系的目标连续模式；
所述连续模式转移条件cguard，包括条件cond和谓词When；连续模式转移条件区别于离散模式转移条件，同时连续模式将始终等待控制器的控制命令，一旦连续模式转移条件满足，将立刻发生连续模式间的转移。
6.如权利要求5所述的方法，其特征在于，所述连续控制流cflow定义为：
eq：：＝der v＝expr|eq||eq|Idel，
所述连续控制流cflow由微分方程eq和终止时的条件until cond构成，条件cond是对离散变量和连续变量的判断，当条件cond被满足时，连续模式中的控制流将会停止执行，但不一定会转移到其它连续模式；当连续模式转移条件被满足后，连续控制流才发生转移；所述连续转移条件是指cguard；
所述微分方程eq使用显式的常微分方程der v＝expr来表达变化规律；所述eq是一个或多个微分方程的组合；其中Idle是一种特殊情况，表示连续变量保持不变。
7.如权利要求1所述的方法，其特征在于，步骤四中，转换目标‑混合自动机以一个六元组表示，所述六元组具体为，(loc，var，inv，flow，jumps，init)，
其中，loc表示连续状态的有限集合，var表示变量集，inv表示每个连续状态的不变式的集合，flow表示连续状态控制流的集合，jumps表示自动机发生跳转的集合如下所示，每个jump是一个四元组，init表示连续变量的初始化；jumps的一般化表示如下所示：jumps：：＝{jump|jump＝{lbegin，lend，guard，reset}}，其中，lbegin表示混合自动机跳转的源状态，lend表示混合自动机跳转的目标状态，guard表示跳转的条件，reset表示跳转过程中对变量进行的更新操作；和/或，步骤四中，所述HHML所建模型中的变量转换到混合自动机的规则可以表示如下：
Tr(v)＝(‑，var∪v，‑，‑，‑，init∪v.inival)，
其中，HHML中的变量分为连续变量、离散变量和常数，变量类型包括整型、浮点型和布尔型，而混合自动机中的变量统一为浮点型的连续变量，布尔变量将转换为1/0，其他变量转换为浮点型；将这些变量直接转化为混合自动机中的连续变量；常量以实际值的形式转换到混合自动机中；在HHML中变量赋初值inival，对应于混合自动机中的初始变量init；Tr(v)表示所建模型中的变量转换到混合自动机的规则，v表示被转换的变量；“‑”表示没有改变的元素；
由于混合自动机中没有离散模式，所以在var中加入了离散模式的名称作为变量，由于混合自动机支持的变量类型为整形和浮点型，故用特殊值1/0标志来区分系统是否处于离散模式；最后还加入了时间项t来记录离散模式的周期，并令其初始值为0。
8.如权利要求1所述的方法，其特征在于，loc是混合自动机连续状态的集合，考虑到不同的连续状态都可以接收控制器的指令，因此每一个连续状态都需要包含同样的离散模式；转换规则设定自动机中某一连续状态l∈loc，其他状态相同；
Tr(dm)＝(‑，‑，‑，flow∪t′，jumps∪jps，‑)，
where jps＝{jp|jp＝(l，l，(t≥dm.period；dm.name＝＝1；dguard)，(dm.name＝0；dm′.name＝1；dm′.dflow；t＝0))，
∧(dm，‑，dguard，dm′)∈dm.dTrans}，
为了转换离散模式的周期并表示时间的变化，规则将时间的变化速度t’添加到自动机的每个flow中；条件t≥dm.period附加到自动机发生转移的卫士条件上，当发生转移时，时间整型变量t将被初始化，重置为0以表示周期的结束，即令t＝0；dm.name＝＝1表示判断系统当前处于哪个离散模式，即判断变量name是否为1，若为1，则处于dm模式，若不为1则不处于dm模式；然后将离散模式的转移条件dguard转换为guard；一旦发生转移，目标模式的离散控制流dm’.dflow将会被执行，并且当前所处的离散模式将由dm变为dm’，即令dm.name＝
0，dm’.name＝1；由于连续模式之间没有发生转移，因此目标连续状态仍然是源连续状态1；
规则中的单等号表示定义、赋值；双等号表示判断两边是否相等；
上述规则中，Tr(dm)表示翻译离散模式的规则，dm表示被翻译的离散模式，flow表示混合自动机控制流的集合，t’表示时间的变化速度，jumps表示混合自动机迁移关系的集合，jps表示转换后新增的迁移关系的集合，jp表示迁移关系集合jps中的某一条关系，1表示混合自动机中的某一状态，dm.period表示离散模式的周期，dm.name表示离散模式的标签，dguard表示离散模式的迁移条件，dm’表示迁移的目标离散模式，dm’.name表示目标离散模式的标签，dm’.dflow表示目标模式的控制流，dm.dTrans表示离散模式dm的转移关系集合；
Tr(dm)＝(‑，‑，‑，flow∪t’，jumps∪jps，‑)，
where jps＝{jp|jp＝(l，l，t≥dm.period；dm.name＝＝1，dm.dflow；t＝0}，该规则表示当离散模式不发生转移时，执行dm.dflow，在周期结束时进入下一个周期；
9.如权利要求1所述的方法，其特征在于，步骤四中，所述HHML所建信物融合系统模型中的离散控制流转换到混合自动机的规则如下：对于离散控制流中的条件语句if cond then stmt1 else stmt2，设置如下规则：Tr(cd)＝(‑，‑，‑，‑，jumps∪jps，‑)，
即包含条件语句的离散控制流dflow将被一分为二，并在jps分别用stmt1和stmt2来替换，转移条件分为条件cond和条件 其中，条件cond表示判断条件，stmt1表示条件成立时执行的操作，条件 表示该判断条件不成立，stmt2表示条件不成立时执行的操作，Tr(cd)表示翻译条件语句的规则，cd表示被翻译的条件语句，jumps表示混合自动机中迁移关系的集合，jps表示混合自动机中新增的迁移关系的集合，1表示混合自动机的某一状态；
Tr(Duration(cond，c))＝(‑，var∪cnt，‑，‑，jumps∪jps，init∪cnt＝0)；
Tr(After(cond，c))＝(‑，var∪cnt，‑，‑，jumps∪jps，init∪cnt＝0)；
where jps＝(‑，‑，cnt≥c，‑)∪(‑，‑，cond，cnt＝cnt+1)∪(‑，‑，cnt＞0，cnt＝cnt+
以上两条规则均引入了一个额外的计数变量cnt；在Duration中，当离散模式的一个周期结束时，如果cond为真，cnt将增加1，否则将重置为0；当cnt≥c时，Duration(cond，c)的表达式为真；同样，对于After(cond，c)，当cond为真或cnt＞0，cnt将在周期结束时增加1，当cnt≥c时，表达式为真；其中，条件cond为判断条件，c表示时间谓词所需满足的周期数，var表示变量集合，cnt表示一个用来计数的变量，jumps表示混合自动机中迁移关系的集合，jps表示混合自动机中新增的迁移关系的集合，init表示混合自动机中初始变量的集合。
10.如权利要求1所述的方法，其特征在于，步骤四中，所述HHML所建信物融合系统模型中的连续模式及其控制流转换到混合自动机的规则如下：Tr(cm)＝(loc∪cm.name，‑，inv∪cm.cond，flow∪cm.eq，jumps∪cm.cguards，‑)，混合自动机的连续状态和HHML的连续模式在语义上是等价的，执行一对一的转换；连续模式的名称name只需转换为标签loc；微分方程eq转化为自动机控制流flow中的微分方程；until后的条件cond转化为自动机中的不变式inv；连续模式间的转移cTrans等价于混合自动机中的跃迁jump行为，且在跃迁过程中不执行任何重置操作；其中，loc表示混合自动机中状态的集合，cm.name表示所建模型中连续模式cm的标签，inv表示混合自动机中不变式的集合，cm.cond表示离散模式微分方程终止时的条件，flow表示混合自动机控制流的集合，cm.eq表示微分方程，jumps表示混合自动机的迁移关系的集合，cm.guards表示连续模式间迁移条件的集合。
一种面向周期控制器的以模式为基础的信物融合系统建模及
验证方法
技术领域
[0001] 本发明属于可信软件、智慧城市和航空航天技术领域，涉及一种面向周期控制器的以模式为基础的信物融合系统建模及验证方法。
背景技术
[0002] 信物融合系统是由连续动力学和离散动力学组成的动态系统，连续部分通常对物理环境的相互作用进行建模，离散部分通常对控制系统的运行进行建模。计算和控制的结合可以导致非常复杂的系统设计，因此它们经常出现在航空航天、汽车工业和工厂自动化设计等领域。在航空航天领域，嵌入式软件及其运行环境具有高复杂性、不确定性和高实时性要求的特点。这就要求建模语言必须能够描述系统和环境的不同组成部分，能够深入刻画嵌入式软件的模型特征，能够组合表达多种交互模式。航天器的控制器一般设计成周期模块，对物理环境的进化进行监控，并对时间具有较强的敏感性。由于这种周期控制器的计算和控制组合较为复杂，对系统设计的安全性要求也很高，因此如何对其建模并进行形式化分析仍然是一个巨大的挑战。
发明内容
[0003] 为了解决现有技术存在的不足，本发明的目的是提供一种面向周期控制器的以模式为基础的信物融合系统建模及验证方法，以对信物融合系统进行建模并进行高置信的形式化分析。本发明提出的信物融合系统建模方法可以在模式层对信物融合系统进行抽象层面的建模，抽象地表示控制器和物理环境以及他们间的交互转移关系，将复杂的系统交互模式宏观地表达出来，使得工程师能够高效地理解和分析系统需求并建模，以便发现需求中是否存在不一致或不明确的地方；其次，每个离散模式都包含离散控制流来构建控制器具体的控制逻辑，每个连续模式都包含连续控制流来构建环境具体的物理变化规律。抽象和具体层面建模的结合构成了完整的信物融合系统建模，并容易以图形化的方式表示出来。本发明将信物融合系统建模模型转换成混合自动机的方法，提供了连接HHML和信物融合系统高置信的验证工具的桥梁，在此基础上可以进行相关高置信的形式化验证和性质分析。
[0004] 本发明提供了一种面向周期控制器的以模式为基础的信物融合系统建模及验证方法，所述方法包括以下步骤：
[0005] 步骤一、利用信物融合系统建模语言HHML，分别构建抽象层面上表示控制器及交互转移关系的离散模式和表示物理环境及交互转移关系的连续模式；
[0006] 步骤二、利用信物融合系统建模语言HHML，分别构建具体层面上表示控制逻辑的离散控制流和表示物理变化规律的连续控制流；
[0007] 步骤三、结合步骤一中获得的抽象层面的建模模型和步骤二中获得的具体层面的建模模型，获得完整的信物融合系统模型，并以图形化方式表示；
[0008] 步骤四、将步骤三中获得的完整的信物融合系统模型中的变量、离散模式、连续模式、离散模式控制流、连续模式控制流按照翻译规则转换成混合自动机，进行相关高置信的形式化验证和性质分析。
[0009] 步骤一中，所述抽象层面的建模在模式层进行，抽象层面的建模可以抽象地表示控制器和物理环境以及他们之间的交互转移关系，将复杂的系统交互模式宏观地表达出来；所述模式层是指抽象层面的信物融合系统，包含离散模式和连续模式；所述离散模式是指抽象层面的控制器及转移关系；所述连续模式是指抽象层面的物理环境及其转移关系。
[0010] 步骤二中，所述离散控制流是指离散模式的具体控制逻辑；所述连续控制流是指连续模式的具体物理变化规律；所述控制逻辑包括赋值、采样、函数调用、跳过、发散、顺序执行、条件判断和循环等；所述物理变化规律包括显式的微分方程及终止时的条件；所述终止时的条件包括代表控制器状态变化的离散条件和代表物理环境变化的连续条件；所述离散条件具体包括对离散变量如信号、开关等的判断；所述连续条件具体包括对连续变量的判断。
[0011] 步骤三中，所述图形化表示以图形的方式描绘离散模式及其控制逻辑、离散模式间的转移关系、连续模式及其物理变化规律、连续模式间的转移关系等。
[0012] 本发明中信物融合系统模型的文法定义如下：
[0013] HModel：：＝(Dictionary，Modes)
[0014] Dictionary：：＝{var|var＝(name，arrti，type，initval)}
[0015] Modes：：＝(dModes，cModes)
[0016] 其中，HModel是混合模型，由字典Dictionary和模式Modes构成。所述字典包含变量var，构建模型时可以在字典中增删变量并初始化。所述变量var是一个四元组，name是变量名，arrti是变量的属性，type是变量的类型，initval是变量的初始值。所述模式由离散模式dModes和连续模式cModes构成，系统只能同时处于一个离散模式和一个连续模式。
[0017] 所述离散模式表示抽象层面的控制器以及转移关系，一个离散模式dMode的文法定义如下：
[0018] dMode：：＝(name，period，(dflow|dModes)，dTrans)
[0019] dTran：：＝(dm，priority，dguard，dm′)
[0020] dguard：：＝cond|Duration(cond，c)|After(cond，c)
[0021] 一个离散模式dMode是一个四元组，其中name表示离散模式的标签；period表示离散模式的周期，这让离散模式可以在一定的时间间隔内处理一系列的周期任务；dflow和dModes分别表示离散模式的控制流和子模式，如果包含子模式，那么该离散模式就不含控制流，反之包含控制流，这使离散模式之间的控制关系和数据关系可以迭代嵌入；dTrans表示离散模式间转移关系的集合。所述子模式是指离散模式中内嵌的若干个离散模式。
[0022] 对于某一条转移关系dTran，也是一个四元组。其中dm表示转移关系的源离散模式，priority表示转移关系的优先级，dguard表示离散模式转移条件，dm’表示转移关系的目标离散模式。
[0023] 对于离散模式转移条件dguard，它可以是基本的条件cond(布尔条件)，也是可以时间谓词Duration(cond，c)和After(cond，c)。当条件cond连续c个周期被满足时，Duration(cond，c)为真。当条件cond被满足后第c个周期，After(cond，c)为真。例如：
[0024] Duration(x＞1，3)
[0025] 表示在某个周期t时满足x＞1，并在接下来的t+1、t+2均满足x＞1，则在第t+3个周期时，Duration(x＞1，3)被满足。
[0026] After(x＞1，3)
[0027] 表示在某个周期t时满足x＞1，则在第t+3个周期时，After(x＞1，3)被满足。
[0028] 所述离散控制流用来表示控制器具体层面的计算过程和控制逻辑，离散控制流dflow的基本文法定义如下：
[0029] dflow：：＝declare|stmts|dflow；dflow
[0030] stmts：：＝pstmt|cstmt
[0031] pstmt：：＝x：＝stmt|x←cv|call func|skip|⊥
[0032] cstmt：：＝stmt；stmt|while cond do stmts|if cond then stmts else stmts[0033] 其中，dflow表示离散模式的执行任务和计算过程，它包括局部声明declare、控制语句stmts和dflow之间的组合。所述控制语句由原子语句pstmt和复合语句cstmt组成。原子语句有以下几种类型：赋值x：＝stmt，连续变量抽样x←cv，函数调用call func，空语句skip和发散⊥。复合语句cstmt包含三种基本的控制结构，即顺序组合stmt；stmt、循环while cond do stmts和条件if cond then stmts else stmts。
[0034] 所述连续模式表示抽象层面周期控制器所处的物理环境及转移关系，一个连续模式cMode的文法定义如下：
[0035] cMode：：＝(name，cflow，cTrans)
[0036] cTran：：＝(cm，priority，cguard，cm′)
[0037] cguard：：＝When(cond)
[0038] 一个连续模式cMode是一个三元组，其中name表示连续模式的标签；cflow连续模式的变化规律，用微分方程表示；cTrans表示连续模式间转移关系的集合。
[0039] 对于某一转移关系cTran，是一个四元组。其中cm表示转移关系的源连续模式，priority表示转移关系的优先级，cguard表示连续模式转移条件，cm’表示转移关系的目标连续模式。
[0040] 对于连续模式转移条件cguard，它由条件cond和谓词When一同构成。一方面，这使连续模式转移条件区别于离散模式转移条件，另一方面，这表示连续模式将始终等待控制器的控制命令，一旦连续模式转移条件满足，将立刻发生连续模式间的转移。
[0041] 所述连续控制流cflow描述了物理世界在连续模式下的具体层面的物理变化规律，连续控制流cflow的文法定义如下：
[0042] cflow：：＝eq until cond
[0043] eq：：＝der v＝expr|eq||eq|Idel
[0044] 所述连续控制流cflow由微分方程eq和终止时的条件until cond构成，条件cond可以是对离散变量和连续变量的判断，当条件cond被满足时，连续模式中的控制流将会停止执行，但不一定会转移到其它连续模式；当连续模式转移条件被满足后，连续控制流才发生转移；所述连续转移条件是指cguard。
[0045] 微分方程eq使用显式的常微分方程der v＝expr来表达变化规律。eq可以是一个或多个方程的组合，其中Idle是一种特殊情况，表示连续变量保持不变。
[0046] 步骤四中，将HHML所建信物融合系统模型中变量转换到混合自动机的规则如下所述：
[0047] 本发明以一个六元组来表示转换目标‑混合自动机，所述六元组具体为，[0048] (loc，var，inv，flow，jumps，init)
[0049] 其中，loc表示连续状态的有限集合，var表示变量集，inv表示每个连续状态的不变式的集合，flow表示连续状态控制流的集合，jumps表示自动机发生跳转的集合，每个jump是一个四元组如下所示，init表示连续变量的初始化。
[0050] jumps：：＝{jump|jump＝{lbegin，lend，guard，reset}}，
[0051] 其中，lbegin表示混合自动机跳转的源状态，lend表示混合自动机跳转的目标状态，guard表示跳转的条件，reset表示跳转过程中对变量进行的更新操作。
[0052] HHML所建模型中的变量转换到混合自动机的规则可以表示如下：
[0053] Tr(v)＝(‑，var∪v，‑，‑，‑，init∪v.inival)
[0054] 其中，HHML中的变量分为连续变量、离散变量和常数，变量类型包括整型、浮点型和布尔型，而混合自动机中的变量一般统一为浮点型的连续变量。因此，布尔变量将转换为1/0，其他变量转换为浮点型。然后将这些变量直接转化为混合自动机中的连续变量。为了减少转换变量的数量，常量将会以实际值的形式转换到混合自动机中。在HHML中变量赋初值inival，对应于混合自动机中的初始变量init。Tr(v)表示所建模型中的变量转换到混合自动机的规则，v表示被转换的变量；用“‑”表示没有改变的元素。
[0055] 由于混合自动机中没有离散模式，所以在var中加入了离散模式的名称作为变量，由于混合自动机支持的变量类型为整形和浮点型，用1/0标志来区分系统是否处于离散模式。最后还加入了时间项t来记录离散模式的周期，并令其初始值为0。
[0056] 步骤四中，将HHML所建信物融合系统模型中的离散模式转换到混合自动机的规则如下所述：
[0057] 在HHML中，离散模式支持模式嵌套，即它可能包含几个子模式，而混合自动机中却不支持。所以在转换之前，离散模式必须被“扁平化”，即简化后的所有离散模式都不包含子模式，并在转换过程中保持语义的一致性。扁平化的离散模式满足的条件如下：
[0058] dmodes′＝{dm|dm.dflow≠emplty∧dm∈dmodes}
[0059] 它表示扁平化后的离散模式都不包含子模式，除去了包含子模式的离散模式，并在转换过程中保持语义的一致性。其中，dmodes’表示扁平化后的离散模式集合，dm表示任意一个离散模式，dmodes表示原离散模式集合，dm.dflow≠empty表示任意一个离散模式的控制流不为空。
[0060] loc是混合自动机连续状态的集合，考虑到不同的连续状态都可以接收控制器的指令，因此每一个连续状态都需要包含同样的离散模式。转换规则中以自动机中某一连续状态1∈loc为例，其他状态相同。下面规则表示一个周期后离散模式发生了转移。
[0061] Tr(dm)＝(‑，‑，‑，flow∪t′＝1，jumps∪jps，‑)
[0062] where jps＝{jp|jp＝(l，l，(t≥dm.period；dm.name＝＝1；dguard)，[0063] (dm.name＝0；dm′.name＝1；dm′.dflow；t＝0))
[0064] ∧(dm，‑，dguard，dm′)∈dm.dTrans}
[0065] 为了转换离散模式的周期并表示时间的变化，规则将时间的变化速度t’＝1添加到自动机的每个flow中。条件t≥dm.period附加到自动机发生转移的卫士条件上，当发生转移时，时间整型变量t将被初始化，重置为0以表示周期的结束，即令t＝0。dm.name＝＝1表示判断系统当前处于哪个离散模式，即判断变量name是否为1，若为1，则处于dm模式，若不为1则不处于dm模式；然后将离散模式的转移条件dguard转换为guard。一旦发生转移，目标模式的离散控制流dm’.dflow将会被执行，并且当前所处的离散模式将由dm变为dm’，即令dm.name＝0，dm’.name＝1。由于连续模式之间没有发生转移，因此目标连续状态仍然是源连续状态l；规则中的单等号表示定义、赋值；双等号表示判断两边是否相等，之后的规则类似。
[0066] 上述规则中，Tr(dm)表示翻译离散模式的规则，dm表示被翻译的离散模式，flow表示混合自动机控制流的集合，t’＝1表示时间的变化速度为1，jumps表示混合自动机迁移关系的集合，jps表示转换后新增的迁移关系的集合，jp表示迁移关系集合jps中的某一条关系，1表示混合自动机中的某一状态，dm.period表示离散模式的周期，dm.name表示离散模式的标签，dguard表示离散模式的迁移条件，dm’表示迁移的目标离散模式，dm’.name表示目标离散模式的标签，dm’.dflow表示目标模式的控制流，dm.dTrans表示离散模式dm的转移关系集合。
[0067] 下面规则表示一个周期后离散模式没有发生转移。
[0068] Tr(dm)＝(‑，‑，‑，flow∪t′＝1，jumps∪jps，‑)
[0069] where jps＝{jp|jp＝(l，l，t≥dm.period；dm.name＝＝1，dm.dflow；t＝0}[0070] 该规则表示当离散模式不发生转移时，执行dm.dflow，在周期结束时进入下一个周期。其他参数与离散模式发生转移时的规则相同。
[0071] 步骤四中，将HHML所建信物融合系统模型中的离散控制流转换到混合自动机的规则如下所述：
[0072] 混合自动机仅支持部分控制流，故给出了对条件语句、时间谓词的转换规则。
[0073] 对于离散控制流中的条件语句if cond then stmt1 else stmt2，本发明设置如下规则：
[0074] Tr(cd)＝(‑，‑，‑，‑，jumps∪jps，‑)
[0075]
[0076] 即包含条件语句的离散控制流dflow将被一分为二，并在jps分别用stmt1和stmt2来替换，转移条件分为条件cond和条件 其中，条件cond表示判断条件，stmt1表示条件成立时执行的操作，条件 表示该判断条件不成立，stmt2表示条件不成立时执行的操作，Tr(cd)表示翻译条件语句的规则，cd表示被翻译的条件语句，jumps表示混合自动机中迁移关系的集合，jps表示混合自动机中新增的迁移关系的集合，1表示混合自动机的某一状态。
[0077] 下面介绍了信物融合系统建模中时间谓词转换规则。
[0078] Tr(Duration(cond，c))＝(‑，var∪cnt，‑，‑，jumps∪jps，init∪cnt＝0)[0079]
[0080] Tr(After(cond，c))＝(‑，var∪cnt，‑，‑，jumps∪jps，init∪cnt＝0)[0081] where jps＝(‑，‑，cnt≥c，‑)∪(‑，‑，cond，cnt＝cnt+1)∪(‑，‑，cnt＞0，cnt＝cnt+1)
[0082] 以上两条规则均引入了一个额外的计数变量cnt。在Duration中，当离散模式的一个周期结束时，如果cond为真，cnt将增加1，否则将重置为0。当cnt≥c时，Duration(cond，c)的表达式为真。同样，对于After(cond，c)，当cond为真或cnt＞0，cnt将在周期结束时增加1，当cnt≥c时，表达式为真。其中，条件cond表示判断条件，c表示时间谓词所需满足的周期数，var表示变量集合，cnt表示一个用来计数的变量，jumps表示混合自动机中迁移关系的集合，jps表示混合自动机中新增的迁移关系的集合，init表示混合自动机中初始变量的集合。
[0083] 步骤四中，将HHML所建信物融合系统模型中的连续模式及其控制流转换到混合自动机的规则如下所述：
[0084] 连续模式及其控制流按照如下规则进行转换。
[0085] Tr(cm)＝(loc∪cm.name，‑，inv∪cm.cond，flow∪cm.eq，jumps∪cm.cguards，‑)[0086] 混合自动机的连续状态和HHML的连续模式在语义上是等价的，因此可以执行一对一的转换。连续模式的名称name只需转换为标签loc；微分方程eq可以转化为自动机控制流flow中的微分方程；until后的终止时的条件cond可以转化为自动机中的不变式inv。连续模式间的转移cTrans等价于混合自动机中的跃迁jump行为，且在跃迁过程中不执行任何重置操作。其中，loc表示混合自动机中状态的集合，cm.name表示所建模型中连续模式cm的标签，inv表示混合自动机中不变式的集合，cm.cond表示离散模式微分方程的终止时的条件，flow表示混合自动机控制流的集合，cm.eq表示微分方程，jumps表示混合自动机的迁移关系的集合，cm.guards表示连续模式间迁移条件的集合。
[0087] 本发明的有益效果包括：能够进行严格地软件需求分析及建模、易于描述嵌入式软件运行环境、可以图形化表示、软件进行充分地高置信的性质验证。
附图说明
[0088] 图1是本发明实施例1信物融合系统中的离散模式及其控制流。
[0089] 图2是本发明实施例2信物融合系统中的连续模式及其控制流。
[0090] 图3是本发明实施例3应用转换规则将月球着陆器慢速下降阶段的信物融合系统模型转换成的混合自动机模型。
[0091] 图4为本发明面向周期控制器的以模式为基础的信物融合系统建模及验证方法流程图。
具体实施方式
[0092] 结合以下具体实施例和附图，对发明作进一步的详细说明。实施本发明的过程、条件、实验方法等，除以下专门提及的内容之外，均为本领域的普遍知识和公知常识，本发明没有特别限制内容。
[0093] 下面将以月球着陆器的慢速下降阶段为例详细地描述本公开的示例性实施方式。在月球着陆器的慢速下降阶段，物理设备和控制程序组成采样数据控制系统。系统不断调整施加在着陆器上的推力，以保证着陆器在缓慢下降阶段保持稳定，从而顺利进入自由落体阶段，完成着陆。本发明将信物融合系统分为制导程序的当前阶段和着陆器动力学，前者是离散模式，后者是连续模式。易于图形化是HHML语言的一大特点。实施例1表示制导程序的离散模式，实施例2表示着陆器动力学的连续模式，实施例3表示将模型翻译成混合自动机的流程。
[0094] 实施例1
[0095] 如图1是信物融合系统中的离散模式及其控制流，它由两个离散模式构成。一个离散模式是周期为0.128s的制导模式guidance_program，首先它会对当前月球着陆器的质量m、所处位置r和速度v进行采样，这些都是在连续模式中的连续变量。接着根据施加在着陆器上的推力Fc来确定着陆器推力引擎的比冲量Isp。最后通过一系列的计算得到新的施加在着陆器上的推力Fc，其中m’表示更新后的着陆器的质量，DeltaT表示采样周期，a表示加速度这个中间变量，alC是所需的加速度，c1和c2表示制导过程中的控制系数，gM表示重力加速度。表示另一个离散模式是周期为0.128s的自由落体模式，此时系统停止进行对月球着陆器的制导，并发出停止制导的信号，即signal＝true，skip表示发出信号后不执行其它操作。由制导模式转移到自由落体模式的卫士条件r≤6∧After(r＞0，80)是指当着陆器所处高度低于6m并在当前慢速下降阶段经过了80个周期时成立。
[0096] 实施例2
[0097] 如图2是信物融合系统中的连续模式及其控制流。它由三个连续模式构成。连续模式一dynamic_1和连续模式二dynamic_2都表示系统制导时着陆器当前位置r、速度v和质量m的变化规律，用微分方程表示，它们的终止时的条件都是r≤0。当由控制器发出的施加在着陆器上的推力Fc＞3000时，连续模式一就会转移到连续模式二，当Fc≤3000时，连续模式二就会转移到连续模式一。连续模式三dynamic_3表示系统不再施加推力、着陆器开始自由落体时的变化规律，终止时的条件都是r≤0。只有当系统发出信号signal时，才会从连续模式一或二进入到连续模式三。
[0098] 实施例3
[0099] 如图3是应用转换规则将月球着陆器慢速下降阶段的信物融合系统模型转换成的混合自动机模型。为了图片的简洁，用g_p.dflow表示制导模式的控制流，用g_p.dflow_1表示将条件语句的前半句替换条件语句更新后的控制流，用g_p.dflow_2表示将条件语句的后半句替换条件语句更新后的控制流，用dynamic_1.cflow、dynamic_2.cflow、dynamic_3.cflow分别表示连续模式的控制流。根据规则引入了新的变量t和cnt分别表示时间和计数器，引入变量名g_p和s_g表示当前所处的离散模式。其它控制流和转移条件按照规则一一转化，在此不再赘述。经测试，转化后的混合自动机可以成功应用在验证工具上进行相关性质的验证。
[0100] 由此，通过对月球着陆器慢速下降阶段信物融合系统的建模，即使用提出的信物融合系统建模语言HHML，使得能够清楚准确的表示控制器间以及物理环境间的交互以及计算过程，并给出了图形化表示。另一方面，转换规则也能成功应用到建立好的模型中，使其转换成混合自动机，从而指导模型开发和验证人员更好的进行相关性质的验证和后续的工作。
[0101] 需要说明的是，在本文中，术语“包括”、“具有”或者其任何其他变体意在涵盖非排他性的包含，从而使得包括一系列要素的过程、方法、物品或者系统不仅包括那些要素，而且还包括没有明确列出的其他要素，或者是还包括为这种过程、方法、物品或者系统所固有的要素。
[0102] 通过以上的实施方式的描述，本领域的技术人员可以清楚地了解到上述实施例方法可借助软件的方式来实现，当然也可以通过硬件，但很多情况下前者是更佳的实施方式。基于这样的理解，本发明的技术方案本质上或者说对现有技术做出贡献的部分可以以软件产品的形式体现出来。
[0103] 本发明的保护内容不局限于以上实施例。在不背离发明构思的精神和范围下，本领域技术人员能够想到的变化和优点都被包括在本发明中，并且以所附的权利要求书为保护范围。
