Santone, Antonella; Vaglini, Gigliola A local approach for temporal model checking of Java bytecode. (English) Zbl 1068.68082 J. Comput. Syst. Sci. 70, No. 2, 258-281 (2005). Summary: Modern computing applications require highly reliable software systems, but current validation techniques, like testing, fail to assure an adequate level of correctness. We present a model checking procedure to verify a subset of the Java virtual machine language with respect to properties expressed by a temporal logic. A tableau-based method is developed to prove the satisfaction of a formula: by this local approach a program computation is checked only if involved in the goal of the property verification. A special symbol \(\perp\) is introduced to represent “unknown” values, and computations are performed in a symbolic way exploiting the set of guards present in the formulae to refine possible unknown values. This kind of abstraction cuts the state explosion of the programs and it is applicable to check arbitrary formulae, but the result of the verification has an imprecision degree depending on the number of unknown values manipulated during each symbolic computation. Cited in 1 Document MSC: 68Q60 Specification and verification (program logics, model checking, etc.) 68N15 Theory of programming languages Keywords:Software systems; Temporal logic; Model checking; Tableau systems; Formula-based abstractions; Symbolic computations Software:Bandera; SPIN; Java PathFinder; LOTOS; SLAM PDFBibTeX XMLCite \textit{A. Santone} and \textit{G. Vaglini}, J. Comput. Syst. Sci. 70, No. 2, 258--281 (2005; Zbl 1068.68082) Full Text: DOI References: [1] T. Ball, S.K. Rajamani, The SLAM toolkit, in: Proceedings of the 13th International Conference on Computer Aided Verification (CAV 2001), Lecture Notes in Computer Science, vol. 2102, 2001, pp. 260-264.; T. Ball, S.K. Rajamani, The SLAM toolkit, in: Proceedings of the 13th International Conference on Computer Aided Verification (CAV 2001), Lecture Notes in Computer Science, vol. 2102, 2001, pp. 260-264. · Zbl 0996.68560 [2] Ball, T.; Rajamani, S. K., The SLAM projectdebugging system software via static analysis, (Proceedings of the 29th SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL 2002) (2002)), 1-3 [3] Barbuti, R.; De Francesco, N.; Santone, A.; Vaglini, G., Selective mu-calculus and formula-based abstractions of transition systems, J. Comput. System Sci., 59, 3, 537-556 (1999) · Zbl 0958.68122 [4] Bolognesi, T.; Brinksma, E., Introduction to ISO specification language LOTOS, Comput. Networks ISDN Systems, 14, 25-59 (1987) [5] Bradfield, J. C.; Stirling, C., Local model checking for infinite state spaces, Theoret. Comput. Sci., 96, 1, 157-174 (1992) · Zbl 0747.68036 [6] G. Bruns, P. Godefroid, Model checking partial state spaces with 3-valued temporal logics, in: Proceedings of the 11th International Conference on Computer Aided Verification (CAV 1999), Lecture Notes in Computer Science, vol. 1633, 1999, pp. 274-287.; G. Bruns, P. Godefroid, Model checking partial state spaces with 3-valued temporal logics, in: Proceedings of the 11th International Conference on Computer Aided Verification (CAV 1999), Lecture Notes in Computer Science, vol. 1633, 1999, pp. 274-287. · Zbl 1046.68583 [7] G. Bruns, P. Godefroid, Generalized model checking: reasoning about partial state spaces, in: Proceedings of the 11th International Conference on Concurrency Theory (CONCUR 2000), Lecture Notes in Computer Science, vol. 1877, 2000, pp. 168-182.; G. Bruns, P. Godefroid, Generalized model checking: reasoning about partial state spaces, in: Proceedings of the 11th International Conference on Concurrency Theory (CONCUR 2000), Lecture Notes in Computer Science, vol. 1877, 2000, pp. 168-182. · Zbl 0999.68524 [8] Char, B. W.; Geddes, K. O.; Gonnet, G. H.; Leong, B. L.; Monagan, M. B.; Watt, S. M., First LeavesA Tutorial Introduction to Maple V (1992), Springer: Springer Berlin · Zbl 0758.68037 [9] Cleaveland, R., Tableau-based model checking in the propositional mu-calculus, Acta Inform., 27, 8, 725-747 (1990) · Zbl 0676.03033 [10] R. Cleaveland, S. Sims, The NCSU concurrency workbench, in: Proceedings of the Eighth International Conference on Computer-Aided Verification (CAV’96), Lecture Notes in Computer Science, vol. 1102, 1996, pp. 394-397.; R. Cleaveland, S. Sims, The NCSU concurrency workbench, in: Proceedings of the Eighth International Conference on Computer-Aided Verification (CAV’96), Lecture Notes in Computer Science, vol. 1102, 1996, pp. 394-397. [11] A. Coen-Porisini, G. Denaro, C. Ghezzi, M. Pezzé, Using symbolic execution for verifying safety-critical systems, in: Proceedings of the Joint 8th European Software Engineering Conference and 9th ACM SIGSOFT Symposium on the Foundations of Software Engineering (ESEC \(/\); A. Coen-Porisini, G. Denaro, C. Ghezzi, M. Pezzé, Using symbolic execution for verifying safety-critical systems, in: Proceedings of the Joint 8th European Software Engineering Conference and 9th ACM SIGSOFT Symposium on the Foundations of Software Engineering (ESEC \(/\) [12] J. Corbett, M. Dwyer, J. Hatcliff, C. Pasareanu, Robby, S. Laubach, H. Zheng, Bandera: extracting finite-state models from Java source code, in: Proceedings of the 22nd International Conference on Software Engineering 2000, ACM Press, 2000, pp. 439-448.; J. Corbett, M. Dwyer, J. Hatcliff, C. Pasareanu, Robby, S. Laubach, H. Zheng, Bandera: extracting finite-state models from Java source code, in: Proceedings of the 22nd International Conference on Software Engineering 2000, ACM Press, 2000, pp. 439-448. [13] S. Das, D.L. Dill, S. Park, Experience with predicate abstraction, in: Proceedings of the 11th International Conference on Computer Aided Verification (CAV 1999), Lecture Notes in Computer Science, vol. 1633, 1999, pp. 160-172.; S. Das, D.L. Dill, S. Park, Experience with predicate abstraction, in: Proceedings of the 11th International Conference on Computer Aided Verification (CAV 1999), Lecture Notes in Computer Science, vol. 1633, 1999, pp. 160-172. · Zbl 1046.68589 [14] Demartini, C.; Iosif, R.; Sisto, R., A deadlock detection tool for concurrent Java programs, Software Practice Exp., 29, 7, 577-603 (1999) [15] P. Godefroid, R. Jagadeesan, Automatic abstraction using generalized model checking, in: Proceedings of the 14th International Conference on Computer Aided Verification (CAV’2002), Lecture Notes in Computer Science 2404, 2002, pp. 137-150.; P. Godefroid, R. Jagadeesan, Automatic abstraction using generalized model checking, in: Proceedings of the 14th International Conference on Computer Aided Verification (CAV’2002), Lecture Notes in Computer Science 2404, 2002, pp. 137-150. · Zbl 1010.68083 [16] Hatcliff, J.; Dwyer, M. B.; Zheng, H., Slicing software for model construction, Higher-Order Symb. Comput., 13, 4, 315-353 (2000) · Zbl 0972.68021 [17] Havelund, K.; Pressburger, T., Model checking Java programs using Java PathFinder, International J. Software Tools Technol. Transfer, 2, 4, 366-381 (2000) · Zbl 1059.68585 [18] T.A. Henzinger, R. Jhala, R. Majumdar, G.C. Necula, G. Sutre, W. Weimer, Temporal-safety proofs for systems code, in: Proceedings of the 14th International Conference on Computer Aided Verification (CAV’2002), Lecture Notes in Computer Science, vol. 2404, 2002.; T.A. Henzinger, R. Jhala, R. Majumdar, G.C. Necula, G. Sutre, W. Weimer, Temporal-safety proofs for systems code, in: Proceedings of the 14th International Conference on Computer Aided Verification (CAV’2002), Lecture Notes in Computer Science, vol. 2404, 2002. · Zbl 1010.68507 [19] Henzinger, T. A.; Jhala, R.; Majumdar, R.; Sutre, G., Lazy abstraction, (Proceedings of the 29th SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL 2002) (2002)), 58-70 · Zbl 1323.68374 [20] Holzmann, G., The model checker spin, IEEE Trans. Software Eng., 23, 5, 279-295 (1997), (special issue on formal methods in software practice) [21] Holzmann, G. J.; Smith, M. H., Software model checkingextracting verification models from source code, (Proceedings of FORTE \(/\) PSTV’99 (1999), Kluwer: Kluwer Beijing, China), 481-497 [22] Khurshid, S.; Pasareanu, C. S.; Visser, W., Generalized symbolic execution for model checking and testing, (Proceedings of TACAS 2003 (2003)), 553-568 · Zbl 1031.68519 [23] Lindholm, T.; Yellin, F., The Java Virtual Machine Specification (1996), Addison-Wesley: Addison-Wesley Reading, MA [24] McMillan, K. L., Symbolic Model Checking (1993), Kluwer Academic Publishers: Kluwer Academic Publishers Dordrecht · Zbl 1132.68474 [25] Milner, R., Communication and Concurrency (1989), Prentice-Hall: Prentice-Hall Englewood Cliffs, NJ · Zbl 0683.68008 [26] Pasareanu, C.; Visser, W., Verification of Java programs using symbolic execution and invariant generation, (Proceedings of SPIN 2004 (2004)), 164-181 · Zbl 1125.68367 [27] A. Santone, G. Vaglini, Model checking programs, Technical Report, TR-DII \(22/\); A. Santone, G. Vaglini, Model checking programs, Technical Report, TR-DII \(22/\) · Zbl 1282.68167 [28] A. Santone, G. Vaglini, Local model checking of Java bytecode, in: Proceedings of the Fourteenth International Conference on Software Engineering and Knowledge Engineering, ACM Press, 2002, pp. 383-389.; A. Santone, G. Vaglini, Local model checking of Java bytecode, in: Proceedings of the Fourteenth International Conference on Software Engineering and Knowledge Engineering, ACM Press, 2002, pp. 383-389. · Zbl 1068.68082 [29] Stata, R.; Abadi, M., A type system for Java bytecode subroutine, ACM Trans. Programming Languages Systems, 21, 1, 90-137 (1999) [30] C. Stirling, An introduction to modal and temporal logics for CCS, in: Concurrency: Theory, Language, and Architecture, Lecture Notes in Computer Science, vol. 391, 1989.; C. Stirling, An introduction to modal and temporal logics for CCS, in: Concurrency: Theory, Language, and Architecture, Lecture Notes in Computer Science, vol. 391, 1989. [31] Stirling, C.; Walker, D. J., Local model checking in the modal mu-calculus, Theoret. Comput. Sci., 89, 1, 161-177 (1991) · Zbl 0745.03027 [32] W. Visser, K. Havelund, G.P. Brat, S. Park, Model checking programs, in: Proceedings of the Fifteenth IEEE International Conference on Automated Software Engineering (ASE’00), IEEE Computer Society, 2000, pp. 3-12.; W. Visser, K. Havelund, G.P. Brat, S. Park, Model checking programs, in: Proceedings of the Fifteenth IEEE International Conference on Automated Software Engineering (ASE’00), IEEE Computer Society, 2000, pp. 3-12. 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.