Model checking dynamic memory allocation in operating systems. (English) Zbl 1192.68147
Summary: Most system software, including operating systems, contains dynamic data structures whose shape and contents should satisfy design requirements during execution. Model checking technology, a powerful tool for automatic verification based on state exploration, should be adapted to deal with this kind of structure. This paper presents a method to specify and verify properties of C programs with dynamic memory management. The proposal contains two main contributions. First, we present a novel method to extend explicit model checking of C programs with dynamic memory management. The approach consists of defining a canonical representation of the heap, moving most of the information from the state vector to a global structure. We provide a formal semantics of the method that allows us to prove the soundness of the representation. Secondly, we combine temporal LTL and CTL logic to define a two-dimensional logic, in time and space, which is suitable to specify complex properties of programs with dynamic data structures. We also define the model checking algorithms for this logic. The whole method has been implemented in the well known model checker SPIN, and illustrated with an example where a typical memory reader/writer driver is modelled and analyzed.
MSC:
| 68N25 | Theory of operating systems |
| 68Q60 | Specification and verification (program logics, model checking, etc.) |
Software:
jETI; BLAST; SPIN; GROOVE; Bogor; Java PathFinder; General Purpose Hash Function Library; veriSoft; dSPIN; BanderaReferences:
| [1] | Alur, R., Arenas, M., Barcelo, P., Etessami, K., Immerman, N., Libkin, L.: First-order and temporal logics for nested words. In: LICS ’07: Proceedings of the 22nd Annual IEEE Symposium on Logic in Computer Science, pp. 151–160. IEEE Computer Society, Washington, DC (2007) · Zbl 1159.03018 |
| [2] | Alur, R., Etessami, K., Madhusudan, P.: A temporal logic of nested calls and returns. In: TACAS, pp. 467–481, Barcelona, 29 March–2 April 2004 · Zbl 1126.68466 |
| [3] | Avots, D., Dalton, M., Benjamin, V., Livshits, Lam, M.S.: Improving software security with a C pointer analysis. In: ICSE ’05: Proceedings of the 27th international conference on Software engineering, pp. 332–341. ACM, New York (2005) |
| [4] | Ball, T., Majumdar, R., Millstein, T., Rajamani, S.K.: Automatic predicate abstraction of C programs. In: PLDI ’01: Proceedings of the ACM SIGPLAN 2001 conference on Programming language design and implementation, pp. 203–213. ACM, New York (2001) |
| [5] | Bennett, B., Cohn, A.G., Wolter, F., Zakharyaschev, M.: Multi-dimensional modal logic as a framework for spatio-temporal reasoning. Appl. Intell. 17(3), 239–251 (2002) · Zbl 1051.03019 · doi:10.1023/A:1020083231504 |
| [6] | Beyer, D., Henzinger, T., Jhala, R., Majumdar, R.: The software model checker BLAST. Int. J. Softw. Tools Technol. Transf. (STTT), 9(5–6), 505–525 (2007) · doi:10.1007/s10009-007-0044-z |
| [7] | Bogudlov, I., Lev-Ami, T., Reps, T.W., Sagiv, M.: Revamping TVLA: making parametric shape analysis competitive. In: CAV, pp. 221–225, Berlin, 3–7 July 2007 |
| [8] | Bouajjani, A., Habermehl, P., Moro, P., Vojnar, T.: Verifying programs with dynamic 1-selector-linked structures in regular model checking. In: Proc. of 11th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS’05), Edinburgh, 4–8 April 2005 · Zbl 1087.68585 |
| [9] | Bouajjani, A., Habermehl, P., Rogalewicz, A., Vojnar, T.: Abstract regular tree model checking of complex dynamic data structures. In: Static Analysis, vol. 2006, pp. 52–70. Springer, New York (2006) · Zbl 1225.68067 |
| [10] | Brochenin, R., Demri, S., Lozes É.: Reasoning about sequences of memory states. In: LFCS, pp. 100–114 (2007) · Zbl 1132.68335 |
| [11] | Clarke, E.M., Grumberg, O., Peled, D.: Model Checking. MIT, Cambridge (1999) |
| [12] | Corbett, J.C., Dwyer, M.B., Hatcliff, J., Laubach, S., Pasareanu, C.S., Robby, S., Zheng, H.: Bandera: extracting finite-state models from Java source code. In: ICSE ’00: Proceedings of the 22nd international conference on Software engineering, pp. 439–448. ACM, New York (2000) |
| [13] | de la Cámara, P., Gallardo, M.M., Merino, P., Sanán, D.: Model checking software with well-defined APIs: the socket case. In: FMICS ’05: Proceedings of the 10th International Workshop on Formal Methods for Industrial Critical Systems, pp. 17–26. ACM, New York (2005) |
| [14] | de la Cámara, P., Gallardo, M.M., Merino, P.: Model extraction for ARINC 653 based avionics software. In: SPIN, pp. 243–262, Berlin, 1–3 July 2007 |
| [15] | Demartini, C., Iosif, R., Sisto, R.: dSPIN: a dynamic extension of SPIN. In: Proceedings of the 5th and 6th International SPIN Workshops on Theoretical and Practical Aspects of SPIN Model Checking, pp. 261–276. Springer, London (1999) |
| [16] | Distefano, D., Ohearn, P.W., Yang, H.: A local shape analysis based on separation logic. In: In TACAS, pp. 287–302. Springer, New York (2006) · Zbl 1180.68112 |
| [17] | Allen Emerson, E.: Automated temporal reasoning about reactive systems. In: Banff Higher Order Workshop, pp. 41–101. Springer, New York (1995) |
| [18] | Fradet, P., Le Métayer, D.: Shape types. In: POPL ’97: Proceedings of the 24th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, pp. 27–39. ACM, New York (1997) |
| [19] | Gallardo, M.M., Merino, P., Joubert, C., Sanan, D.: On-the-fly model checking for C programs with extended CADP in FMICS-jETI. In: ICECCS ’07: Proceedings of the 12th IEEE International Conference on Engineering Complex Computer Systems (ICECCS 2007), pp. 321–329. IEEE Computer Society, Washington, DC (2007) |
| [20] | Gallardo, M.M., Merino, P., Sanan, D.: Model checking C programs with dynamic memory allocation. In: to appear in the Proc. of the 32nd Annual IEEE International Computer Software and Applications Conference COMPSAC2008, Turku, 28 July–1 August 2008 |
| [21] | Godefroid, P.: Software model checking: The Verisoft approach. Form. Methods Syst. Des. 26(2), 77–101 (2005) · doi:10.1007/s10703-005-1489-x |
| [22] | Havelund, K., Pressburger, T.: Model checking Java programs using Java pathfinder. STTT, 2(4), 366–381 (2000) · Zbl 1059.68585 |
| [23] | Hendren, L.J., Hummell, J., Nicolau, A.: Abstractions for recursive pointer data structures: improving the analysis and transformation of imperative programs. In: PLDI ’92: Proceedings of the ACM SIGPLAN 1992 conference on Programming language design and implementation, pp. 249–260. ACM, New York (1992) |
| [24] | Holzmann, G.J.: The model checker SPIN. IEEE Trans. Softw. Eng. 23(5), 279–295 |
| [25] | Holzmann, G.J.: The SPIN Model Checker: Primer and Reference Manual. Addison-Wesley, Reading (2003) |
| [26] | Holzmann, G.J., Smith, M.H.: Software model checking: extracting verification models from source code. Softw. Test. Verif. Reliab. 11(2), 65–79 (2001) · doi:10.1002/stvr.228 |
| [27] | Kastenberg, H., Rensink, A.: Model checking dynamic states in GROOVE. In: SPIN, pp. 299–305, Vienna, 30 March–1 April 2006 |
| [28] | Klarlund, N., Schwartzbach, M.I.: Graph types. In: POPL, pp. 196–205, Charleston, January 1993 |
| [29] | Lerda, F., Visser, W.: Addressing dynamic issues of program model checking. In: SPIN ’01: Proceedings of the 8th International SPIN Workshop on Model Checking of Software, pp. 80–102. Springer, New York (2001) · Zbl 0985.68639 |
| [30] | Manevich, R., Yahav, E., Ramalingam, G., Sagiv, M.: Predicate abstraction and canonical abstraction for singly-linked lists. In: Proc. of VMCAI05. LNCS, vol. 3385, pp. 181–198. Springer, New York (2005) · Zbl 1111.68398 |
| [31] | Møller, A.: Verifying programs that manipulate pointers: (invited talk). In: Proceedings of INFINITY 2003, the 5th International Workshop on Verification of Infinite-State Systems. Elect. Notes Theor. Comp. Sci. 98, 3–4 (2004) |
| [32] | Møller, A., Schwartzbach, M.I.: The pointer assertion logic engine. In: PLDI ’01: Proceedings of the ACM SIGPLAN 2001 Conference on Programming Language Design and Implementation, pp. 221–231. ACM, New York (2001) |
| [33] | Musuvathi, M., Park, D.Y.W., Chou, A., Engler, D.R., Dill, D.L.: CMC: a pragmatic approach to model checking real code. SIGOPS Oper. Syst. Rev. 36(SI), 75–88 (2002) · doi:10.1145/844128.844136 |
| [34] | Nielson, F., Nielson, H.R., Hankin, C.: Principles of Program Analysis. Springer, New York (1999) · Zbl 0932.68013 |
| [35] | Partow, A.: General purpose hash function algorithms. http://www.partow.net/programming/hashfunctions/ |
| [36] | Reynolds, J.C.: Separation logic: a logic for shared mutable data structures. In: LICS, pp. 55–74, Copenhagen, 22–25 July 2002 |
| [37] | Robby, S., Dwyer, M.B., Hatcliff, J.: Bogor: an extensible and highly-modular software model checking framework. In: ESEC/FSE-11: Proceedings of the 9th European Software Engineering Conference Held Jointly with 11th ACM SIGSOFT International Symposium on Foundations of Software Engineering, pp. 267–276. ACM, New York (2003) |
| [38] | Sagiv, M., Reps, T., Wilhelm, R.: Parametric shape analysis via 3-valued logic. In: POPL ’99: Proceedings of the 26th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pp. 105–118. ACM, New York (1999) |
| [39] | Vardi, M.Y., Wolper, P.: An automata-theoretic approach to automatic program verification (preliminary report). In: LICS, pp. 332–344, Cambridge, 16–18 June 1986 |
| [40] | Yahav, E., Reps, T., Sagiv, M., Wilhelm, R.: Verifying temporal heap properties specified via evolution logic. In: ESOP2003: European Symp. on Programming. LNCS, vol. 2618, pp. 204–222. Springer, New York (2003) · Zbl 1032.68062 |
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. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.
