用户名: 密码: 验证码:
基于数据库的简单非函数依赖程序不变量动态检测
详细信息    本馆镜像全文|  推荐本文 |  |   获取CNKI官网全文
摘要
迄今为止,计算机软件系统虽然仅仅只有短短的几十年历史,但是已经成为最广泛、最重要的应用系统之一。从而软件的质量成为人们目前广泛关注、高度重视的热点问题之一。基于合约的程序设计是提高软件质量的一种重要技术,已经得到了很大的发展。合约描述了程序内部的基本属性,良性运行的保证条件以及运行后的期望结果。程序不变量一般包含类不变量、前置条件和后置条件,它是一种基本的合约。
     本文研究并且建立了程序不变量动态生成系统的理论模型。在此理论模型中,针对函数依赖程序不变量和简单非函数依赖程序不变量动态生成理论、方法和技术进行了阐述;重点对简单非函数依赖程序不变量进行分析,基于数据库的理论提出了一种新的简单非函数依赖程序不变量动态检测的技术,针对各种的简单非函数依赖程序不变量类型建立了一系列检测方法。本文的不变量检测技术通过数据库中提供的SQL条件查询功能,灵活多变的检测各种常见类型的简单非函数依赖程序不变量,并且可以根据用户的实际
     需要随时指定新的程序不变量查询条件。最后,本文设计实现了一个简单非函数依赖程序不变量原型系统。该系统与现有的其它程序不变量检测工具(例如Daikon)比较具有明显的特色和优势:第一,基于关系数据库技术,具有良好的可扩展性;第二,使用SQL条件查询功能实现简单非函数依赖程序不变量检测,检测方法具有很好的灵活性。
The computer software system has been more and more popular and important today, so the quality of software has been a significant and hot issue. In order to improve software quality, DBC (Design By Contract) has been developed. Contracts describe properties, expectations and guarantees of a program. Program invariant, which includes class invariants, pre-condition and post-condition, is a common kind of contracts.
     In this paper, a theory model for dynamically generating program invariant is built. Based on the model, the dynamical generating technique of program invariant, both function dependent invariant and non- function dependent invariant, is discussed. Furthermore, a new method of dynamically generating non- functional dependent program invariant is presented. The method, which comprises of series of detecting measures of specific non-functional dependent program invariants by using SQL query, takes the advantage of database. So, we can dynamically discover any kind of non-function dependent program invariants by giving the query conditions.
     Finally, a prototype system for dynamically generating program invariant is implemented. Comparing with other tools, e.g. Daikon, the system has two excellent features. First, it is expansible; second, it can detect program invariants in a nimble way.
引文
[1]Jezequel J.M, Bertrand Meyer. Design by contract: the lessons of Ariane. Computer[J], Jan. 1997, pp. 129-130
    [2]Arnout.K. Extracting implicit contracts from .NET libraries. http://se.inf.ethz.ch/people/arnout 2002
    [3]Dodoo.N, Donovan. Al, Lin .L ,et al. Selecting predicates for implications in program analysis. March 16, 2002 http://pag.csail.mit.edu/~mernst/pubs/invariants-implications.ps
    [4]Ernst M. D, Griswold W.G, Yoshio Kataoka, et al. Dynamically discovering pointer-based program invariants[R]. University of Washington Department of Computer Science and Engineering technical report UW-CSE-99-11-02, (Seattle, WA), November 16, 1999. Revised March 17, 2000
    [5]Ernst M. D. Dynamically Discovering Likely Program Invariants. Ph.D. dissertation, University of Washington Department of Computer Science and Engineering, (Seattle, Washington), Aug. 2000
    [6]Ernst M. D, Adam Czeisler, Griswold W. G,et al. Quickly detecting relevant program invariants[C]. In ICSE 2000, Proceedings of the 22nd International Conference on Software Engineering, (Limerick, Ireland), June 7-9, 2000, pp. 449-458
    [7]Ernst M. D, Griswold W. G, Kataoka .Y , et al. Dynamic discovering program invariants involving collections. TR UW-CSE-99-11-02, University of Washington,2000
    [8]Ernst M. D, Cockrell.J,Griswold W. G ,et al. Dynamically discovering likely program invariants to support program evolution[J]. IEEE Transactions on Software Engineering, vol. 27, no. 2, Feb. 2001, pp. 99-123
    [9]Ernst M. D. Static and dynamic analysis: Synergy and duality[C]. InWODA 2003: ICSE Workshop on Dynamic Analysis, (Portland, OR), May 9, 2003, pp. 24-27
    [10]Hangal.S, Lam M. S. Tracking down software bugs using automatic detection[C]. In proceedings of the 24th international conference on software engineering, page 291-301, 2002
    [11]Arnout.K,Simon.R.The .Net contract wizard: Adding design by contract to language other than Eiffel[C].In Proceedings of TOOLs 39, IEEE Computer Society,2001,pp. 14-23
    [12]Kataoka.Y, Ernst M. D, Griswold W. G , et al. Automated support for program refactoring using invariants[C]. In Proceedings of the International Conference on Software Maintenance, (Florence, Italy), November 6-10, 2001, pp. 736-743
    [13]Bertrand Meyer. Applying “design by contract” [J]. Computer, 25(10):40-51, Oct. 1992
    [14]Bertrand Meyer. Eiffel: The Language. Object-Oriented Series. Prentice Hall, New York, NY, 1992
    [15]Bertrand Meyer. Object-Oriented Software Construction. Prentice Hall, New York, NY, 1997
    [16]Mock.M. Dynamic analysis from the bottom up. In Proceedings of international conference on software engineering ICSE workshop on dynamic analysis, pp. 13-16, May, 2003
    [17]Nimmer J.W, Ernst M.D.Static verification of dynamically detected program invariants: Integrating Daikon and ESC/Java. In Proceedings of RV'01, First Workshop on Runtime Verification, (Paris, France), July 23, 2001
    [18]连瑞琦.具有可适应性的程序分析技术.博士论文,中国科学院计算技术研究所,2000
    [19]Pytlik.B, Renieris.M, Krishnamurthi.S, et al. Automated fault localization using potential invariants. In AADEBUG, Sept. 2003
    [20]Xie.T , Notkin.D. Exploiting Synergy between testing and inferredpartial specification. In Proceedings of international conference on software engineering ICSE workshop on dynamic analysis, pp. 17-20, May, 2003
    [21]http://www.artima.com/intv/contracts.html/
    [22]http://www.eiffel.com/doc/manuals/technology/contract/
    [23]Richard Mitchell,Jim Mckim ,孟岩. Design by Contract 原则与实践[M].北京:人民邮电出版社,2003
    [24]Bertrand Meyer, Design by contract: building bug-free O-O software, in Hotline on Object-Oriented Technology, volume 4, pages 4-8 ,Number 2, December 1992
    [25]杨淑群,章仕昌.程序形式化验证中的两个基本问题[J],上饶师范学院学报 ,Vol.22 ,No.6 Dec. 2002
    [26]黄万徽.谓词逻辑在程序正确性证明中的应用[J],高等函授学报(自然科学版),1997年第6期
    [27]牟光灿等. 软件测试是软件质量保证的重要手段[J], 计算机应用研究, 1997年第2期
    [28]Hoare .C. An Axiomatic Approach to Computer Programming[J ] . Committ of the ACM,1969 ,(12) :10
    [29]Dijkstra E.W,A Discipline of programming[M]. Prentice - Hall ,Inc. ,Englewood Cliffs,1976 :93- 131
    [30]David Saff, Shay Artzi, Perkins J.H ,et al. Automatic test factoring for Java[C] ,In ASE 2005: Proceedings of the 21st Annual International Conference on Automated Software Engineering, (Long Beach, CA, USA), November 9-11, 2005, pp. 114-123
    [31]Ernst M.D., Perkins J.H. Learning from Executions: Dynamic Analysis for Software Engineering and Program Understanding ,November 7, 2005. Tutorial at 21st Annual International Conference on Automated Software Engineering
    [32]Ernst M.D. Verification for legacy programs In Verified Tools: Theories, Tools, Experiments, (Zürich, Switzerland), October 10-13,2005
    [33]Carlos Pacheco , Ernst M.D. Eclat: Automatic generation and classification of test inputs In ECOOP 2005 --- Object-Oriented Programming, 19th European Conference, (Glasgow, Scotland), July 25-29, 2005, pp. 504-527
    [34]Lilian Burdy, Yoonsik Cheon, David Cok, et al. An overview of JML tools and applications Software Tools for Technology Transfer, vol. 7, no. 3, June 2005, pp. 212-232
    [35]Ernst M.D,John Chapin. The Groupthink specification exercise In ICSE'05, Proceedings of the 26th International Conference on Software Engineering, (St. Louis, MO, USA), May 18-20, 2005, pp. 617-618
    [36]Perkins J.H, Ernst M.D.Efficient incremental algorithms for dynamic detection of likely invariants In Proceedings of the ACM SIGSOFT 12th Symposium on the Foundations of Software Engineering (FSE 2004), (Newport Beach, CA, USA), November 2-4, 2004, pp. 23-32
    [37] Kramer.R.iContract-The Java design by contract tool. In proceedings Technology of Object-oriented Language (TOOLS 26), 1998, pp. 295-307
    [38]Edward S.H,Sitaraman.M, Weide B.W ,et al. Contract-checking wrappers for C++ components. TR RSRG-04-02, Department of computer science, Clemson University, Feb. 2004.
    [39]Beugnard.A,Jezequel J.M, Plouzeau.N. et al. Making components contract aware. IEEE Computer, 38-45, July 1999
    [40]Meredith L.G ,Bjorg.S. Contracts and types. Communication of the ACM, 46(10), 41-47, Oct. 2003
    [41]Harder.M,Mellen.J,Ernst M.D.Improving test suites via operational abstraction. In Proceedings of the 25th International Conference on Software Engineering, (Portland, Oregon), May 6-8, 2003, pp. 60-71
    [42]Win T.N, Ernst M.D, Garland S.J ,et al. Using simulated execution in verifying distributed algorithms. Software Tools for TechnologyTransfer, vol. 6, no. 1, July 2004, pp. 67-76
    [43]Stephen McCamant ,Ernst M.D.Predicting problems caused by component upgrades[C]. In Proceedings of the 10th European Software Engineering Conference and the 11th ACM SIGSOFT Symposium on the Foundations of Software Engineering, (Helsinki, Finland), September 3-5, 2003, pp. 287-296
    [44]McCamant.S,Ernst M.D. Early identification of incompatibilities in multi-component upgrades[C]. In Object-Oriented Programming, 18th European Conference, (Olso, Norway), June 16-18, 2004, pp. 440-464
    [45]Stephen McCamant, Ernst M.D. Formalizing lightweight verification of software component composition[C]. In Specification and Verification of Component-Based Systems Workshop, (Newport Beach, CA, USA), October 31-November 1, 2004
    [46]陆汝玲.计算机语言的形式语义[M] 北京: 科学出版社, 1992. 327
    [47]http://jrat.sourceforge.net/index.html
    [48]http://jrat.sourceforge.net/flow.html
    [49]http://sourceforge.net/projects/jrat
    [50]Ernst M.D,et al. “The Daikon system for dynamic detection of likely invariants” [J]. Science of Computer Programming, 2007
    [51]Nadya Kuzmina, Ruben Gamboa. “Extending dynamic constraint detection with polymorphic analysis” [C].In WODA 2007: Workshop on Dynamic Analysis, (Minneapolis, MN, USA), May 22, 2007
    [52]Xie.T , Notkin.D. “Tool-assisted unit test generation and selection based on operational abstractions” [J]. Automated Software Engineering Journal, 2006
    [53]Leonardo Mariani. Ph.D. dissertation, “Behavior Capture and Test: Dynamic Analysis of Component-Based Systems” [D] .University of Milano -- Bicocca, (Milan, Italy), 2005
    [54]Hai Yuan , Xie.T.“Automatic extraction of abstract-object-state machines based on branch coverage” In 1st International Workshop on Reverse Engineering To Requirements (RETR 2005), (Pittsburgh, PA, USA), Nov. 2005, pp. 5-11
    [55]Tristan Denmat, Arnaud Gotlieb, “Proving or disproving likely invariants with constraint reasoning” In 15th Workshop on Logic-based Methods in Programming Environments (WLPE'05), October 5, 2005
    [56]Carlos Pacheco, Ernst M.D. “Eclat: Automatic generation and classification of test inputs” [C].In ECOOP 2005 --- Object-Oriented Programming, 19th European Conference, (Glasgow, Scotland), July 27-29, 2005, pp. 504-527.
    [57]Braberman Víctor, Garbervetsky Diego,et al.“Synthesizing parametric specifications of dynamic memory utilization in object-oriented programs” [C].In FTfJP'2005: 7th Workshop on Formal Techniques for Java-like Programs, (Glasgow, Scotland), July 26, 2005
    [58]Lilian Burdy, Yoonsik Cheon, David Cok, et al. “An overview of JML tools and applications” [J] .Software Tools for Technology Transfer, vol. 7, no. 3, June 2005, pp. 212-232
    [59] 刘 磊 , 叶 晓 煜 . 过 程 间 的 数 据 流 分 析 技 术 [J]. 计 算 机 研 究 与 发展,1997.4,34(4)
    [60]郁卫江,朱根江,谢立.一个过程间数据流分析的框架[J]. 软件学报,1997.9,8(9)
    [61]Carlos Pacheco, Ernst M.D.Eclat: Automatic generation and classification of test inputs [C],ECOOP 2005 --- Object-Oriented Programming, 19th European Conference, (Glasgow, Scotland)
    [62]http://pag.csail.mit.edu/eclat/
    [63]李慧贤,刘坚.数据流分析方法[J].计算机工程与应用,2003.13,142~144
    [64]黄波,臧斌宇,韦俊银等.上下文敏感的过程间指针分析[J],计算机学报,2000.5,23(5)

© 2004-2018 中国地质图书馆版权所有 京ICP备05064691号 京公网安备11010802017129号

地址:北京市海淀区学院路29号 邮编:100083

电话:办公室:(+86 10)66554848;文献借阅、咨询服务、科技查新:66554700