基于自适应点火的软件验证方法

摘要

本发明提供了一种基于自适应点火的软件验证方法，其将软件模型转换成情境Petri网模型，并通过自适应点火方式，消除情境Petri网变迁的歧义性，其中：所述情境petri网，是指在petri网中，通过在库所中加入情境语义维来为petri网的动态验证提供决策信息；所述情境语义包括由软件动态生成时存储在库所中的情境信息；所述自适应点火方式用于描述软件对不同情境条件的自主反应性；所述自适应点火方式是指根据当前库所中的情境语义来推测出托肯应该进入后面哪一个输出库所。本发明通过将软件模型转换成情境Petri网模型，利用Petri网本身的特性，并通过自适应点火来验证普适软件的正确性。

主权项

一种基于自适应点火的软件验证方法，其特征在于，将软件模型转换成情境Petri网模型，并通过自适应点火方式，消除情境Petri网变迁的歧义性，其中：所述情境Petri网，是指在Petri网中，通过在库所中加入情境语义维来为Petri网的动态验证提供决策信息；所述情境语义包括由软件动态生成时存储在库所中的情境信息；所述自适应点火方式用于描述软件对不同情境条件的自主反应性；如果一个变迁的每个输入库所都拥有托肯，该变迁即为被允许；一个变迁被允许时，变迁将发生点火，输入库所的托肯被消耗，同时为输出库所产生令牌；所述自适应点火方式是指根据当前库所中的情境语义来推测出托肯应该进入后面哪一个输出库所；所述情境语义包括功能性语义和非功能性语义，利用功能性语义的匹配程度和非功能性语义的效用值各自的排名结果来确定点火方向，其中，所述点火方向是指输入库所到输出库所的方向；所述的确定点火方向，具体为：根据情境语义的功能性语义的匹配程度进行排名，得到排名位置根据情境语的非功能性语义的效用值进行排名，得到排名位置根据如下公式得到每个候选托肯的得分，并选择得分最高的作为点火方向$R_i=\lambda \times \frac{1}{{\log }_2(P_{c_i}+1)}+(1-\lambda )\times \frac{1}{{\log }_2(P_{u_i}+1)}---\left(5\right)$其中，R_i表示候选的第i个情境语义的得分，1/log₂(P+1)用来表示用户潜在需求在P位置的值；λ∈[0,1],定义为情境语义的功能性语义比情境语义的非功能性语义的重要性；功能性语义是指用户兴趣；非功能性语义是指用户偏好；i＝1,2,…,k，k为基本情境的数量。