Skip to main content

Part of the book series: Lecture Notes in Computer Science ((LNCS,volume 3147))

Abstract

The specification and modelling of reasonably large software systems is usually a complex task that involves the description of several aspects or dimensions that are not easily described by means of a single specification technique or formalism. However, an obvious problem in this context is to know how can we be sure that these specifications are consistent and really model the system that we want to design. A second problem is how to verify or prove properties about these systems. In this paper, we will provide a formal framework that will allow us to reason about heterogeneous specifications and we will present some results concerning these two problems.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Astesiano, E., Kreoski, H.-J., Krieg Brueckner, B. (eds.): Algebraic Foundations for System Specification. IFIP State-of-the-art Reports. Springer, Heidelberg (1999)

    Google Scholar 

  2. Bidoit, M., Cengarle, M.V., Hennicker, R.: ch. 11: Proof Systems for Structured Specification and Their Refinement. In: [1] (1999)

    Google Scholar 

  3. Braatz, B., Klein, M., Schroeter, G.: Semantical Integration of Object-OrientedViewpoint Specification Methods. In: Ehrig, H., Damm, W., Desel, J., Große-Rhode, M., Reif, W., Schnieder, E., Westkämper, E. (eds.) INT 2004. LNCS, vol. 3147, pp. 602–626. Springer, Heidelberg (2004)

    Chapter  Google Scholar 

  4. Booch, G., Rumbaugh, J., Jacobson, I.: The Unified Modeling Language User Guide. Addison-Wesley, Reading (1998)

    Google Scholar 

  5. Cerioli, M., Meseguer, J.: I borrow your logic? Theoretical Computer Science 173, 311–347 (1997)

    Article  MATH  MathSciNet  Google Scholar 

  6. Diaconescu, R., Goguen, J.A., Stefaneas, P.: Logical support for modularisation. Report Prog. Res. Group, Oxford University (1991)

    Google Scholar 

  7. Ehrig, H., Mahr, B.: Fundamentals of Algebraic Specification 2: Module Specifications and Constraints. EATCS Monographs on Theor. Comp. Science, vol. 21. Springer, Berlin (1990)

    MATH  Google Scholar 

  8. Ehrig, H., Orejas, F.: Integration Paradigm for Data Type and Process Specification Techniques. Bulletin of the EATCS 65, 90–97 (1998)

    MATH  Google Scholar 

  9. Ehrig, H., Orejas, F., Braatz, B., Klein, M., Piirainen, M.: A Generic Component Framework for System Modeling. In: Kutsche, R.-D., Weber, H. (eds.) FASE 2002. LNCS, vol. 2306, pp. 33–48. Springer, Heidelberg (2002)

    Chapter  Google Scholar 

  10. Gaifman, H., Shapiro, E.: Fully abstract compositional semantics for logics programs. In: Proc. Sixteenth Annual ACM Symp. on Principles of Programming Languages, pp. 134–142 (1989)

    Google Scholar 

  11. Goguen, J.A., Burstall, R.M.: Institutions: Abstract model theory for specification and programming. Journal of the ACM 39(1), 95–146 (1992)

    Article  MATH  MathSciNet  Google Scholar 

  12. Große-Rhode, M.: Integrating Semantics for Object-Oriented System Models. In: Orejas, F., Spirakis, P.G., van Leeuwen, J. (eds.) ICALP 2001. LNCS, vol. 2076, pp. 238–255. Springer, Heidelberg (2001)

    Chapter  Google Scholar 

  13. M. Große-Rhode. Semantic integration of heterogeneous formal specifications via transformation systems. Habilitation Thesis. TU Berlin (2001)

    Google Scholar 

  14. Große-Rhode, M.: Semantic integration of heterogeneous software specifications. Springer, Heidelberg (2004)

    Google Scholar 

  15. Information processing systems - Open Systems Interconnection - LOTOS - A formal description technique based on the temporal ordering of observational behaviour. International Standard ISO 8807, ISO (1989)

    Google Scholar 

  16. Meseguer, J.: General logic. In: Ebbinghaus, H.-D., et al. (eds.) Logic Colloq. 1987, pp. 279–329. North Holland, Amsterdam (1998)

    Google Scholar 

  17. Meseguer, J.: Conditioned Rewriting Logic as a United Model of Concurrency. Theor. Comput. Sci. 96(1), 73–155 (1992)

    Article  MATH  MathSciNet  Google Scholar 

  18. 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)

    Chapter  Google Scholar 

  19. Navarro, M., Orejas, F., Sanchez, A.: On the correctness of modular systems. Theoretical Computer Science 140, 139–177 (1995)

    Article  MATH  MathSciNet  Google Scholar 

  20. Orejas, F.: Chapter 6: Structuring and Modularity. In: [1] (1999)

    Google Scholar 

  21. Orejas, F., Pino, E.: A general algebraic framework for studying modular systems. In: Bert, D., Choppy, C., Mosses, P.D. (eds.) WADT 1999. LNCS, vol. 1827, pp. 271–290. Springer, Heidelberg (2000)

    Chapter  Google Scholar 

  22. Orejas, F., Pino, E.: Heterogeneous Modular Systems. In: Proc. IDPT 2002, Pasadena (2002)

    Google Scholar 

  23. Orejas, F., Pino, E., Ehrig, H.: Institutions for logic programming. Theoretical Computer Science 173, 485–511 (1997)

    Article  MATH  MathSciNet  Google Scholar 

  24. Paulson, L.C.: Mechanizing UNITY in Isabelle. ACM Trans. Comput. Log. 1(1), 3–32 (2000)

    Article  MathSciNet  Google Scholar 

  25. Pino, E.: An Algebraic Study of Modularity in Logic Programming. PhD thesis, Dept. de Llenguatges i Sistemes Informàtics. Universitat Politècnica de Catalunya (1999), http://www.upc.lsi.es/~pino

  26. Reichel, H.: Initiallity restricting algebraic theories. In: Proc. Mathematical Foundations of Computer Science 1980. LNCS, vol. 88, pp. 504–514. Springer, Heidelberg (1980)

    Chapter  Google Scholar 

  27. Sannella, D.T., Tarlecki, A.: Toward formal development of ml programs: Foundations and methodology. In: Díaz, J., Orejas, F. (eds.) TAPSOFT 1989 and CCIPL 1989. LNCS, vol. 352, pp. 375–389. Springer, Heidelberg (1989)

    Google Scholar 

  28. 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)

    Google Scholar 

  29. Tarlecki, A.: Towards heterogeneous specifications. In: Proc. Workshop on Frontiers of Combining Systems FroCoS 1998. Applied Logic Series, Kluwer Academic Publishers, Dordrecht (1998)

    Google Scholar 

Download references

Author information

Authors and Affiliations

Authors

Editor information

Editors and Affiliations

Rights and permissions

Reprints and permissions

Copyright information

© 2004 Springer-Verlag Berlin Heidelberg

About this chapter

Cite this chapter

Orejas, F., Pino, E. (2004). On the Integration of Modular Heterogeneous Specifications. In: Ehrig, H., et al. Integration of Software Specification Techniques for Applications in Engineering. Lecture Notes in Computer Science, vol 3147. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-27863-4_31

Download citation

  • DOI: https://doi.org/10.1007/978-3-540-27863-4_31

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-23135-6

  • Online ISBN: 978-3-540-27863-4

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics