期刊文献+

复杂网络软件的着色Petri网层次建模及模型集成确认方法 被引量:2

Colored Petri nets based hierarchical modeling and integrated model validation approach for complicated network software
下载PDF
导出
摘要 为准确描述复杂网络软件多交互、高并发等行为特征,以提高复杂网络软件设计质量和效率,提出了一种基于着色Petri网(CP-net)的复杂网络软件层次化建模及模型集成确认方法。给出了复杂数据抽象、并发行为控制、同类实体建模等层次建模关键技术,以及功能单元覆盖划分、模型等价抽象等模型集成确认关键技术的解决方案,并以典型网络软件系统为例分析了上述方法的可用性和有效性。从目前鲜有对特定形式模型论述模型正确性确认方法的现状看,这种融合多种CP-net模型分析技术的模型集成确认方法能够有效确保层次模型正确描述网络软件多交互、高并发的复杂功能行为,为软件验证、一致性测试等重要软件分析过程的高效实施提供描述准确且规模可控的基础形式模型。 An approach for hierarchical modeling and integrated model validation of complicated network software based on colored Petri nets (CPnet) is proposed to precisely describe the software's complicated functionalities and con current behaviors to improve the software's design and efficiency. Certain significant techniques for modeling, such as complex data abstraction, concurrency control and homogeneous entities modeling, are presented in detail, and the resolutions of function units generation and concurrentequivalent model abstraction used for model validation are given. Besides, the proposed approach was applied to a specific network system as a representative to illustrate its usability and effectiveness. As there is few specific model validation methods discussed in literatures, this study con tributes to a novel CPnet based integrated model validation approach with better feasibility. Validated software CP net hierarchical models can specify complicated functionality and concurrent behaviors precisely for complex net work software systems, and furthermore, they can be well used as fundamental formal models to promote the effec tiveness and efficiency for the software verification or conformance testing technologies.
出处 《高技术通讯》 CAS CSCD 北大核心 2013年第11期1139-1147,共9页 Chinese High Technology Letters
基金 国家自然科学基金(61262017 61262082) 973计划(2012CB315802) 内蒙古自然科学基金重点项目(20080404Zd20) 内蒙古大学高层次引进人才基金资助项目
关键词 着色Petri网(CP-net) 网络软件 模型确认 并发控制 模型检验 colored Petri nets( CP-net), network software, model validation, concurrency control, model chec-king
  • 相关文献

参考文献24

  • 1Woodcock J, Larsen P G, Bicarregui J, et al. Formal meth- ods: practice and experience. ACM Computing Surveys, 2009,41(4) :19:1-19:36.
  • 2陈火旺,王戟,董威.高可信软件工程技术[J].电子学报,2003,31(z1):1933-1938. 被引量:115
  • 3梅宏,王千祥,张路,王戟.软件分析技术进展[J].计算机学报,2009,32(9):1697-1710. 被引量:101
  • 4Jhala R, Majumdar R. Software model checking. ACM Computing Surveys,2009,41 (4) :21:1-21:54.
  • 5Tretmans J. Model based testing with labelled transition systems. Formal Methods and Testing, LNCS 4949,2008, 1-38.
  • 6Jensen K, Kristensen L M. Coloured Petri Nets:Modelling and Validation of Concurrent Systems. Berlin:Springer, 2009.95-188.
  • 7Kupferman O, Vardi M Y. Model checking of safety prop- erties. In : Proceedings of the 11 th International Conference on Computer-Aided Verification, Trento, Italy, 1999. 172- 183.
  • 8蒋屹新,林闯,曲扬,尹浩.基于Petri网的模型检测研究[J].软件学报,2004,15(9):1265-1276. 被引量:20
  • 9Drusinsky D, Michael J B, Shing M T. A visual tradeoff space for formal verification and validation techniques. IEEE System Journal, 2008,2 (4) : 513-519.
  • 10Heimdahl M P. A case for specification validation. Verified Software : Theories, Tools, Experiments, LNCS 4171,2008, 392-402.

二级参考文献140

  • 1蒋屹新,林闯,曲扬,尹浩.基于Petri网的模型检测研究[J].软件学报,2004,15(9):1265-1276. 被引量:20
  • 2周建涛,史美林,叶新铭.工作流过程建模中的形式化验证技术[J].计算机研究与发展,2005,42(1):1-9. 被引量:31
  • 3Shaw M. Truth Vs. knowledge: The difference between what a component does and what we know it does//Proeeedings of the 8th International Workshop Software Specification and Design. Budapest, Hungary, 1996: 181- 185.
  • 4Binkley David. Source code analysis: A road map//Proceedings of the Future of Software Engineering. Minneapolis, MN, USA, 2007:104 -119.
  • 5Dwyer Matthew B, Hatcliff John, Robby, Pasareanu Corina S, Visser Willem. Formal software analysis emerging trends in software model cheeking//Proceedings of the Future of Software Engineering. Minneapolis, MN, USA, 2007: 120- 136.
  • 6Flemming Nielson, Hanne Riis Nielson, Chris Hankin. Principles of Program Analysis. Berlin, Germany: Springer Verlag, 2005.
  • 7Jackson Daniel, Rinard Martin. Software analysis: A roadmap//Proceedings of the Future of Software Engineering. Limerick, Ireland, 2000:133-145.
  • 8Aho Alfred V, Sethi Ravi, Ullman Jeffrey D. Compilers: Principles, Techniques, and Tools. New Jersey, USA: Addison-Wesley, 1986.
  • 9Clarke E M, Jr Grumberg O, Peled D A. Model Checking, Cambridge, MA: MIT Press, 2000.
  • 10Ball T, Rajamani S K. Automatically validating temporal safety properties of interfaces//Dwyer M B ed. Proceedings of the 8th SPIN Workshop. LNCS 2057. Springer, 2001:103-122.

共引文献236

同被引文献9

引证文献2

二级引证文献4

相关作者

内容加载中请稍等...

相关机构

内容加载中请稍等...

相关主题

内容加载中请稍等...

浏览历史

内容加载中请稍等...
;
使用帮助 返回顶部