Compositionality for Tightly Coupled Systems: A New Application of the Propositions-as-Types Interpretation

• Autorzy: Stehr M-O.
• Języki publikacji: EN

Abstrakty

EN

The design of complex software systems fundamentally relies on the understanding of abstract components and their interactions. Although compositional techniques are being successfully employed in practice, the use of such techniques is often rather informal and intuitive, and typically a justification for correct behaviour of the composed system exists but is not expressed explicitly. In this paper, we show what can be gained from treating such justifications as first-class citizens. The fairly general setting for this paper is a formal development of a UNITY-style temporal logic for labeled transition systems in the calculus of inductive constructions which has been conducted using the Coq proof assistant in a formally rigorous way. Our development not only subsumes the original UNITY approach to program verification and the more recent approach of New UNITY, but goes beyond it in several essential aspects, such as the generality of the program/system model (arbitrary labeled transition systems instead of UNITY programs), the notion of fairness (weak group fairness instead of unconditional fairness), and the issue of compositionality (not only for safety but also for liveness assertions). The last aspect, which we feel is crucial in the foundations for software engineering, is subject of this paper. We present a general proof rule for compositional verification of liveness assertions in tightly coupled systems. It relies on a notion of compositional proofs, which in turn is closely related to classical work on interference-free proofs for parallel programs. The formulation of this new proof rule and the verification of its soundness does not only exploit the strong inductive reasoning capabilities of the calculus of inductive constructions, but it also uses the propositions-as-types interpretation and the associated proofs-as-objects interpretation in an essential way.

• Wydawca: IOS Press
• Czasopismo: Fundamenta Informaticae
• Rocznik: 2008
• Tom: Vol. 82, nr 4
• Strony: 311--340
• Opis fizyczny: bibliogr. 57 poz.

Twórcy

autor

Stehr M-O.

• SRI International, Computer Science Laboratory, 333 Ravenswood Avenue, Menlo Park, CA 94025, USA,

Bibliografia

• [1] Alpern, B., Schneider, F. B.: Defining Liveness, Information Processing Letters, 21, 1985, 181-185.
• [2] Andersen, F., Petersen, K. D., Pettersson, J. S.: Program verification using HOL-UNITY, Higher Order Logic Theorem Proving and its Applications: 6th InternationalWorkshop, HUG'93, Vancouver, B.C., August 11-13 1993, Proceedings (J. J. Joyce, C.-J. H. Segar, Eds.), 780, Springer-Verlag, 1994.
• [3] Apt, K. R., Olderog, E.-R.: Verification of Sequential and Concurrent Programs, Graduate Texts in Computer Science, Springer-Verlag, 1997.
• [4] Barras, B., Boutin, S., Cornes, C., Courant, J., Coscoy, Y., Delahaye, D., de Rauglaudre, D., Filliatre, J. C. ., Giménez, E., Herbelin, H., Huet, G., Laulh`ere, H., Mu˜noz, C., Murthy, C., Parent-Vigouroux, C., Loiseleur, P., Paulin, C., Sa¨ıbi, A., Werner, B.: The Coq Proof Assistent Reference Manual, Version 6.3.1, Coq Project, Technical report, INRIA, 1999, http://logical.inria.fr/.
• [5] Carpentier, M., Chandy, K. M.: Towards a compositional approach to the design and verification of distributed systems, FM'99 - Formal Methods, World Congress on Formal Methods in the Development of Computing Systems, Toulouse, France, September 1999. Proceedings, Volume I (J. M. Wing, J. Wookcock, J. Davies, Eds.), 1708, Springer-Verlag, 1999.
• [6] Chandy, K. M., Misra, J.: Parallel Program Design. A Foundation, Addison-Wesley, 1988.
• [7] Chandy, K. M., Misra, J.: Proofs of Distributed Algorithms: An Exercise, in: Developments in Concurrency and Communication (C. A. R. Hoare, Ed.), chapter 11, Addison-Wesley, Reading, Massachusetts, 1990, 305-332.
• [8] Chetali, B.: Formal verification of concurrent programs using the Larch prover, Proceedings of the Workshop on Tools and Algorithms for the Construction and Analysis of Systems, Aarhus, Denmark, 19-20 May, 1995 (U. H. Engberg, K. G. Larsen, A. Skou, Eds.), BRICS, University of Aarhus, Aarhus, Denmark, 1995.
• [9] Chetali, B.: Formal verification of concurrent programs using the Larch prover, IEEE Transactions on Software Engineering, 24(1), 1998, 46-62.
• [10] Chetali, B., Heyd, B.: Formal Verification of Concurrent Programs in LP and in Coq: A Comparative Analysis, Theorem Proving in Higher Order Logics, 10th International Conference, TPHOLs'97, Murray Hill, NJ, USA, August 19-22, 1997, Proceedings (E. L. Gunter, A. Felty, Eds.), 1275, Springer-Verlag, 1997.
• [11] Collette, P., Knapp, E.: A foundation for modular reasoning about safety and progress properties of statebased concurrent programs, Theoretical Computer Science, 183, 1997, 253-279.
• [12] Coquand, T.: On the analogy between propositions and types, in: Logical Foundations of Functional Programming (G. Huet, Ed.), The UT year of programming series, Addison-Wesley, 1990.
• [13] Desel, J., Gomm, D., Kindler, E., Walter, R., Paech, B.: Bausteine eines kompositionalen Beweiskalk¨uls für netzmodellierte Systeme, SFB-Bericht 342/16/92A, Technische Universit¨atM¨unchen, Institut f¨ur Informatik, 1992.
• [14] Francez, N.: Fairness, Springer-Verlag, 1986.
• [15] Gerth, R., Pnueli, A.: Rooting UNITY, Proceedings Fifth International Workshop on Software Specification and Design, Pittsburgh, Pennsylvania,May 1989.
• [16] Geuvers, H.: Logics and Type Systems, Ph.D. Thesis, University of Nijmegen, 1993.
• [17] Goldschlag, D. M.: Mechanically verifying concurrent programs with the Boyer-Moore prover, IEEE Transactions on Software Engineering, 16(9), 1990.
• [18] Goldschlag, D. M.: Mechanically Verifying Safety and Liveness Properties of Delay Insensitive Circuits, Computer Aided Verification, 3rd International Workshop, CAV '91, Aalborg, Denmark, July 1-4, 1991, Proceedings (K. G. Larsen, A. Skou, Eds.), 575, Springer-Verlag, July 1992.
• [19] Heyd, B.: Application de la théorie des types et du démonstrateur Coq á la vérification de programmes parallèlles, Ph.D. Thesis, Universit´e Henri Poincaré - Nancy 1, 1997.
• [20] Heyd, B., Crégut, P.: A modular coding of UNITY in Coq, Theorem Proving in Higher Order Logics, 9th International Conference, TPHOLs'96, Turku, Finland, August 26-30, 1996, Proceedings (J. von Wright, J. Grundy, J. Harrison, Eds.), 1125, Springer-Verlag, 1996.
• [21] Heyting, A.: Intuitionism - An Introduction, Studies in Logic and the Foundations of Mathematics, North-Holland, 1971.
• [22] Howard, W. A.: The formulae-as-types notion of construction, in: To H.B. Curry: Essays on Combinatory Logic (J. Hindley, J. Seldin, Eds.), Academic Press, 1980.
• [23] Kindler, E.: Invariants, Composition, and Substitution, Acta Informatica, 32(4), 1995, 299-312.
• [24] Kindler, E., Reisig,W.: Algebraic system nets for modelling distributed algorithms, Petri Net Newsletter, 51, December 1996, 16-31.
• [25] Knapp, E.: Derivation of Concurrent Programs, Sci. Comput. Programming, 19, 1992, 1-23.
• [26] Knapp, E.: Soundness and Completeness of UNITY logic, Foundations of Software Technology and Theoretical Computer Science, 14th Conference, Madras, India, December 15-17, 1994, Proceedings (P. S. Thiagarajan, Ed.), 880, Springer-Verlag, 1994.
• [27] Lamport, L.: Proving the Correctness of Multiprocess Programs, IEEE Transactions on Software Engineering, SE-3(2), 1977, 126-143.
• [28] Lamport, L.: Win and sin: predicate transformers for concurrency, ACM Transactions on Programming Languages and Systems, 12, 1990, 396-428.
• [29] Lamport, L.: The temporal logic of actions, ACM Transactions on Programming Languages and Systems, 16(3),May 1994, 872-923.
• [30] Mackenthun, R., Valk, R.: Verifying coloured nets in UNITY-style, Fachbereichsmitteilung FBI-HH-M-222/93, Universit¨at Hamburg, 1991.
• [31] Manna, Z., Pnueli, A.: The Temporal Logic of Reactive and Concurrent Systems, Springer-Verlag, 1992.
• [32] McCann, P. J., Roman, G.-C.: Mobile UNITY Coordination Constructs applied to Packet Forwarding for Mobile Hosts, Coordination Languages and Models, 1282, Springer-Verlag, Berlin, 1997.
• [33] Meseguer, J.: Conditional rewriting logic as a unified model of concurrency, Theoretical Computer Science, 96, 1992, 73-155.
• [34] Misra, J.: A Simple Proof of a Simple Consensus Algorithm, in: Beauty is Our Business, chapter 35, Springer-Verlag, New York, 1990, 312-318.
• [35] Misra, J.: Soundness of the Substitution Axiom,March 1990, Notes on UNITY, http://www.cs.utexas.edu/users/psp/notesunity.html.
• [36] Misra, J.: New UNITY, 1994, Manuscript, http://www.cs.utexas.edu/users/psp/newunity.html.
• [37] Misra, J.: A logic for Concurrent Programming: Safety and Progress, Journal of Computer and Software Engineering, 3(2), 1995, 239-300.
• [38] Misra, J.: A discipline of multiprogramming: programming theory for distributed applications, vol. 18 of Monographs in Computer Science, Springer-Verlag, 2001.
• [39] Owicki, S., Gries, D.: Verifying properties of parallel programs: an axiomatic approach, Communications of the ACM, 19, May 1976, 279-285.
• [40] Pachl, J.: A simple proof of a completeness result for leads-to in the UNITY logic, Technical Report RZ 2060, IBM Research Division, Zurich Research Laboratory, 1990.
• [41] Pachl, J.: A Simple Proof of a Completeness Result for leads-to in the UNITY Logic, Information Processing Letters, 41, 1992.
• [42] Paulin-Mohring, C.: Inductive Definitions in the system Coq - Rules and Properties, Typed Lambda Calculi and Applications, International Conference, TLCA '93, Utrecht, The Netherlands, March 16-18, 1993, Proceedings (M. Bezem, J. . F. Groote, Eds.), 664, Springer Varlag, 1993.
• [43] Paulson, L. C.: Mechanizing UNITY in Isabelle, ACM Transactions on Computational Logic, 1(1), 2000, 3-32.
• [44] Pettersson, J. S.: Comments on "Always-True is not Invariant": Assertional Reasoning About Invariance, Information Processing Letters, 40(5), 1991, 231-233.
• [45] Prasetya, I. S. W. B.: Error in the UNITY Substitution Rule for Subscripted Operators, Formal Aspects of Computing, 6, 1994, 466-470.
• [46] Reichwein, G., Fiadeiro, J. L.: Models for the Substitution Axiom of UNITY Logic, Information Processing Letters, 48(4), 1993, 171-176.
• [47] Reisig, W.: Elements of Distributed Algorithms: Modeling and Analysis with Petri Nets, Springer-Verlag, 1998.
• [48] Sanders, B. A.: Eliminating the Substitution Axiom from UNITY Logic, Formal Aspects of Computing, 3, 1991, 189-205.
• [49] Shankar, A. U.: An introduction to assertional reasoning for concurrent systems, ACM Computing Surveys, 25(3), 1993, 226-262.
• [50] Shankar, N.: A Lazy Approach to Compositional Verification, Compositionality: The Significant Difference, International Symposium, COMPOS'97, Bad Malente, Germany, September 8-12, 1997, Revised Lectures (W. P. de Roever, H. Langmaack, A. Pnueli, Eds.), 1536, Springer-Verlag, 1998.
• [51] Singh, A. K., Overbeek, R.: Derivation of efficient parallel programs: An example from Genetic Sequence Analysis, International Journal of Parallel Programming, 18, 1989, 447-484.
• [52] Staskauskas, M. G.: Formal derivation of Concurrent Programs: an Example from Industry, IEEE Transactions on Software Engineering, 19, 1993, 503-528.
• [53] Stehr, M.-O.: Embedding UNITY into the Calculus of Inductive Constructions, Fachbereichsbericht FBIHH-B-214/98, University of Hamburg, Germany, September 1998.
• [54] Stehr,M.-O.: Programming, Specification, and Interactive Theorem Proving - Towards a Unified Language based on Equational Logic, Rewriting Logic, and Type Theory, Doctoral Thesis, Universit¨at Hamburg, Fachbereich Informatik, Germany, 2002, http://www.sub.uni-hamburg.de/disse/810/.
• [55] Stehr,M.-O.: Assertional Reasoning, in: Petri Nets for System Engineering - A Guide to Modeling, Verification, and Applications (C. Girault, R. Valk, Eds.), Springer-Verlag, 2004.
• [56] Swierstra, S. D., Lentfert, P. J. A., Uittenbogaard, A. H.: Distributed Incremental Maximum Finding in Hierarchicaly Divided Graphs, Technical Report RUU-CS-90-30, Utrecht University, September 1990.
• [57] Weber, M., Walter, R., V¨olzer, H., Vesper, T., Reisig, W., Peuker, S., Kindler, E., Freiheit, J., Desel, J.: DAWN: Petrinetzmodelle zur Verifikation Verteilter Algorithmen, Informatik-Bericht 88, Humboldt-Universtit¨at zu Berlin, 1997.