模型精化过程中模型间一致性检测研究

RESEARCH OF CONSISTENCY CHECKING BETWEEN MODELS IN THE PROCESS OF MODEL REFINEMENTS

传统的模型精化过程中模型间一致性检测专注于检测模型自身的正确性、死锁、以及不变式保持性等,而无法保证模型间行为方面的一致性。为此提出利用系统行为属性来反应模型行为,结合模型检测的方法来检测模型间的行为一致性。首先对精化前模型分析生成抽象测试用例并抽取其代表的系统行为属性;然后根据精化后的模型抽取模型精化关系并进一步更新系统属性;最后使用这些系统行为属性来验证精化后的模型是否依然满足其代表的系统行为,如果不满足则说明模型间存在不一致行为,可以通过生成的反例路径找出不一致的位置。实验结果表明使用该方法可以有效找出模型精化前后的大多数不一致行为。

During model refinement process,traditional consistency checking techniques tend to focus on the syntax and semantics of the models,their structural correctness,as well as deadlock and invariants retention,while ignoring the behavior consistency. To address the problem,the system behaviors are captured via the form of system property and model checking techniques are utilized to check the consistencies among system models. Firstly,the pre-refinement model is analyzed and abstract test cases are generated from it,important system behaviors are then extracted as system properties and expressed as linear temporal logic( LTL); Secondly,these system properties are updated based on the refinement relationships,which are extracted between pre and after refinement models. Thirdly,the extracted system properties are checked over the after-refinement model. The possible inconsistency positions could be found through the counter-example path.The early experimental results show that most of the inconsistency could be found between pre and after refinement models using this approach.