本发明涉及软件工程，具体为一种基于sysml模型的软件建模方法。
背景技术：
1、系统建模语言(sysml)是一种用于支持系统工程应用的通用建模语言。它提供了一种标准化的方法来描述系统的各个方面，包括其结构、行为、要求和参数。sysml中的活动图是一种重要的行为图，用于描述系统中的流程和操作的逻辑顺序，它们以图形方式表示系统的活动(或过程)、决策路径、并行控制流和同步信息，从而使工程师能够以直观的方式理解和分析复杂的系统行为。
2、模型检查是一种自动化的技术，用于验证有限状态系统的模型是否满足给定的规范或属性，通过全面探索系统的所有可能状态，模型检查能够确保系统行为遵循特定的正确性条件，这在复杂系统的设计和验证中尤为重要，因为人工分析往往难以涵盖所有潜在的行为和交互，模型检查的一个关键优势是其能够提供反例(counterexample)，即导致规范不满足的具体系统执行路径，这对于诊断和解决设计问题非常有用。
3、为此，我们研发出了新的一种基于sysml模型的软件建模方法。
技术实现思路
1、(一)解决的技术问题
2、针对现有技术的不足，本发明提供了一种基于sysml模型的软件建模方法，解决了现有模型驱动开发的软件开发方式中存在的形式化验证效率低、成本高的问题。
3、(二)技术方案
4、为实现以上目的，本发明通过以下技术方案予以实现：一种基于sysml模型的软件建模方法，包括以下具体步骤：
5、s101、基于emf技术，构建sysml活动图和uppaal的元模型；
6、s102、基于sysml活动图元素和uppaal模型元素的对应关系，借助元模型，实现sysml活动图到uppaal时间自动机模型的转换；
7、s103、基于形式化验证技术，编写形式化性质规约，通过对uppaal时间自动机进行验证，进而确认sysml活动图满足性质规约的条件。
8、优选的，所述s101包括：
9、根据sysml活动图中关键元素的定义，及其xml源文件细节，使用ecore将sysml活动图建立为元模型；
10、根据uppaal时间自动机中的关键元素定义，及其xml源文件细节，使用ecore将uppaal时间自动机建立为元模型。
11、优选的，所述s102包括：
12、将sysml活动图中的动作节点映射到uppaal中的template，包含两个location，一个名为“initial”表示等待状态，另一个与动作名称相同表示动作正在执行；
13、sysml活动图中动作的启动条件使用uppaal中的布尔类型全局变量来模拟，uppaal中为每个控制流的输入边提供唯一的布尔变量来表示控制令牌；
14、sysml活动图中的控制节点对应到uppaal中的template中，不同的控制节点对应的template中location的数量和edge的信息有所差异。
15、优选的，所述s103包括：
16、基于ltl，ctl，tctl定义形式化性质规约模板；
17、根据实际软件需求，将需要满足的性质填入性质规约模板中，构成形式化性质规约；
18、根据定义好的形式化性质规约，对uppaal时间自动机进行验证，根据模型检查器返回的结果，判定sysml活动图是否满足性质规约，即是否满足软件需求。
19、优选的，所述sysml活动图建立的元模型采用模型管理模块进行管理输入，并且，sysml活动图输入后，根据上述所述方法，将sysml活动图转换为uppaal时间自动机。
20、优选的，所述s103中的形式化性质规约采用性质管理模块管理输入，并根据上述所述方法，提供形式化性质规约模板并记录输入的形式化性质规约。
21、优选的，所述s102中包括映射配置模块，用于sysml活动图的变量映射到形式化性质规约中的原子命题。
22、优选的，所述s102中包括模型验证模块，用于根据sysml活动图变量和形式化性质规约原子命题的映射，调用模型求解器，对uppaal模型进行验证，并返回验证结果。
23、(三)有益效果
24、本发明提供了一种基于sysml模型的软件建模方法。具备以下有益效果：
25、1、该种基于sysml模型的软件建模方法，通过将sysml活动图转换为uppaal模型，并利用模型检查进行验证，构成了一种强大的方法来确保系统设计的正确性和鲁棒性，通过这种方法，可以在设计阶段早期发现并纠正潜在的问题，从而避免了在系统开发后期或者实际部署中遇到昂贵的重新设计和维护问题，这种基于模型的验证方法为复杂系统的开发提供了一种高效、系统化的方式，确保了系统设计能够满足其要求和预期的行为。
26、2、该种基于sysml模型的软件建模方法，通过将sysml模型活动图与uppaal时间自动机均建模为emf元模型，之后，定义了sysml模型活动图的模型元素与uppaal时间自动机组成元素之间的映射关系，基于emf元模型实现二者之间的转换，接下，该方法提供了基于ltl、ctl和tctl的形式化规范性质模板，允许使用者基于此模板将软件需求转换为形式化性质规约，最后，再根据形式化性质规约，调用模型检查器验证uppaal时间自动机是否满足规约，进而说明代表软件结构的sysml模型活动图是否满足形式化规约，即软件需求，该方法填补了目前基于模型的软件开发领域缺乏可用的形式化验证工具的问题，显著提高了软件的可靠性与安全性，降低了软件的测试成本，并且，能够降低对使用者专业性的要求，可以显著提高形式化性质规范的编写速度。
1.一种基于sysml模型的软件建模方法，其特征在于，包括以下具体步骤：
2.根据权利要求1所述的一种基于sysml模型的软件建模方法，其特征在于：所述s101包括：
3.根据权利要求1所述的一种基于sysml模型的软件建模方法，其特征在于：所述s102包括：
4.根据权利要求1所述的一种基于sysml模型的软件建模方法，其特征在于：所述s103包括：
5.根据权利要求3所述的一种基于sysml模型的软件建模方法，其特征在于：所述sysml活动图建立的元模型采用模型管理模块进行管理输入，并且，sysml活动图输入后，根据上述所述方法，将sysml活动图转换为uppaal时间自动机。
6.根据权利要求4所述的一种基于sysml模型的软件建模方法，其特征在于：所述s103中的形式化性质规约采用性质管理模块管理输入，并根据上述所述方法，提供形式化性质规约模板并记录输入的形式化性质规约。
7.根据权利要求1所述的一种基于sysml模型的软件建模方法，其特征在于：所述s102中包括映射配置模块，用于sysml活动图的变量映射到形式化性质规约中的原子命题。
8.根据权利要求1所述的一种基于sysml模型的软件建模方法，其特征在于：所述s102中包括模型验证模块，用于根据sysml活动图变量和形式化性质规约原子命题的映射，调用模型求解器，对uppaal模型进行验证，并返回验证结果。
