Advertisement

Foundations of Heterogeneous Specification

  • Till Mossakowski
Part of the Lecture Notes in Computer Science book series (LNCS, volume 2755)

Abstract

We provide a semantic basis for heterogeneous specifications that not only involve different logics, but also different kinds of translations between these. We show that Grothendieck institutions based on spans of (co)morphisms can serve as a unifying framework providing a simple but powerful semantics for heterogeneous specification.

Keywords

Linear Temporal Logic Label Transition System Logical Framework Computation Tree Logic Abstract Data Type 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. 1.
    Alagi, S.: Institutions: integrating objects, XML and databases. Information and Software Technology 44, 207–216 (2002)CrossRefGoogle Scholar
  2. 2.
    Arrais, M., Fiadeiro, J.L.: Unifying theories in different institutions. In: Haveraaen, M., Dahl, O.-J., Owe, O. (eds.) Abstract Data Types 1995 and COMPASS 1995. LNCS, vol. 1130, pp. 81–101. Springer, Heidelberg (1996)CrossRefGoogle Scholar
  3. 3.
    Astesiano, E., Cerioli, M.: Relationships between logical frameworks. In: Bidoit, M., Choppy, C. (eds.) Abstract Data Types 1991 and COMPASS 1991. LNCS, vol. 655, pp. 126–143. Springer, Heidelberg (1993)CrossRefGoogle Scholar
  4. 4.
    Autexier, S., Hutter, D., Mantel, H., Schairer, A.: Towards an evolutionary formal software-development using Casl. In: Bert, D., Choppy, C., Mosses, P.D. (eds.) WADT 1999. LNCS, vol. 1827, pp. 73–88. Springer, Heidelberg (2000)CrossRefGoogle Scholar
  5. 5.
    Bidoit, M., Hennicker, R.: Using an institution encoding for proving consequences of structured COL-specifications. Talk at the WADT 2002, Frauenchiemsee (2002)Google Scholar
  6. 6.
    Borzyszkowski, T.: Logical systems for structured specifications. Theoretical Computer Science 286, 197–245 (2002)MathSciNetCrossRefzbMATHGoogle Scholar
  7. 7.
    Brinksma, E. (ed.): Information processing systems — open systems interconnection. LOTOS: a formal description technique based on the temporal ordering of observational behaviour (1988); International Standard ISO 8807Google Scholar
  8. 8.
    Cerioli, M.: Relationships between Logical Formalisms. PhD thesis, TD-4/93, Università di Pisa-Genova-Udine (1993)Google Scholar
  9. 9.
    Cerioli, M., Meseguer, J.: I borrow your logic (transporting logical structures along maps). Theoretical Computer Science 173, 311–347 (1997)MathSciNetCrossRefzbMATHGoogle Scholar
  10. 10.
    CoFI. The Common Framework Initiative for algebraic specification and development, electronic archives. Notes and Documents accessible from http://www.cofi.info
  11. 11.
    CoFI Semantics Task Group. Casl – The CoFI Algebraic Specification Language – Semantics. Note S-9 (Documents/CASL/Semantics, version 0.96). In: [10] (July 1999)Google Scholar
  12. 12.
    Diaconescu, R.: Grothendieck institutions. Applied categorical structures 10, 383–402 (2002)MathSciNetCrossRefzbMATHGoogle Scholar
  13. 13.
    Diaconescu, R., Futatsugi, K.: Logical foundations of CafeOBJ. Theoretical computer science 285, 289–318 (2002)MathSciNetCrossRefzbMATHGoogle Scholar
  14. 14.
    Diaconescu, R., Goguen, J., Stefaneas, P.: Logical support for modularisation. In: Huet, G., Plotkin, G. (eds.) Proceedings of a Workshop on Logical Frameworks (1991)Google Scholar
  15. 15.
    Durán, F., Meseguer, J.: Structured theories and institutions. In: Hofmann, M., Rosolini, G., Pavlovic, D. (eds.) CTCS 1999 Conference on Category Theory and Computer Science. ENTCS 29 (1999)Google Scholar
  16. 16.
    Ehrig, H., Mahr, B.: Fundamentals of Algebraic Specification 2. Springer, Heidelberg (1990)CrossRefzbMATHGoogle Scholar
  17. 17.
    Emerson, E.A.: Temporal and Modal Logic. In: van Leeuwen, J. (ed.) Handbook of Theoretical Computer Science, vol. B. Elsevier / MIT Press (1990)Google Scholar
  18. 18.
    Ghribi, B., Logrippo, L.: A validation environment for LOTOS. In: Protocol Specification, Testing and Verification, pp. 93–108 (1993)Google Scholar
  19. 19.
    Gibson, P., Mermet, B., Mery, D.: Feature interactions: A mixed semantic model approach. In: IWFM (1997)Google Scholar
  20. 20.
    Goguen, J., Rosu, G.: Institution morphisms. Formal aspects of computing 13, 274–307 (2002)CrossRefzbMATHGoogle Scholar
  21. 21.
    Goguen, J.A., Burstall, R.M.: Institutions: Abstract model theory for specification and programming. Journal of the Association for Computing Machinery 39, 95–146 (1992); Predecessor in: LNCS, vol. 164, pp. 221–256 (1984)MathSciNetCrossRefzbMATHGoogle Scholar
  22. 22.
    Goguen, J.A., Tracz, W.: An implementation-oriented semantics for module composition. In: Leavens, G.T., Sitaraman, M. (eds.) Foundations of Component-Based Systems. ch. 11, pp. 231–263. Cambridge University Press, New York (2000)Google Scholar
  23. 23.
    Hoare, C.A.R.: Communicating Sequential Processes. Prentice-Hall, Englewood Cliffs (1985)zbMATHGoogle Scholar
  24. 24.
    Kreowski, H.-J., Mossakowski, T.: Equivalence and difference of institutions: Simulating Horn clause logic with based algebras. Mathematical Structures in Computer Science 5, 189–215 (1995)MathSciNetCrossRefzbMATHGoogle Scholar
  25. 25.
    Martí-Oliet, N., Meseguer, J.: From abstract data types to logical frameworks. In: Reggio, G., Astesiano, E., Tarlecki, A. (eds.) Abstract Data Types 1994 and COMPASS 1994. LNCS, vol. 906, pp. 48–80. Springer, Heidelberg (1995)CrossRefGoogle Scholar
  26. 26.
    Meseguer, J.: General logics. In: Logic Colloquium 87, pp. 275–329. North-Holland, Amsterdam (1989)Google Scholar
  27. 27.
    Meseguer, J.: Conditional rewriting as a unified model of concurrency. Theoretical Computer Science 96(1), 73–156 (1992)MathSciNetCrossRefzbMATHGoogle Scholar
  28. 28.
    Mossakowski, T.: Equivalences among various logical frameworks of partial algebras. In: Kleine Büning, H. (ed.) CSL 1995. LNCS, vol. 1092, pp. 403–433. Springer, Heidelberg (1996)CrossRefGoogle Scholar
  29. 29.
    Mossakowski, T.: Comorphism-based Grothendieck logics. In: Diks, K., Rytter, W. (eds.) MFCS 2002. LNCS, vol. 2420, pp. 593–604. Springer, Heidelberg (2002)CrossRefGoogle Scholar
  30. 30.
    Mossakowski, T.: Heterogeneous development graphs and heterogeneous borrowing. In: Nielsen, M., Engberg, U. (eds.) FOSSACS 2002. LNCS, vol. 2303, pp. 326–341. Springer, Heidelberg (2002)CrossRefGoogle Scholar
  31. 31.
    Mossakowski, T.: Relating Casl with other specification languages: the institution level. Theoretical Computer Science 286, 367–475 (2002)MathSciNetCrossRefzbMATHGoogle Scholar
  32. 32.
    Mossakowski, T., Autexier, S., Hutter, D.: Extending development graphs with hiding. In: Hussmann, H. (ed.) FASE 2001. LNCS, vol. 2029, pp. 269–283. Springer, Heidelberg (2001)CrossRefGoogle Scholar
  33. 33.
    Kolyang, T.M., Krieg-Brückner, B.: Static semantic analysis and theorem proving for Casl. In: Parisi-Presicce, F. (ed.) WADT 1997. LNCS, vol. 1376, pp. 333–348. Springer, Heidelberg (1998)CrossRefGoogle Scholar
  34. 34.
    Mosses, P.D.: CoFI: The Common Framework Initiative for Algebraic Specification and Development. In: Bidoit, M., Dauchet, M. (eds.) CAAP 1997, FASE 1997, and TAPSOFT 1997. LNCS, vol. 1214, pp. 115–137. Springer, Heidelberg (1997)CrossRefGoogle Scholar
  35. 35.
    Reggio, G., Astesiano, E., Choppy, C.: Casl-LTL - a Casl extension for dynamic reactive systems - summary. Technical Report of DISI - Università di Genova,DISITR- 99-34, Italy (2000)Google Scholar
  36. 36.
    Roggenbach, M.: CSP-Casl – a new integration of process algebra and algebraic specification. Manuscript, Bremen, submitted for publicationGoogle Scholar
  37. 37.
    Roggenbach, M., Mossakowski, T.: The Csp-Casl institution and its relation to temporal logic. Manuscript, University of BremenGoogle Scholar
  38. 38.
    Roscoe, A.: The Theory and Practice of Concurrency. Prentice-Hall, Englewood Cliffs (1997)Google Scholar
  39. 39.
    Salibra, A., Scollo, G.: A soft stairway to institutions. In: Bidoit, M., Choppy, C. (eds.) Proc. 8th ADT workshop. LNCS, vol. 655, pp. 310–329. Springer, Heidelberg (1992)Google Scholar
  40. 40.
    Salibra, A., Scollo, G.: Interpolation and compactness in categories of preinstitutions. Mathematical Structures in Computer Science 6(3), 261–286 (1996)MathSciNetCrossRefzbMATHGoogle Scholar
  41. 41.
    Sannella, D., Tarlecki, A.: Working with multiple logical systems. In: Foundations of Algebraic Specifications and Formal Program Development. ch. 10. Cambridge University Press, Cambridge (to appear), See http://zls.mimuw.edu.pl/~tarlecki/book/index.html
  42. 42.
    Sannella, D., Tarlecki, A.: Specifications in an arbitrary institution. Information and Computation 76, 165–210 (1988)MathSciNetCrossRefzbMATHGoogle Scholar
  43. 43.
    Sannella, D., Tarlecki, A.: Toward formal development of programs from algebraic specifications: implementations revisited. Acta Inf. 25, 233–281 (1988)MathSciNetCrossRefzbMATHGoogle Scholar
  44. 44.
    Scollo, G.: On the engineering of logics. PhD thesis, University of Twente, Enschede (1993)Google Scholar
  45. 45.
    Tarlecki, A.: Institution representation. draft note (1987)Google Scholar
  46. 46.
    Tarlecki, A.: Moving between logical systems. In: Haveraaen, M., Dahl, O.-J., Owe, O. (eds.) Abstract Data Types 1995 and COMPASS 1995. LNCS, vol. 1130, pp. 478–502. Springer, Heidelberg (1996)CrossRefGoogle Scholar
  47. 47.
    Tarlecki, A.: Towards heterogeneous specifications. In: Gabbay, D., Rijke, M.d. (eds.) Frontiers of Combining Systems 2, 1998. Studies in Logic and Computation, pp. 337–360. Research Studies Press, Hertfordshire (2000)Google Scholar
  48. 48.
    Wolter, U., Didrich, K., Cornelius, F., Klar, M., Wessäly, R., Ehrig, H.: How to cope with the spectrum of spectrum. In: Jähnichen, S., Broy, M. (eds.) KORSO 1995. LNCS, vol. 1009, pp. 173–189. Springer, Heidelberg (1995)CrossRefGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2003

Authors and Affiliations

  • Till Mossakowski
    • 1
  1. 1.BISS, Dept. of Computer ScienceUniversity of BremenGermany

Personalised recommendations