计算机科学 ›› 2014, Vol. 41 ›› Issue (7): 135-139.doi: 10.11896/j.issn.1002-137X.2014.07.027
孙涛,叶新铭
SUN Tao and YE Xin-ming
摘要: 状态爆炸问题导致CP-nets并发模型的正确性验证工作十分困难。提出了基于并发属性的模型化简方法和基于功能组合的模型抽象方法,用于对模型进行处理,移去与并发属性不相关的模型元素,提升模型的抽象层次,使模型状态空间规模得到显著降低,并在并发属性相关行为上与原模型保持一致;在处理后模型中运用状态空间分析、模型检测等验证方法完成模型验证,针对验证得出的模型错误,通过处理前后模型的对照关系在原模型中进行改正。这在一定程度上避免了状态爆炸问题并实现了模型验证。通过将 上述方法应用于HMIPv6协议模型,验证了其有效性。
[1] Dalal S R,Jain A,Karunanithi N,et al.Model-Based Testing in Practice[C]∥Proc.of the 21st International Conference on Software Engineering.1999:285-294 [2] Yan J,Wang J,Chen H W.Survey of Model-based SoftwareTesting[J].Computer Science,2004,31(2):184-187 [3] Utting M.The Role of Model-Based Testing[C]∥Verified Software:Theories,Tools,Experiments,LNCS 4171.2008:510-517 [4] Farooq U,Lam C P,Li H.Towards Automated Test Sequence Generation[C]∥Proc.of the 19th Australian Conference on Software Engineering.2008:441-450 [5] Broy M,Jonsson B,Katoen J P,et al.Model-Based Testing of Reactive Systems[C]∥LNCS 3472.Springer,Heidelberg,2005 [6] Sun T,Ye X,Liu J,et al.CPN based protocol testing sequence generating method[J].Journal of PLA University of Science and Technology,2012,13(2):165-170 [7] Constant C,Jeron T,Marchand H,et al.Integrating FormalVerification and Conformance Testing for Reactive Systems[J].IEEE Transaction on Software Engineering,2007,33(8):558-574 [8] Zeng Y,Zhang L,Zhang Y,et al.Activity Diagram-based Method to Generate Test Sequence of Concurrent Software[J].Computer Science,2007,4(12):286-290 [9] Buchs D,Lucio L,Chen A.Model Checking Techniques for TestGenera-tion from Business Process Models[C]∥Proc.of the 14th Ada-Europe International Conference.2009:59-74 |
No related articles found! |
|