On certification of specifications for TROLL light objects | SpringerLink
Skip to main content
Springer Nature Link
Log in

On certification of specifications for TROLL light objects

  • Contributed Papers
  • Conference paper
  • First Online:
Recent Trends in Data Type Specification (ADT 1992, COMPASS 1992)

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

  • 146 Accesses

Abstract

In this paper we informally present a certification calculus for the object specification language TROLL light. The language supports the state- and behavior-oriented specification of information systems. It allows orthogonal construction of large systems from subsystems. The certification calculus provides a basis for verifying properties of specified objects. Besides an introduction to this calculus we show how formulae of this calculus can be derived from TROLL light specifications. The transformation from specification language into calculus shall later be done automatically. Furthermore, we demonstrate proving of object properties by means of an example.

Work reported here has been partially supported by the German Ministry for Research and Technology (BMFT) under Grant No. 01 IS 203 D (project “KorSo”, i.e., correct software) and by CEC under Grant No. BRA 6112 (COMPASS II).

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

Access this chapter

Log in via an institution

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

Similar content being viewed by others

References

  1. C. Arapis. Temporal Specifications of Object Behavior. In B. Thalheim, J. Demetrovics, and H.-D. Gerhardt, editors, Proceedings 3rd. Symp. on Mathematical Fundamentals of Database and Knowledge Base Systems MFDBS'91, pages 308–324. Springer, LNCS 495, 1991.

    Google Scholar 

  2. G. v. Bochmann, M. Barbeau, M. Erradi, L. Lecomte, P. Mondain-Monval, and N. Williams. Mondel: An Object-Oriented Specification Language. Département d'Informatique et de Recherche Opérationnelle, Publication 748, Université de Montréal, 1990.

    Google Scholar 

  3. M. Broy, C. Facchi, R. Grosu, R. Hettler, H. Hussmann, D. Nazareth, F. Regensburger, and K. Stølen. The Requirement and Design Specification Language SPECTRUM — An Informal Introduction (Version 0.3). Technical Report TUM-I9140, Technische Universität München, 1992.

    Google Scholar 

  4. S.Conrad, M. Gogolla, and R. Herzig. TROLL light: A Core Language for Specifying Objects. Informatik-Bericht 92-02, Technische Universität Braunschweig, 1992.

    Google Scholar 

  5. S. Conrad. Ein Basiskalkül für die Verifikation von Eigenschaften synchron interagierender Objekte (A Basic Calculus for Verifying Properties of Synchronously Interacting Objects; in German). Submitted as PhD thesis, Technische Universität Braunschweig, 1993.

    Google Scholar 

  6. G. Denker and M. Gogolla. Translating TROLL light Concepts to Maude. In F. Orejas, editor, Proc. 9th Workshop on Abstract Data Types — 4th Compass Workshop (WADT/Compass'92). Springer LNCS, 1994. (this volume).

    Google Scholar 

  7. H.-D. Ehrich, M. Gogolla, and A. Sernadas. Objects and their Specification. In M. Bidoit and C. Choppy, editors, Proc. 8th Workshop on Abstract Data Types (ADT'91), pages 40–65. Springer, Berlin, LNCS 655, 1992.

    Google Scholar 

  8. H. Ehrig and B. Mahr. Fundamentals of Algebraic Specification 1: Equations and Initial Semantics. Springer, Berlin, 1985.

    Google Scholar 

  9. H. Ehrig and B. Mahr. Fundamentals of Algebraic Specification 2: Modules and Constraints. Springer, Berlin, 1990.

    Google Scholar 

  10. H.-D. Ehrich and A. Sernadas. Fundamental Object Concepts and Constructions. In Saake and Sernadas [SS91], pages 1–24.

    Google Scholar 

  11. H.-D. Ehrich, A. Sernadas, and C. Sernadas. From Data Types to Object Types. Journal on Information Processing and Cybernetics EIK, 26(1–2):33–48, 1990.

    Google Scholar 

  12. J. Fiadeiro. Cálculo de Objectos e Eventos. PhD thesis, Instituto Superior Técnico, Technical University of Lisbon, 1988.

    Google Scholar 

  13. J. Fiadeiro and T. Maibaum. Temporal Reasoning over Deontic Specifications. Journal of Logic and Computation, 1(3):357–395, 1991.

    Google Scholar 

  14. J. Fiadeiro and T. Maibaum. Towards Object Calculi. In Saake and Sernadas [SS91], pages 129–178.

    Google Scholar 

  15. J. Fiadeiro and T. Maibaum. Temporal Theories as Modularisation Units for Concurrent System Specification. Journal Formal Aspects of Computing, 4(3):239–272, 1992.

    Google Scholar 

  16. J. Fiadeiro and A. Sernadas. Logics of Modal Terms for System Specification. Journal of Logic and Computation, 1(2):187–227, 1990.

    Google Scholar 

  17. M. Gogolla, S. Conrad, and R. Herzig. Sketching Concepts and Computational Model of TROLL light. In A. Miola, editor, Proc. 3rd Int. Conf. Design and Implementation of Symbolic Computation Systems (DISCO'93), pages 17–32. Springer, Berlin, LNCS 722, 1993.

    Google Scholar 

  18. M. Große-Rohde. Towards Object-Oriented Algebraic Specifications. In H. Ehrig, K.P. Jantke, F. Orejas, and H. Reichel, editors, Recent Trends in Data Type Specification, pages 98–116. Springer, LNCS 534, 1990.

    Google Scholar 

  19. R. Herzig, S. Conrad, and M. Gogolla. Compositional Description of Object Communities with TROLL light. In C. Chrisment, editor, Proc. Basque Int. Workshop on Information Technology (BIWIT'94). Cepadues Society Press, France, 1994.

    Google Scholar 

  20. R. Jungclaus, G. Saake, and T. Hartmann. Language Features for Object-Oriented Conceptual Modeling. In T.J. Teorey, editor, Proc. 10th Int. Conf. on Entity-Relationship Approach, pages 309–324. E/R Institute, 1991.

    Google Scholar 

  21. R. Jungclaus, G. Saake, T. Hartmann, and C. Sernadas. Object-Oriented Specification of Information Systems: The TROLL Language. Informatik-Bericht 91-04, Technische Universität Braunschweig, 1991.

    Google Scholar 

  22. S. Khosla and T. Maibaum. The Prescription and Description of State Based Systems. In B. Banieqbal, H. Barringer, and A. Pnueli, editors, Temporal Logic in Specification, pages 243–294. Springer, LNCS 398, 1989.

    Google Scholar 

  23. T. Käufl and N. Zabel. Cooperation of Decision Procedures in a Tableau-Based Theorem Prover. Revue d'Intelligence Artificielle, 4(3):99–125, 1990.

    Google Scholar 

  24. R.A. Meersman, W. Kent, and S. Khosla, editors. Object-Oriented Databases: Analysis, Design & Construction (DS-4), Proc. IFIP WG 2.6 Working Conference, Windermere (UK) 1990. North-Holland, 1991.

    Google Scholar 

  25. L.C. Paulson. Isabelle: The Next 700 Theorem Provers. In P. Odifreddi, editor, Logic and Computer Science, pages 361–385. Academic Press, 1990.

    Google Scholar 

  26. G. Reggio. Entities: An Institution for Dynamic Systems. In H. Ehrig, K.P. Jantke, F. Orejas, and H. Reichel, editors, Recent Trends in Data Type Specification, pages 246–265. Springer, LNCS 534, 1990.

    Google Scholar 

  27. A. Sernadas and H.-D. Ehrich. What is an Object, after all? In Meersman et al. [MKK91], pages 39–70.

    Google Scholar 

  28. G. Saake and A. Sernadas, editors. Information Systems — Correctness and Reusability, Workshop IS-CORE '91, ESPRIT BRA WG 3023, London. Informatik-Bericht 91-03, Technische Universität Braunschweig, 1991.

    Google Scholar 

  29. A. Sernadas, C. Sernadas, and J.F. Costa. Object Specification Logic. Internal report, INESC, University of Lisbon, 1992.

    Google Scholar 

  30. R. Wieringa. Equational Specification of Dynamic Objects. In Meersman et al. [MKK91], pages 415–438.

    Google Scholar 

  31. M. Wirsing. Algebraic Specification. In J. Van Leeuwen, editor, Handbook of Theoretical Computer Science, Vol. B, pages 677–788. Elsevier, North-Holland, 1990.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Informatik, Abt. Datenbanken, Technische Universität Braunschweig, Postfach 3329, D-38023, Braunschweig, Germany

    Stefan Conrad

Authors
  1. Stefan Conrad
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Hartmut Ehrig Fernando Orejas

Rights and permissions

Reprints and permissions

Copyright information

© 1994 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Conrad, S. (1994). On certification of specifications for TROLL light objects. In: Ehrig, H., Orejas, F. (eds) Recent Trends in Data Type Specification. ADT COMPASS 1992 1992. Lecture Notes in Computer Science, vol 785. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-57867-6_9

Download citation

  • DOI: https://doi.org/10.1007/3-540-57867-6_9

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-57867-3

  • Online ISBN: 978-3-540-48361-8

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation