Java程序模型验证中的程序建模问题研究
|
摘要
计算机系统的发展对软件提出了更高的要求,相应的提升软件质量这一课题的研究也日益受到从业人员的重视,而软件的可靠性、正确性是保证软件具有高质量的关键因素。
目前,在实际的软件验证中,普遍采用的方法是对系统进行大规模的测试,通过输入多个测试用例并检查执行结果是否正确来发现系统中可能存在的问题,但是这种方法通常无法穷举系统所有可能的行为。近些年来,模型验证在验证硬件系统组件和通信协议上的应用已经相当成熟,把模型检测应用于软件系统的验证已经成为备受关注的焦点,且已取得显著成就。许多研究小组开发出了多种实用的软件模型验证工具,如SLAM、MAGIC、JPF等。
模型验证技术成功应用于软件系统中的最大阻碍就是程序建模时的状态爆炸问题,本文结合NASA Ames的自动化软件工程小组开源项目JPF(Java PathFinder),在建模—验证—模型细化框架下研究了Java程序模型验证的程序建模过程中缩减程序状态空间的两种方法:程序切片技术和抽象技术。
本文的主要工作包括以下几个部分:
1.介绍了在建模—验证—模型细化框架下对软件系统进行模型验证的方法。
2.在对处理并发机制的并发流程语言(CFCL)进行了形式化描述的基础上,探讨了对多线程程序切片的正确性进行互模拟验证的方法,有效的保证了多线程切片的正确性。
3.提出了正确构造多线程程序切片的方法。模型验证与规范化建模语言的紧密结合,极大的推动了验证自动化的发展。
4.针对抽象技术的使用会出现反例路径“不可行”的情况,提出了验证反例路径可行性的两种方法:无选择路径搜索和抽象反例导向模拟。
As the development of the computer system, the study for the advance in the quality of the software is attached more and more importance by the professional. And the key factors for the high qualities of the software systems are the correctness and reliability.
Recently, the method which is used frequently in the software verification is testing the large system. By imputing many testing cases and examining the results, we may find the bugs of the system. But by this method, we couldn't perform all the behaviors of the system. At present, model checking has matured into an effective technique for reasoning about realistic components of the hardware systems and the communication protocols, and the applying of the model checking in the software system verification is becoming one of the focuses now. A lot of software model checking tools are already developed by many research groups, such as SLAM、MAGIC、JPF etc.
The state explosion problem is the major hurdle in applying model checking to software systems. In this paper, we research two methods for reducing the state-space in the modeling of the Java program model checking, which are the program-slicing and abstract. Our work is in the frame of modeling-verify-refine modeling and based on the open source project JPF (Java PathFinder). The main work in this paper is as follow:
1. Introduced the software model checking in the frame of modeling-verify-refine modeling.
2. Based on the formal study of the CFCL(Concurrent Flowchart Language), we researched the bisimulation method for correctness of the multi-thread program slicing .
3. Put forward the multi-thread program slicing method. The model checking method combined with the formal modeling language can impulse the automatic software verification observably.
4. To handle the spurious counter example which are caused by the program abstract technique, we put forward two methods for finding the feasible counter example in the model checking, which are free-choice search and guided simulation.
目前,在实际的软件验证中,普遍采用的方法是对系统进行大规模的测试,通过输入多个测试用例并检查执行结果是否正确来发现系统中可能存在的问题,但是这种方法通常无法穷举系统所有可能的行为。近些年来,模型验证在验证硬件系统组件和通信协议上的应用已经相当成熟,把模型检测应用于软件系统的验证已经成为备受关注的焦点,且已取得显著成就。许多研究小组开发出了多种实用的软件模型验证工具,如SLAM、MAGIC、JPF等。
模型验证技术成功应用于软件系统中的最大阻碍就是程序建模时的状态爆炸问题,本文结合NASA Ames的自动化软件工程小组开源项目JPF(Java PathFinder),在建模—验证—模型细化框架下研究了Java程序模型验证的程序建模过程中缩减程序状态空间的两种方法:程序切片技术和抽象技术。
本文的主要工作包括以下几个部分:
1.介绍了在建模—验证—模型细化框架下对软件系统进行模型验证的方法。
2.在对处理并发机制的并发流程语言(CFCL)进行了形式化描述的基础上,探讨了对多线程程序切片的正确性进行互模拟验证的方法,有效的保证了多线程切片的正确性。
3.提出了正确构造多线程程序切片的方法。模型验证与规范化建模语言的紧密结合,极大的推动了验证自动化的发展。
4.针对抽象技术的使用会出现反例路径“不可行”的情况,提出了验证反例路径可行性的两种方法:无选择路径搜索和抽象反例导向模拟。
As the development of the computer system, the study for the advance in the quality of the software is attached more and more importance by the professional. And the key factors for the high qualities of the software systems are the correctness and reliability.
Recently, the method which is used frequently in the software verification is testing the large system. By imputing many testing cases and examining the results, we may find the bugs of the system. But by this method, we couldn't perform all the behaviors of the system. At present, model checking has matured into an effective technique for reasoning about realistic components of the hardware systems and the communication protocols, and the applying of the model checking in the software system verification is becoming one of the focuses now. A lot of software model checking tools are already developed by many research groups, such as SLAM、MAGIC、JPF etc.
The state explosion problem is the major hurdle in applying model checking to software systems. In this paper, we research two methods for reducing the state-space in the modeling of the Java program model checking, which are the program-slicing and abstract. Our work is in the frame of modeling-verify-refine modeling and based on the open source project JPF (Java PathFinder). The main work in this paper is as follow:
1. Introduced the software model checking in the frame of modeling-verify-refine modeling.
2. Based on the formal study of the CFCL(Concurrent Flowchart Language), we researched the bisimulation method for correctness of the multi-thread program slicing .
3. Put forward the multi-thread program slicing method. The model checking method combined with the formal modeling language can impulse the automatic software verification observably.
4. To handle the spurious counter example which are caused by the program abstract technique, we put forward two methods for finding the feasible counter example in the model checking, which are free-choice search and guided simulation.
引文
[1] Claus Pahl, A Pi-Calculus based Framework for the Composition and Replacement of Components [C]. In: OOPSLA'2001 Workshop on Specification and Verification of Component- Based Systems. ACM Press. 2001.
[2] Charatonik, W., Talbot, J. M. The Decidability of Model Checking Mobile Ambients [C]. In: Proc, of FoSSaCS'04, LNCS. Springer-Verlag, 2004.
[3] 林惠民, 张文辉. 模型检测:理论、方法与应用[J]. 电子学报, 2002(12): 12-18.
[4] Havelund K, Pressburger T. Model checking Java programs using Java PathFinder [C]. International Journal on Software Tools for Technology Transfer, 2000, 2 (4): 366-381
[5] Ball T, Rajamani S K. Bebop : A symbolic model checker for Boolean programs[C]. The 7th International SPIN Workshop on Model Checking of Software, Stanford, USA, 2000.
[6] Henzinger T A, Jhala R, Majumdar R , et al . Lazy abstraction[C]. The 29th Annual ACM SIGPLAN 2 SIGACT Symposium on Principles of Programming Languages , Portland , USA , 2002.
[7] Chaki S, Clarke E, Groce A , et al . Modular Verification of Software Components in [J]. ACM Transactions on Software Engineering, 2004, 30 (6) : 388-402.
[8] Flanagan C, Leino KRM, LillibridgeM, et al. Extended static checking for java[C]. The 2002 ACM SIGPLAN Conference on Programming Language Design and Implementation , Berlin , Germany , 2002.
[9] Visser W, Park S, Penix J. Using predicate abst raction to reduce object oriented programs for model checking [C]. The 3rd Workshop on Formal Methods in Software Practice, Portland, USA, 2000.
[10] A. Pnueli. Applicat ions of Temporal Logic to the Specification and Verification of Reactive System: A Survey of Current Trends [C]. In J. W. de Bakker, W.-P. de Roever, and GRozenberg, editors, Current Trends in Concurrency, volume 224 of Lecture Note in Computer Science, pages 510 584. springer-Verlag, 1986.
[11] Clarke M, Emerson E A, Sistlaap. Automatic verification of finite- state concurrent systems using temporal logic specification[C]. ACM Transact ions on Programming Languages and Systems, 1986, 8(2): 244-263.
[12] McMillan KL. Symbolic Model Checking[M]. Kluwer Academic Publishers , 1993
[13]G.J.Holzmann.The model Checker SPIN[C].IEEE Transactions on Software Engineering,1997,23(5):279-294.
[14]K.Havelund and T.Pressburger.Model Checking Java Programs Using Java PathFinder[C].International Journal on Software Tools for Technology Transfer (STTT),2000,2(4):366-381.Special issue of STTT containing selected submissions to the 4~(th)SPIN workshop,Paris,France,1998.
[15]Weiser M.Program Slicing[C].IEEE Transactions on Software Engineering,1984,10(4):352-357.
[16]Ottenstein K J,Ottenstein L M.The program dependence graph in a software development environment[C].ACM SIGPLAN Notices 1984,19(5):177-184.
[17]Horwitz S B,et al.Interprocedural slicing using dependence graphs[C].ACM Transactions on Programming Language and Systems.1990,12(1):26-60.
[18]Kamkar M,Shahmehri N.Interprocedural dynamic slicing[C].In:Proceedings of the 4~(th)Conference on Programming Language Implementation and Logic Programming.370-384 1992.
[19]Zhao J,et al.Static slicing of concurrent object-oriented programs[C].In:Proceedings of the 20~(th)IEEE Annual International Computer Software and Applications Conference,1996,312-320.
[20]Ohata F,et al.A Slicing method for object-oriented programs using lightweight dynamic information[C].In:Proceedings of the ACM SIGSOFT/SIGPLAN Software Engineering Symposium on Practical Software Development Environments.ACM SIGSOFT Notices.19(5):177-184.
[21]李必信,李宣东,郑国梁.一种对传统依赖图进行面向对象扩充的方案[J].软件学报,12(2):241-248。
[22]Li B,et al.A model for slicing Java Programs hierarchically[J].Journal of Computer Science & technology,2004,19(6):848-858.
[23]Cheng J.Slicing concurrent programs[C].In:proceedings of the 1~(st)International Workshop on Automated and Algorithmic Debugging.LNCS749 1993.
[24]Krinke J.Static slicing of threaded programs[C].In:Proceedings of the International Workshop on Program Analysis for software Tools and Engineering (PASTE 98),1998,35-42.
[25]Goswami D,Mall R.Dynamic slicing of concurrent programs[C].niPC2000:Bangalore,India,2000.
[26]Venkatesh G A.The semantic approach to program slicing[C].ACM SIGPLAN Notices.1991,26(6).
[27] Raja Vallee-Rai, Phong Co, Etienne Gagnon, et al. Soot: a Java Bytecode Optimization Framework [C]. Proc. of CASCON'99, 125-135, 1999 For http: //www. sable. mcgill. ca/soot/.
[28] Carsten K. Gomard and Neil D. Jones. Compiler generation by partial evaluation [C]. In G. X. Ritter, Editor. Information Processing 1989. Proceedings of the IFIP 11th World Computer Congress, pages 1139-1144. IFIP, North-Holland. 1989.
[29] Neil D, Jones, Carsten K, Gomard, and Peter Sestoft. Partial Evaluation and Automatic Program Generation[M]. Prentice-Hall International, 1993.
[30] Dwyer, M. and Hatcliff, J. Slicing software for model construction [C]. In : Proceedings of the 1999 ACM Workshop on Partial Evaluation and Program Manipulation, January 1999.
[31] K. Arnold and J. Gosling. The Java Programming Language [M]. Addison-Wesley, 1998.
[32] R.Milner. Communication and Concurrency [M]. Prentice Hall,1989.
[33] E.M. Clarke, O. Grumberg, and D. E. Long. Model checking and abstraction [C]. ACM Transactions on Programming Languages and Systems, 1994,16 (5): 1515-1542.
[34] Ball T, Majumdar R, Millstein T, et al. Automatic Predicate Abstraction of C Programs [C]. In: Proceedings of the Conference on Programming Language Design and Implementation (PLDI2001), Snowbird, Utah, 2001.
[35] Dams D, Gerth R, Grumberg O. Abstract Interpretation of Reactive Systems [C]. ACM Transactions on Programming Languages and Systems (TOPLAS), 19 (2): 253-291, 1997.
[36] Y. Kesten and A. Pnueli. Modularization and abstraction: The Keys to practical formal verification [C]. Lecture Notes in Computer Science, 1450, 1998.
[37] H. Saidi. Model checking guided abstraction and analysis [C]. In Proceedings of the 7~(th) International Static Analysis Symposium, 2000.
[38] D. Dam, R. Gerth, G. Dhmen, et al. Model checking using adaptive state and data abstraction [C]. In: Proc. 6~(th) International Conference on Computer-Aided Verification, 1994.
[39] E. M. Clarke, O. Grumberg, S. Jha, et al. Counterexample-guided abstraction refinement [C]. In: Proc. 12~(th) internat ional Conference on Computer-Aided Verification, 2000.
[40] T Ball and S. K. Rajamani. Checking temporal properties of software with Boolean programs [C]. In Proc. of the Workshop on Advances in Verification, 2000.
[41] V. Rusu and E. Singerman. On Proving safety properties by integrating static analysis, theorem proving and abstraction [C]. In Proceedings of Tools and Algorithms for the Construction and Analysis of Systems, 1999.
[42] M. B. Dwyer, J. Hatcliff, et al. Tool-supported program abstraction for finite-state verification [C]. In Proceedings of the 23rd International Conference on Software Engineering, 2001.
[2] Charatonik, W., Talbot, J. M. The Decidability of Model Checking Mobile Ambients [C]. In: Proc, of FoSSaCS'04, LNCS. Springer-Verlag, 2004.
[3] 林惠民, 张文辉. 模型检测:理论、方法与应用[J]. 电子学报, 2002(12): 12-18.
[4] Havelund K, Pressburger T. Model checking Java programs using Java PathFinder [C]. International Journal on Software Tools for Technology Transfer, 2000, 2 (4): 366-381
[5] Ball T, Rajamani S K. Bebop : A symbolic model checker for Boolean programs[C]. The 7th International SPIN Workshop on Model Checking of Software, Stanford, USA, 2000.
[6] Henzinger T A, Jhala R, Majumdar R , et al . Lazy abstraction[C]. The 29th Annual ACM SIGPLAN 2 SIGACT Symposium on Principles of Programming Languages , Portland , USA , 2002.
[7] Chaki S, Clarke E, Groce A , et al . Modular Verification of Software Components in [J]. ACM Transactions on Software Engineering, 2004, 30 (6) : 388-402.
[8] Flanagan C, Leino KRM, LillibridgeM, et al. Extended static checking for java[C]. The 2002 ACM SIGPLAN Conference on Programming Language Design and Implementation , Berlin , Germany , 2002.
[9] Visser W, Park S, Penix J. Using predicate abst raction to reduce object oriented programs for model checking [C]. The 3rd Workshop on Formal Methods in Software Practice, Portland, USA, 2000.
[10] A. Pnueli. Applicat ions of Temporal Logic to the Specification and Verification of Reactive System: A Survey of Current Trends [C]. In J. W. de Bakker, W.-P. de Roever, and GRozenberg, editors, Current Trends in Concurrency, volume 224 of Lecture Note in Computer Science, pages 510 584. springer-Verlag, 1986.
[11] Clarke M, Emerson E A, Sistlaap. Automatic verification of finite- state concurrent systems using temporal logic specification[C]. ACM Transact ions on Programming Languages and Systems, 1986, 8(2): 244-263.
[12] McMillan KL. Symbolic Model Checking[M]. Kluwer Academic Publishers , 1993
[13]G.J.Holzmann.The model Checker SPIN[C].IEEE Transactions on Software Engineering,1997,23(5):279-294.
[14]K.Havelund and T.Pressburger.Model Checking Java Programs Using Java PathFinder[C].International Journal on Software Tools for Technology Transfer (STTT),2000,2(4):366-381.Special issue of STTT containing selected submissions to the 4~(th)SPIN workshop,Paris,France,1998.
[15]Weiser M.Program Slicing[C].IEEE Transactions on Software Engineering,1984,10(4):352-357.
[16]Ottenstein K J,Ottenstein L M.The program dependence graph in a software development environment[C].ACM SIGPLAN Notices 1984,19(5):177-184.
[17]Horwitz S B,et al.Interprocedural slicing using dependence graphs[C].ACM Transactions on Programming Language and Systems.1990,12(1):26-60.
[18]Kamkar M,Shahmehri N.Interprocedural dynamic slicing[C].In:Proceedings of the 4~(th)Conference on Programming Language Implementation and Logic Programming.370-384 1992.
[19]Zhao J,et al.Static slicing of concurrent object-oriented programs[C].In:Proceedings of the 20~(th)IEEE Annual International Computer Software and Applications Conference,1996,312-320.
[20]Ohata F,et al.A Slicing method for object-oriented programs using lightweight dynamic information[C].In:Proceedings of the ACM SIGSOFT/SIGPLAN Software Engineering Symposium on Practical Software Development Environments.ACM SIGSOFT Notices.19(5):177-184.
[21]李必信,李宣东,郑国梁.一种对传统依赖图进行面向对象扩充的方案[J].软件学报,12(2):241-248。
[22]Li B,et al.A model for slicing Java Programs hierarchically[J].Journal of Computer Science & technology,2004,19(6):848-858.
[23]Cheng J.Slicing concurrent programs[C].In:proceedings of the 1~(st)International Workshop on Automated and Algorithmic Debugging.LNCS749 1993.
[24]Krinke J.Static slicing of threaded programs[C].In:Proceedings of the International Workshop on Program Analysis for software Tools and Engineering (PASTE 98),1998,35-42.
[25]Goswami D,Mall R.Dynamic slicing of concurrent programs[C].niPC2000:Bangalore,India,2000.
[26]Venkatesh G A.The semantic approach to program slicing[C].ACM SIGPLAN Notices.1991,26(6).
[27] Raja Vallee-Rai, Phong Co, Etienne Gagnon, et al. Soot: a Java Bytecode Optimization Framework [C]. Proc. of CASCON'99, 125-135, 1999 For http: //www. sable. mcgill. ca/soot/.
[28] Carsten K. Gomard and Neil D. Jones. Compiler generation by partial evaluation [C]. In G. X. Ritter, Editor. Information Processing 1989. Proceedings of the IFIP 11th World Computer Congress, pages 1139-1144. IFIP, North-Holland. 1989.
[29] Neil D, Jones, Carsten K, Gomard, and Peter Sestoft. Partial Evaluation and Automatic Program Generation[M]. Prentice-Hall International, 1993.
[30] Dwyer, M. and Hatcliff, J. Slicing software for model construction [C]. In : Proceedings of the 1999 ACM Workshop on Partial Evaluation and Program Manipulation, January 1999.
[31] K. Arnold and J. Gosling. The Java Programming Language [M]. Addison-Wesley, 1998.
[32] R.Milner. Communication and Concurrency [M]. Prentice Hall,1989.
[33] E.M. Clarke, O. Grumberg, and D. E. Long. Model checking and abstraction [C]. ACM Transactions on Programming Languages and Systems, 1994,16 (5): 1515-1542.
[34] Ball T, Majumdar R, Millstein T, et al. Automatic Predicate Abstraction of C Programs [C]. In: Proceedings of the Conference on Programming Language Design and Implementation (PLDI2001), Snowbird, Utah, 2001.
[35] Dams D, Gerth R, Grumberg O. Abstract Interpretation of Reactive Systems [C]. ACM Transactions on Programming Languages and Systems (TOPLAS), 19 (2): 253-291, 1997.
[36] Y. Kesten and A. Pnueli. Modularization and abstraction: The Keys to practical formal verification [C]. Lecture Notes in Computer Science, 1450, 1998.
[37] H. Saidi. Model checking guided abstraction and analysis [C]. In Proceedings of the 7~(th) International Static Analysis Symposium, 2000.
[38] D. Dam, R. Gerth, G. Dhmen, et al. Model checking using adaptive state and data abstraction [C]. In: Proc. 6~(th) International Conference on Computer-Aided Verification, 1994.
[39] E. M. Clarke, O. Grumberg, S. Jha, et al. Counterexample-guided abstraction refinement [C]. In: Proc. 12~(th) internat ional Conference on Computer-Aided Verification, 2000.
[40] T Ball and S. K. Rajamani. Checking temporal properties of software with Boolean programs [C]. In Proc. of the Workshop on Advances in Verification, 2000.
[41] V. Rusu and E. Singerman. On Proving safety properties by integrating static analysis, theorem proving and abstraction [C]. In Proceedings of Tools and Algorithms for the Construction and Analysis of Systems, 1999.
[42] M. B. Dwyer, J. Hatcliff, et al. Tool-supported program abstraction for finite-state verification [C]. In Proceedings of the 23rd International Conference on Software Engineering, 2001.