Logic in formal verification of computer systems. Some remarks

Trzęsicki, K.

Artykuł - szczegóły

Tytuł artykułu

Logic in formal verification of computer systems. Some remarks

Autorzy

Trzęsicki K.

Treść / Zawartość

Pełne teksty:

httpwww_wi_pb_edu_plplikinaukazeszytyz4trzesicki-full.pdf

Pobierz

Identyfikatory

Warianty tytułu

Logika i formalna weryfikacja systemów komputerowych. Kilka uwag

Języki publikacji

Abstrakty

Do specyfikacji i weryfikacji zarówno sprzętu jak i programów stosowane są różne logiki. Główną wadą metody teorio-dowodowej weryfikacji jest problem znalezienia dowodu. Zastosowanie tej metody zakłada aksjomatyzację logiki. Własności systemu mogą być sprawdzane za pomocą jego modelu. Model jest zbudowany w języku specyfikacji i sprawdzany automatycznie. Zastosowanie sprawdzania za pomocą modelu zakłada rozstrzygalność zadania. Istnieje wielka różnorodność programów (model checker) do sprawdzania własności za pomocą modeli.

Various logics are applied to specification and verification of both hardware and software systems. The problem with finding of proof is the most important disadvantage of proof-theoretical method. The proof-theoretical method presupposes the axiomatization of the logic. Proprieties of a system can also be checked using a model of the system. A model is constructed with the specification language and checked using automatic model checkers. The model checking application presupposes the decidability of the task.

Słowa kluczowe

logika weryfikacja metoda teorio-dowodowa sprawdzanie za pomocą modelu

logic verification proof-theoretical method model checking

Wydawca

Oficyna Wydawnicza Politechniki Białostockiej

Czasopismo

Zeszyty Naukowe Politechniki Białostockiej. Informatyka

Rocznik

2009

Tom

Z. 4

Strony

151--175

Opis fizyczny

Bibliogr. 92 poz.

Twórcy

autor

Trzęsicki K.

Bibliografia

[1] Alur R., Courcoubetis C., Dill D. L. (1990): Model-checking for real-time systems, in ‘Proceedings of the 5th Annual IEEE Symposium on Logic in Computer Science’, IEEE Computer Society Press, Philadelphia, PA, pp. 414–425.
[2] Alur R., Dill D. (1993): A theory of timed automata’, Inf. Comput. 194, 2–34.
[3] Aziz A., Sanwal K., Singhal V., Brayton R. (2000): Model checking continuous time Markov chains, ACM Trans. Computational Logic 1(1), 162–170.
[4] Aziz A., Sanwal K., Singhal V., Brayton R. K. (1996): Verifying continuous timeMarkov chains, in R. Alur, T. A. Henzinger, eds, ‘Eighth International Conference on Computer Aided Veriﬁcation CAV 1996’, Vol. 1102 of Lecture Notes in Computer Science, Springer Verlag, New Brunswick, NJ, USA, pp. 269–276.
[5] Baier C., Katoen J. P. (2008): Principles of Model Checking, The MIT Press. Foreword by Kim Guldstrand Larsen.
[6] Baier C., Katoen J.-P., Hermanns H. (1999): Approximate symbolic model checking of continuous-time Markov chains, in ‘International Conference on Concurrency Theory’, pp. 146—-161.
[7] Beer, I., Ben-David, S., Eisner, C., Landver, A. (1996): Rulebase: An industry-oriented formal veriﬁcation tool, in ‘Proceedings of the 33rd Conference on Design Automation (DAC’96)’, ACM Press, Las Vegas, NV, pp. 655––660.
[8] Ben-Ari, M., Manna, Z., Pnueli, A. (1981): The temporal logic of branching time, in ‘Proc. 8th ACM Symposium on Principles of Programming Languages’, ACM Press, New York, pp. 164–176. Por. [9].
[9] Ben-Ari, M., Manna, Z., Pnueli, A. (1983): ‘The temporal logic of branching time’, Acta Informatica 20, 207–226. Por. [8].
[10] Bérard, B., Bidoit, M., Finkel, A., Laroussinie, F., Petit, A., Petrucci, L., Schnoebelen, P. (2001): Systems and Software Veriﬁcation. Model-Checking Techniques and Tools, Springer.
[11] Bidoit, B. M., Finkel, A., Laroussinie, F., Petit, A., Petrucci, L. , Schnoebelen, P. (2001): Systems and Software Veriﬁcation: Model-checking Techniques and Tools, Springer.
[12] Boyer, R. S., Moore, J. S. (1979): A Computational Logic, Academic Press, New York.
[13] Boyer, R. S., Moore, J. S. (1988): ‘Integrating decision procedures into heuristic theorem provers: A case study of linear arithmetic’, Machine Intelligence 11, 83–124.
[14] Bradﬁeld, J. C., Stirling, C. (2001):Modal logics and µ-calculi: An introduction, in J. A. Bergstra, A. Ponse, S. A. Smolka, eds, ‘Handbook of Process Algebra’, Elsevier Science, chapter 4, pp. 293–330.
[15] Brock, B., Hunt, W. (1997): Formally specifying and mechanically verifying programs for the motorola complex arithmetic processor dsp, in ‘Proceedings of the IEEE International Conference on Computer Design (ICCD’97)’, pp. 31—-36.
[16] Cengarle, M. V., Haeberer, A. M. (2000): Towards an epistemology-based methodology for veriﬁcation and validation testing, Technical report 0001, Ludwig-Maximilian’s Universität, Institut für Informatik, München, Oettingen-str. 67. 71 pages.
[17] Cimatti, A., Clarke, E., Giunchig lia, E., Giunchig lia, F., Pistore, M., Roveri, M., Sebastiani, R., Tacchella, A. (2002): NUSMV2: A new opensource tool for symbolic model checking, in E. Brinksma, K. Larsen, eds, ‘Proceedings of the 14th International Conference on Computer-Aided Veriﬁcation (CAV 2002)’, Vol. 2404 of Lecture Notes in Computer Science, Springer-Verlag, Copenhagen, Denmark, pp. 359—-364.
[18] Cimatti, A., Clarke, E., Giunchig lia, F., Roveri, M. (1999): NUSMV2: A new symbolic model veriﬁer, in N. Halbwachs, D. Peled, eds, ‘Proceedings of the 11th International Conference on Computer-Aided Veriﬁcation (CAV ’99)’, Vol. 1633 of Lecture Notes in Computer Science, Springer-Verlag, Trento, Italy, pp. 495––499.
[19] Cimatti, A., Clarke, E.M., Giunchig lia, F., Roveri,M. (2000): ‘NUSMV: A new symbolic model checker’, International Journal on Software Tools for Technology Transfer 2(4), 410–425.
[20] Clarke, E. M. (2008): The birth of model checking, in DBLP:conf/spin/5000, pp. 1–26.
[21] Clarke, E. M., E., E. A. (1982): Design and synthesis of synchronization skeletons using branching-time temporal logic, in ‘Logic of Programs, Workshop’, Vol. 131 of Lecture Notes in Computer Science, Springer-Verlag, London, UK, pp. 52—-71.
[22] Clarke, E. M., Emerson, E. A., Sistla, A. P. (1983): Automatic veriﬁcation of ﬁnite state concurrent systems using temporal logic speciﬁcations: A practical approach, in ‘Conference Record of the Tenth Annual ACM Symposium on Principles of Programming Languages’, Austin, Texas, pp. 117–126.
[23] Clarke, E. M., Emerson, E. A., Sistla, A. P. (1986): ‘Automatic veriﬁcation of ﬁnite-state concurrent systems using temporal logic speciﬁcations’, ACMTransactions on Programming Languages and Systems 8(2), 244–263.
[24] Clarke, E. M., Grumberg, J. O., Peled, D. A. (1999): Model Checking, The MIT Press.
[25] Clarke, E. M., Grumberg, O., Jha, S., Lu, Y., Veith, H. (2001): Progress on the state explosion problem in model checking, in ‘Informatics — 10 Years Back. 10 Years Ahead.’, Vol. 2000 of Lecture Notes in Computer Science, Springer-Verlag, London, UK, pp. 176–194.
[26] Clarke, E.M.,Wing, J.M., Alur, R., Cleaveland, R., Dill, D., Emerson, A., Garland, S., German, S., Guttag, J., Hall, A., Henzinger, T., Holzmann, G., Jones, C., Kurshan, R., Leveson, N., McMillan, K., Moore, J., Peled, D., Pnueli, A., Rushby, J., Shankar, N., Sifakis, J., Sistla, P., Steffen, B.,Wolper, P.,Woodcock, J., Zave, P. (1996): ‘Formal methods: state of the art and future directions’, ACM Computing Surveys 28(4), 626–643.
[27] Clarke, E.,Wing, J. M. (1996): ‘Formal methods: State-of-the-art and future directions’, ACM Comput. Surv. 28(4), 626—-643. Report by theWorking Groupon Formal Methods for the ACMWorkshop on Strategic Directions in Computing Research.
[28] Coe, T., Mathisen, T., Moler, C., Pratt, V. (1995): ‘Computational aspects of the pentium affair’, IEEE Comput. Sci. Eng. 2(1), 18–31.
[29] Connelly, R., Gousie, M. B., Hadimioglu, H., Ivanov, L., Hoffman, M. (2004):‘The role of digital logic in the computer science curriculum’, Journal of Computing Sciences in Colleges 19, 5–8.
[30] Courcoubetis, C., M. Yannakakis, M. (1988): Verifying temporal properties of ﬁnite state probabilistic programs, in ‘Proc. 29th Annual Symposium on Foundations of Computer Science (FOCS’88)’, IEEE Computer Society Press, pp. 338—-345.
[31] Daskalopulu, A. (2000): Model checking contractual protocols, in J. Breuker, R. Leenes, R. Winkels, eds, ‘Legal Knowledge and Information Systems’, JURIX 2000: The 13th Annual Conference, IOS Press, Amsterdam, pp. 35–47.
[32] Dijkstra, E. W. (1968): Notes on structured programming, in E. W. D. O.- J. Dahl, C. A. R. Hoare, eds, ‘Structured Programming’, Academic Press, London, pp. 1–82.
[33] Dijkstra, E. W. (1989): In reply to comments. EWD1058.
[34] Dill, D. L. (1996): The murf veriﬁcation system, in R. Alur, T. Henzinger, eds, ‘Proceedings of the 8th International Conference on Computer Aided Veriﬁcation (CAV ’96)’, Vol. 1102 of Lecture Notes in Computer Science, Springer-Verlag, New Brunswick, NJ, pp. 390—-393.
[35] Dill, D. L., Drexler, A. L., Hu, A. J., Yang, C. H. (1992): Protocol veriﬁcation as a hardware design aid, in ‘Proceedings of the 1992 IEEE International Conference on Computer Design: VLSI in Computer and Processors (ICCD’92)’, IEEE Computer Society, Cambridge, MA, pp. 522–525.
[36] Emerson, E. A. (2008): The beginning of model checking: A personal perspective, in DBLP:conf/spin/5000, pp. 27–45.
[37] Floyd, R. W. (1967): Assigning meanings to programs, in J. T. Schwartz, ed., ‘Mathematical Aspects of Computer Science. Proceedings of Symposia in Applied Mathematics’, Vol. 19, American Mathematical Society, Providence, pp. 19–32.
[38] Giunchig lia, F., Traverso, P. (1999): Planning as model checking, in ‘Proceedings of the Fifth European Workshop on Planning, (ECP’99)’, Springer, pp. 1–20.
[39] Gordon, M., Melham, T. (1993): Introduction to HOL: A Theorem Proving Environment for Higher Order Logic, Cambridge University Press.
[40] Grumberg, O., Veith, H., eds (2008): 25 Years of Model Checking - History, Achievements, Perspectives, Vol. 5000 of Lecture Notes in Computer Science, Springer.
[41] Hansson, H., Jonsson, B. (1994): ‘A logic for reasoning about time and reliability’, Formal Aspects of Computing 6, 512–535.
[42] Hasle, P. F. V., Øhrstrøm, P. (2004): Foundations of temporal logic. TheWWW-site for Arthur Prior, http://www.kommunikation.aau.dk/prior/index2.htm.
[43] Heath, J., Kwiatowska, M., Norman, G., Parker, D., Tymchysyn, O. (2006): Probabalistic model checking of complex biological pathways, in C. Priami, ed., ‘Proc. Comp. Methods in Systems Biology, (CSMB’06)’, Vol. 4210 of Lecture Notes in Bioinformatics, Springer, pp. 32–47.
[44] Henzinger, T., Ho, P., Wong-Toi, H. (1997): ‘A model checker for hybrid systems’, Int. J. Softw. Tools Technol. Transfer 1(1/2), 110–122.
[45] Henzinger, T., Jhala, R., Majumdar, R., Sutre, G. (2003): Software veriﬁcation with BLAST, in T. Ball, S. Rajamani, eds, ‘Model Checking Software: Proceedings of the 10th International SPIN Workshop (SPIN 2003)’, Vol. 2648 of Lecture Notes in Computer Science, Springer-Verlag, Portland, OR, pp. 235–239.
[46] Hermanns, H., Katoen, J.-P., Meyer-Kayser, J., Siegle, M. (2000): A Markov chain model checker, in ‘Tools and Algorithms for Construction and Analysis of Systems’, pp. 347—-362.
[47] Hillston, J. (1996): A Compositional Approach to Performance Modeling, Distinguished Dissertations in Computer Science, Cambridge University Press, Cambridge, UK.
[48] Hoare, C. A. R. (1969): ‘An axiomatic basis for computer programming’, Communications of the ACM 12(10), 576–580,583. Równie˙ z w: [49, 45–58].
[49] Hoare, C. A. R., Jones, C. B. (1989): Essays in Computing Science, Prentice Hall.
[50] Holzmann, G. (1991): Design and validation of computer protocols, Prentice Hall, New Jersey.
[51] Holzmann, G. J. (2002): Software analysis and model checking, in ‘CAV’, pp. 1–16.
[52] Holzmann, G. J., Smith, M. H. (2002): FEAVER 1.0 user guide, Technical re- port, Bell Labs. 64 pgs.
[53] Holzmann, G., Smith, M. (1999): A practical method for the veriﬁcation of event-driven software, in ‘Proceedings of the 21st International Conference on Software engineering (ICSE ’99), Los Angeles, CA’, ACM Press, New York, pp. 597–607.
[54] Holzmann, G., Smith,M. (1999): Software model checking. Extracting veriﬁcation models from source code, in J.W. et al., ed., ‘Proceedings of the Joint International Conference on Formal Description Techniques for Distributed Systems and Communication Protocols and Protocol Speciﬁcation, Testing and Veriﬁcation (FORTE/PSTV ’99)’, Vol. 156, International Federation for Information Processing, Kluwer, Beijing, China, pp. 481–497.
[55] Hughes, G. E., Cresswell, M. J. (1968): An Introduction to Modal Logic, Methuen and Co., London.
[56] Huth, M. R. A., D., R. M. (2000): Logic in Computer Science: Modelling and Reasoning about Systems, Cambridge University Press.
[57] Iosif, R., Sisto, R. (1999): dspin: A dynamic extension of spin, in D. D. et al., ed., ‘Proceedings of the 5th and 6th International SPIN Workshops’, Vol.1680 of Lecture Notes in Computer Science, Springer-Verlag, Trento, Italy and Toulouse, France, pp. 20–33.
[58] Katoen, J.-P., Khattri, M., Zapreev, I. S. (2005): A Markov reward model checker, in ‘Quantitative Evaluation of Systems (QEST)’, pp. 243—-244.
[59] Kaufmann,M.,Moore, J. S. (2004): ‘Some key research problems in automated theorem proving for hardware and software veriﬁcation’, Rev. R. Acad. Cien. Serie A. Mat. 98(1), 181—-196.
[60] Kautz, H., Selman, B. (1992): Planning as satisﬁability, in ‘ECAI ’92: Proceedings of the 10th European conference on Artiﬁcial intelligence’, John Wiley & Sons, Inc., New York, NY, USA, pp. 359–363.
[61] Kröger, F. (1977): ‘A logic of algorithmic reasoning’, Acta Informatica 8(3), 243–266.
[62] Kröger, F. (1987): Temporal Logic of Programs, Springer-Verlag New York, Inc., New York, NY, USA.
[63] Kröger, F., Merz, S. (1991): ‘Temporal logic and recursion’, Fundam. Inform. 14(2), 261–281.
[64] Kröger, F., Merz, S. (2008): Temporal Logic and State Systems, Springer.
[65] Kuntz, M., Siegle, M., Werner, E. (2004): Symbolic performance and dependability evaluation with the tool CASPA.
[66] Kurshan, R. (1995): Computer-Aided Veriﬁcation of Coordinating Processes: The Automata-Theoretic Approach, Princeton Series in Computer Science, Princeton University Press, Princeton, NJ.
[67] Kwiatkowska, M., Norman, G., Parker, D. (2001): PRISM: Probabilistic symbolic model checker, in P. Kemper, ed., ‘Proc. Tools Session of Aachen 2001’, International Multiconference on Measurement, Modelling and Evaluation of Computer-Communication Systems, Dortmund, pp. 7–12. Available as Technical Report 760/2001, University of Dortmund.
[68] Kwiatkowska,M., Norman, G., Parker, D. (2002): Probabilistic symbolic model checking with PRISM: A hybrid approach, in J.-P. Katoen, P. Stevens, eds, ‘Proc. 8th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS’02)’, Vol. 2280 of Lecture Notes in Computer Science, Springer, pp. 56–66.
[69] Kwiatkowska,M., Norman, G., Parker, D. (2002): Probabilistic symbolic model checking with PRISM, in J. Katoen, P. Stevens, eds, ‘Proceedings of the 8th International Conference on Tools and Algorithms for Construction and Analysis of Systems (TACAS 2002)’, Vol. 2280 of Lecture Notes in Computer Science, Springer-Verlag, Grenoble, France, pp. 52–66. Held as part of the Joint European Conference on Theory and Practice of Software (ETAPS 2002).
[70] Larson, K., Pettersson, P., Yi, W. (1997): ‘Uppaal in a nutshell’, Int. J. Softw.Tools. Technol. Transfer 1(1/2), 134–152.
[71] M. Kaufmann, M., Manolios, P., Moore, J. S. (2000): Computer-Aided Reasoning: An Approach, Kluwer Academic Press, Boston.
[72] Manna, Z., A. Pnueli, A. (1992, 1995): The Temporal Logic of Reactive and Concurrent Systems, Vol. 1: Speciﬁcation, 2: Safety, Springer-Verlag, New York.
[73] Manna, Z., Bjørner, N., Browne, A., Chang, E., Alfaro, L. D., Devarajan, H., Kapur, A., Lee, J., Sipma, H. (1994): STEP: The stanford temporal prover, Technical report, Computer Science Department, Stanford University Stanford, CA.
[74] Manna, Z., Waldinger, R. (1985): The Logical Basis for Computer Programming, Addison-Wesley.
[75] McMillan, K. L. (1993): Symbolic Model Checking: An approach to the State Explosion Problem, Kluwer Academic, Hingham, MA.
[76] Miller, A., Donaldson, A., Calder, M. (2006): ‘Symmetry in temporal logic model checking’, ACM Computing Surveys 38(3).
[77] Naur, P. (1966): ‘Proof of algorithms by general snapshots’, BIT 6(4), 310–316.
[78] Owicki, S. S., Lamport, L. (1982): ‘Proving liveness properties of concurrent programs’, ACM Trans. Program. Lang. Syst. 4(3), 455–495.
[79] Pnueli, A. (1977): The temporal logic of programs, in ‘Proceedings of the 18th IEEE-CS Symposium on Foundation of Computer Science (FOCS-77)’, IEEE Computer Society Press, pp. 46–57.
[80] Pnueli, A. (1981): ‘The temporal semantics of concurrent programs’, Theoretical Comput. Sci. 13, 45–60.
[81] Pratt, V. R. (1980): ‘Applications of modal logic to programming’, Studia Logica 9, 257–274.
[82] Queille, J.-P., Sifakis, J. (1982): Speciﬁcation and veriﬁcation of concurrent systems in CESAR, in ‘Proceedings 5th International Symposium on Programming’, Vol. 137 of Lecture Notes in Computer Science, Springer-Verlag, pp. 337–351.
[83] Randell, B. (1973): The Origin of Digital Computers, Springer Verlag.
[84] Rescher, N., Urquhart, A. (1971): Temporal Logic, Springer, Wien, New York.
[85] Rutten, J., Kwiatkowska, M., Norman, G., Parker, D. (2004): Mathematical Techniques for Analysing Concurrent and Probabilisitic Systems, Vol. 23 of American Mathematical Society, CRM Monograph Series, Centre de Recherches Mathématiques, Université de Montréal.
[86] Schneider, K. (2003): Veriﬁcation of Reactive Systems. Formal Methods and Algorithms, Texts in Theoretical Computer Science (EATCS Series), Springer-Verlag.
[87] Schnoebelen, P. (2002): ‘The complexity of temporal logic model checking’, Advances in Modal Logic 4, 1–44.
[88] Turing, A. M. (1936–37): ‘On computable numbers, with an application to the Entscheidungsproblem’, Proceedings of the London Mathematical Society 42(Series 2), 230–265. Received May 25, 1936; Appendix added August 28; read November 12, 1936; corrections Ibid. vol. 43(1937), pp. 544–546. Turing’s paper appeared in Part 2 of vol. 42 which was issued in December 1936 (Reprint in: [89]; 151–154). Online version: http://www.abelard.org/ turpap2/tp2-ie.asp.
[89] Turing, A. M. (1965): On computable numbers, with an application to the Entscheidungsproblem, in M. Davis, ed., ‘The Undecidable’, Raven Press, Hewlett, NY, pp. 116–151.
[90] Vaandrager F.W.and De Nicola, R. (1990): Actions versus state based logics for transition systems, in ‘Proc. Ecole de Printemps on Semantics of Concurrency’, Vol. 469 of Lecture Notes in Computer Science, Springer, pp. 407—-419.
[91] Wang, W., Hidvegi, Z., Bailey, A., Whinston, A. (2000): ‘E-process design and assurance using model checking’, IEEE Computer 33(10), 48–53.
[92] Yovine, S. (1997): ‘Kronos: A veriﬁcation tool for real-time systems’, Int. J. Softw. Tools Technol. Transfer 1(1/2), 123–133.

Typ dokumentu

Bibliografia

Identyfikator YADDA

bwmeta1.element.baztech-article-BPB2-0036-0017