zbMATH — the first resource for mathematics

Verification of evolving software via component substitutability analysis. (English) Zbl 1147.68047
Summary: This paper presents an automated and compositional procedure to solve the substitutability problem in the context of evolving software systems. Our solution contributes two techniques for checking correctness of software upgrades: (1) a technique based on simultaneous use of over-and under-approximations obtained via existential and universal abstractions; (2) a dynamic assume-guarantee reasoning algorithm – previously generated component assumptions are reused and altered on-the-fly to prove or disprove the global safety properties on the updated system. When upgrades are found to be non-substitutable, our solution generates constructive feedback to developers showing how to improve the components. The substitutability approach has been implemented and validated in the Comfort reasoning framework, and we report encouraging results on an industrial benchmark.

MSC:
 68Q60 Specification and verification (program logics, model checking, etc.) 68N30 Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.)
ComFoRT; YASM
Full Text:
References:
 [1] Abadi M, Lamport L (1995) Conjoining specifications. ACM Trans Program Lang Syst 17(3):507–534 · Zbl 01936471 · doi:10.1145/203095.201069 [2] ABB (2005) http://www.abb.com [3] Alur R, Cerny P, Madhusudan P, Nam W (2005) Synthesis of interface specifications for java classes. In: Proceedings of the 32nd ACM SIGPLAN-SIGACT symposium on principles of programming languages (POPL’05), Long Beach, CA, January 12–14, 2005. Assoc Comput Mach, New York, pp 98–109 · Zbl 1369.68126 [4] Alur R, Henzinger T (1996) Reactive modules. In: Proceedings of the 11th annual IEEE symposium on logic in computer science (LICS’96), New Brunswick, NJ, July 27–30, 1996. IEEE Comput Soc Press, Los Alamitos, pp 207–218 [5] Alur R, Madhusudan P, Nam W (2005) Symbolic compositional verification by learning assumptions. In: Proc of 17th int conf on computer aided verification · Zbl 1081.68601 [6] Angluin D (1987) Learning regular sets from queries and counterexamples. Inf Comput 75(2):87–106 · Zbl 0636.68112 · doi:10.1016/0890-5401(87)90052-6 [7] Ball T, Majumdar R, Millstein T, Rajamani S (2001) Automatic predicate abstraction of C programs. In: Proceedings of the ACM SIGPLAN conference on programming language design and implementation (PLDI), Snowbird, UT, June 20–22, 2001. Assoc Comput Mach, New York, pp 203–213 [8] Ball T, Rajamani SK (2000) Boolean programs: a model and process for software analysis. Technical Report MSR-TR-2000-14, Microsoft Research, Redmond, WA, February ftp://ftp.research.microsoft.com/pub/tr/tr-2000-14.pdf [9] Chaki S, Clarke E, Giannakopoulou D, Păsăreanu CS (2004) Abstraction and assume-guarantee reasoning for automated software verification. Technical Report 05.02, Research Institute for Advanced Computer Science (RIACS), Mountain View, CA [10] Chaki S, Sharygina N, Sinha N (2004) Verification of evolving software. In: Proceedings of the third workshop on specification and verification of component based systems (SAVCBS), Newport Beach CA, October 31–November 1, 2004. Iowa State University, Ames, pp 55–61 [11] Chaki S, Clarke E, Groce A, Ouaknine J, Strichman O, Yorav K (2004) Efficient verification of sequential and concurrent C programs. Form Methods Syst Des 25(2–3) · Zbl 1101.68677 [12] Chaki S, Clarke E, Sharygina N, Sinha N (2005) Dynamic component substitutability analysis. In: Proc of conf on formal methods · Zbl 1120.68421 [13] Chaki S, Clarke E, Sinha N, Thati P (2005) Automated assume-guarantee reasoning for simulation conformance. In: Proc of 17th int conf on computer aided verification · Zbl 1081.68612 [14] Chaki S, Ivers J, Sharygina N, Wallnau K (2005) The comfort reasoning framework. In: Proceedings of the 17th international conference on computer aided verification (CAV’05), Edinburgh Scotland, July 6–10, 2005. Lecture notes in computer science, vol 3576. Springer, New York, pp 164–169 · Zbl 1081.68613 [15] Chaki S, Strichman O (2007) Optimized L * for assume-guarantee reasoning. In: Proceedings of the 13th international conference on tools and algorithms for the construction and analysis of systems (TACAS’07) · Zbl 1147.68568 [16] Chakrabarti A, de Alfaro L, Henzinger TA, Jurdzinski M, Mang FYC (2002) Interface compatibility checking for software modules. In: Proceedings of the 14th international conference on computer aided verification (CAV’02), Copenhagen, Denmark, July 27–31, 2002. Lecture notes in computer science, vol 2404. Springer, New York, pp 428–441 · Zbl 1010.68505 [17] Clarke E, Grumberg O, Jha S, Lu Y, Veith H (2000) Counterexample-guided abstraction refinement. In: Proceedings of the 12th international conference on computer aided verification (CAV’00), Chicago, IL, July 15–19, 2000. Lecture notes in computer science, vol 1855. Springer, Berlin, pp 154–169 · Zbl 0974.68517 [18] Clarke E, Grumberg O, Long D (1992) Model checking and abstraction. In: Proceedings of the 19th ACM SIGPLAN-SIGACT symposium on principles of programming languages (POPL’92), Albuquerque, NM, January 19–22, 1992. Assoc Comput Mach, New York, pp 343–354 [19] Clarke E, Emerson A (1982) Design and synthesis of synchronization skeletons for branching time temporal logic. In: Proceedings of workshop on logic of programs, Yorktown Heights, New York, May 4–6 1982. Lecture notes in computer science, vol 131. Springer, Berlin, pp 52–71 [20] Clarke E, Long D, McMillan K (1989) Compositional model checking. In: Proceedings of the fourth annual IEEE symposium on logic in computer science (LICS’89), Pacific Grove, CA, June 5–8, 1989. IEEE Comput Soc, Los Alamitos, pp 353–362 · Zbl 0716.68035 [21] Clarke EM, Grumberg O, Peled D (2000) Model checking. MIT Press, Cambridge [22] Cobleigh JM, Giannakopoulou D, Păsăreanu CS (2003) Learning assumptions for compositional verification. In: Proceedings of the ninth international conference on tools and algorithms for the construction and analysis of systems (TACAS’03), Warsaw Poland, April 7–11, 2003. Lecture notes in computer science, vol 2619. Springer, New York, pp 331–346 [23] Cobleigh JM, Avrunin GS, Clarke LA (2006) Breaking up is hard to do: an investigation of decomposition for assume-guarantee reasoning. In: Proc of the ACM/SIGSOFT international symposium on software testing and analysis, pp 97–108 [24] Colón M, Uribe TE (1998) Generating finite-state abstractions of reactive systems using decision procedures. In: Proceedings of the 10th international conference on computer aided verification (CAV’98), Vancouver, Canada, June 28–July 2, 1998. Lecture notes in computer science, vol 1427. Springer, Berlin, pp 293–304 [25] Das S, Dill DL (2001) Successive approximation of abstract transition relations. In: Proceedings of the 16th annual IEEE symposium on logic in computer science (LICS’01), Boston, MA, June 16–19, 2001. IEEE Comput Soc, Los Alamitos, pp 51–60 [26] de Alfaro L, Henzinger TA (2001) Interface automata. In: Proceedings of the ninth ACM SIGSOFT symposium on foundations of software engineering (FSE’01), Vienna, Austria, September 10–14, 2001. Assoc Comput Mach, New York, pp 109–120 [27] de Roever WP, Langmaack H, Pnueli A (eds) (1998) Compositionality: the significant difference, international symposium, COMPOS’97, Bad Malente, Germany, September 8–12, 1997. Lecture notes in computer science, vol 1536. Springer, Berlin. (Revised lectures) [28] Dijkstra E (1976) A discipline of programming. Prentice-Hall, Englewood Cliffs · Zbl 0368.68005 [29] Gheorghiu M, Giannakopoulou D, Păsăreanu CS (2007) Refining interface alphabets for compositional verification. In: Proceedings of the 13th international conference on tools and algorithms for the construction and analysis of systems (TACAS’07) · Zbl 1186.68290 [30] Giannakopoulou D, Păsăreanu CS, Barringer H (2002) Assumption generation for software component verification. In: Proceedings of the 17th international conference on automated software engineering (ASE’02), Edinburgh, Scotland, September 23–27, 2002. IEEE Comput Soc, Los Alamitos, pp 3–12 [31] Graf S, Saïdi H (1997) Construction of abstract state graphs with PVS. In: Proceedings of the ninth international conference on computer aided verification (CAV’97), Haifa, Israel, June 22–25, 1997. Lecture notes in computer science, vol 1254. Springer, New York, pp 72–83 [32] Groce A, Peled D, Yannakakis M (2002) Adaptive model checking. In: Proceedings of the eighth international conference on tools and algorithms for the construction and analysis of systems (TACAS’02), Grenoble, France, April 8–12, 2002. Lecture notes in computer science, vol 2280. Springer, New York, pp 357–370 · Zbl 1043.68570 [33] Gupta A, McMillan K, Fu Z (2007) Automated assumption generation for compositional verification. In: Proceedings of the 19th international conference on computer aided verification (CAV’07) · Zbl 1135.68473 [34] Gurfinkel A, Chechik M (2006) Why waste a perfectly good abstraction? In: Proceedings of the 12th international conference on tools and algorithms for the construction and analysis of systems, pp 212–226 · Zbl 1180.68174 [35] Gurfinkel A, Wei O, Chechik M (2006) Yasm: A software model-checker for verification and refutation. In: Proc of computer-aided verification, pp 170–174 [36] Henzinger TA, Jhala R, Majumdar R, Sutre G (2002) Lazy abstraction. In: Proceedings of the 29th ACM SIGPLAN-SIGACT symposium on principles of programming languages (POPL’02). SIGPLAN notices, vol 37(1). Assoc Comput Mach, New York, pp 58–70 · Zbl 1323.68374 [37] Hopcroft JE, Ullman JD (1979) Introduction to automata theory, languages, and computation. Addison-Wesley, Reading · Zbl 0426.68001 [38] Ivers J, Sharygina N (2004) Overview of ComForT: a model checking reasoning framework. In: CMU/SEI-2004-TN-018 [39] Jones CB (1983) Tentative steps toward a development method for interfering programs. ACM Trans Program Lang Syst 5(4):596–619 · Zbl 0517.68032 · doi:10.1145/69575.69577 [40] Kurshan RP (1995) Computer-aided verification of coordinating processes: the automata-theoretic approach. Princeton University Press, Princeton · Zbl 0822.68116 [41] Liskov BH, Wing JM (1994) A behavioral notion of subtyping. ACM Trans Program Lang Syst 16(6):1811–1841 · doi:10.1145/197320.197383 [42] MAGIC: http://www.cs.cmu.edu/$$\sim$$chaki/magic · Zbl 06176318 [43] McCamant S, Ernst MD (2004) Early identification of incompatibilities in multi-component upgrades. In: Proceedings of the 18th European conference on object-oriented programming (ECOOP’04), Oslo, Norway, June 14–18, 2004. Lecture notes in computer science, vol 3086. Springer, New York, pp 440–464 [44] McMillan K (1997) A compositional rule for hardware design refinement. In: Proceedings of the ninth international conference on computer aided verification (CAV’97), Haifa, Israel, June 22–27, 1997. Lecture notes in computer science, vol 1254. Springer, New York, pp 24–35 [45] Misra J, Chandy KM (1981) Proofs of networks of processes. IEEE Trans Softw Eng 7(4):417–426 · Zbl 05341575 · doi:10.1109/TSE.1981.230844 [46] Nam W, Alur R (2006) Learning-based symbolic assume-guarantee reasoning with automatic decomposition. In: 4th International symposium on automated technology for verification and analysis (ATVA’06), pp 170–185 · Zbl 1161.68578 [47] Pnueli A (1985) In transition from global to modular temporal reasoning about programs. In: Logics and models of concurrent systems. Springer, New York, pp 123–144 [48] Rivest RL, Schapire RE (1993) Inference of finite automata using homing sequences. Inf Comput 103(2):299–347 · Zbl 0786.68082 · doi:10.1006/inco.1993.1021 [49] Roscoe AW (1998) The theory and practice of concurrency. Prentice-Hall International, New York [50] Shoham S, Grumberg O (2004) Monotonic abstraction-refinement for CTL. In: Proceedings of the 10th international conference on tools and algorithms for the construction and analysis of systems (TACAS’04), pp 546–560 · Zbl 1126.68487 [51] Sinha N, Clarke E (2007) SAT-based compositional verification using lazy learning. In: Proceedings of the 19th international conference on computer aided verification (CAV’07) · Zbl 1135.68483
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.