计算机应用与软件2016，Vol.33Issue(11)：1-7,48,8.DOI:10.3969/j.issn.1000-386x.2016.11.001
模型精化过程中模型间一致性检测研究
RESEARCH OF CONSISTENCY CHECKING BETWEEN MODELS IN THE PROCESS OF MODEL REFINEMENTS
摘要
Abstract
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.关键词
模型精化/模型检测/一致性检测/属性抽取/线性时序逻辑Key words
Model refinement/Model checking/Consistency checking/Property extract/Linear temporal logic分类
信息技术与安全科学引用本文复制引用
王玲,徐立华..模型精化过程中模型间一致性检测研究[J].计算机应用与软件,2016,33(11):1-7,48,8.基金项目
国家自然科学基金项目（61502170）；上海市科委自然科学基金项目（13ZR1413000）。 （）
