一种基于模型驱动工程进行SysML状态机图分析验证的方法

摘要

基于模型驱动工程进行SysML状态机图分析验证的方法，包括步骤：步骤10：根据编辑器设计一个SysML状态机图；步骤11：设计状态机图的时钟；步骤12：新建一个ATL工程；步骤13：将用户设计的状态机图及我们提供的两个元模型和一个转换文件导入到工程中；步骤14：运行转换文件得到结果文件；步骤15：将结果文件用Uppaal打开，模拟分析及验证用户设计的SysML状态机图。本发明为可以验证半形式化的SysML状态机图，自动化程度高，基于模型驱动工程理念而非传统方法，有效利用现有验证工具等。

主权项

一种基于模型驱动工程进行SysML状态机图分析验证的方法，其特征是包括步骤：步骤10：根据编辑器设计一个SysML状态机图；步骤11：设计状态机图的时钟；步骤12：新建一个ATL工程；步骤13：将用户设计的状态机图及两个元模型和一个转换文件导入到工程中；步骤14：运行转换文件得到结果文件；步骤15：将结果文件用Uppaal打开，模拟分析及验证用户设计的SysML状态机图；所述的设计一个SysML状态机图即步骤10的具体步骤如下：步骤200：用eclipse运行SysML状态机图编辑器；步骤201：右键单击根节点，新建一个或多个Region；步骤202：右键单击Region节点，创建系统中所需要的State节点，同时为每个State节点命名，如果State节点有时限变量，则跳转到步骤203，否则跳转到步骤204；步骤203：右键单击State节点，增加时限变量节点，并设置初始值；步骤204：右键单击Region节点，创建系统中所需要的Transition节点，同时为每个Transition节点命名及指定源和目标状态；步骤205：右键单击Region节点，增加局部变量声明节点；步骤206：右键单击Region节点，增加参数节点；步骤207：右键单击Region节点，增加名字节点；步骤208：右键单击根节点，增加全局变量声明节点；步骤209：右键单击根节点，增加系统模型声明节点；步骤210：结束本次SysML状态机图设计；所述的设计状态机图的时钟即步骤11中步骤如下：要描述时间触发机制，首先需要对时间进行建模，建立系统的时间访问入口即时钟，具体过程为：步骤 30：建立一个离散的时钟类，采用<<ClockType>>构造型表明该类是一个时钟类，并在约束中描述相应的标记值来定义其他特征；步骤 31：导入MARTE库中的idealClk实例，代表实际物理时间的连续时钟；步骤 32：定义离散时钟类的两个实例（clk1，clk2）；创建一个新的ATL工程并将设计的SysML状态机图和两个元模型和一个转换文件导入到工程即步骤12和步骤13，过程包括：步骤40：安装ATL插件；步骤41：将设计的SysML状态机图和上述两个元模型和一个转换文件导入到工程；所述运行转换文件即步骤14，其中运行的过程包括：步骤51：状态机图到时间自动机网络的转换；步骤52：状态机图Region到时间自动机的转换；步骤53：状态机图中状态到时间自动机Location和分支点的转换；步骤54：状态机图中状态图迁移到时间自动机迁移的转换；步骤55：状态机图中初始状态到时间自动机初始节点的转换；步骤56：状态机图中迁移上的卫式，触发动作，触发后的行为到时间自动机迁移上Label的转换；步骤57：状态机图中概率到时间自动机概率的转换；步骤58：状态机图中时间约束到时间自动机时间约束的转换；步骤59：得到转换结果文件；SysML状态机图设计模型的模拟，分析与验证即所述步骤15，其过程包括：步骤61：用模型检验工具Uppaal打开转换结果文件；步骤62：在模拟器标签中，通过点击下一步来模拟系统的运行过程；模拟过程能够保存文件；步骤63：在验证器标签中，通过点击添加按钮来增加系统的一条验证性质；步骤64：在验证器标签中，通过构造简单CTL表达式来表示系统的某些性质；步骤65：在验证器标签中，通过点击开始验证按钮来验证某条性质是否满足，若不满足可以得到一个反例；步骤66：在验证器标签中，通过点击删除按钮，删除某条不再需要的性质；步骤67：在验证器标签中，验证结果与进度显示了整个验证过程和结果。