Skip to main content
SpringerLink
Log in

A Global Semantics for Views

  • Conference paper
  • First Online:
Algebraic Methodology and Software Technology (AMAST 2000)

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

Abstract

We focus on the specification of mixed systems that contain static and dynamic aspects. Our approach aims at keeping advantage of the languages dedicated to both aspects (algebraic specifications for data types, and state transition diagrams for dynamic behaviour) while providing an underlying unifying framework accompanied by an appropriate semantic model. This underlying framework is based on our notion of views. In [4] we addressed the composition of any number of views in a composition. Here we address the strong links that exist between all aspects of a single component, and that altogether build its global semantics. After presenting the (state and transition) formulas and their semantics, we show how to glue the different aspects together, and we present the retrieval of the global view for components. We provide here a new set of rules for the STS part of our views, taking into account the composition of all aspects. We then give the formal (global) semantics for such global views. We illustrate our view model on a password management example.

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

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 84.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 109.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. André Arnold. Systèmes de transitions finis et sémantique des processus communicants. Etudes et recherches en informatique. Masson, 1992.

    Google Scholar 

  2. Tommaso Bolognesi and Ed Brinksma. Introduction to the ISO Specification Language LOTOS. Computer Networks and ISDN Systems, 14(1):25–29, January 1988.

    Article  Google Scholar 

  3. Christine Choppy, Pascal Poizat, and Jean-Claude Royer. A Global Semantics for Views. Research Report 189, IRIN, 1999. /papers/rr189.ps.gz in Poizat’s web page.

    Google Scholar 

  4. Christine Choppy, Pascal Poizat, and Jean-Claude Royer. Control and Datatypes using the View Formalism. Research Report 188, IRIN, 1999. /papers/rr188.ps.gz in Poizat’s web page.

    Google Scholar 

  5. Jan Ellsberger, Dieter Hogrefe, and Amardeo Sarma. SDL: Formal Object-oriented Language for Communicating Systems. Prentice-Hall, 1997.

    Google Scholar 

  6. M. Hennessy and H. Lin. Symbolic Bisimulations. Theoretical Computer Science, 138(2):353–389, 1995.

    Article  MATH  MathSciNet  Google Scholar 

  7. ISO/IEC. LOTOS: A Formal Description Technique based on the Temporal Ordering of Observational Behaviour. ISO/IEC 8807, International Organization for Standardization, 1989.

    Google Scholar 

  8. Leslie Lamport. The Temporal Logic of Actions. ACM Transactions on Programming Languages and Systems, 16(3):872–923, 1994.

    Article  Google Scholar 

  9. Radu Mateescu. Vérification des propriétés temporelles des programmes parallèles. PhD thesis, Institut National Polytechnique de Grenoble, 1998.

    Google Scholar 

  10. José Meseguer. Rewriting logic as a semantic framework for concurrency: a progress report. In CONCUR’96: Concurrency Theory, volume 1119 of Lecture Notes in Computer Science, pages 331–372, Pisa, Italy, 1996.

    Google Scholar 

  11. Gaël Nedelec, Marielle Papillon, Christelle Piedsnoirs, and Gwen Salaün. CLAP: a Class Library for Automata in Python. Master’s thesis, 1999. CLAP.html in Poizat’s web page.

    Google Scholar 

  12. Pascal Poizat, Christine Choppy, and Jean-Claude Royer. Concurrency and Data Types: A Specification Method. An Example with LOTOS. In J. Fiadeiro, editor, Recent Trends in Algebraic Development Techniques, Selected Papers of the 13th International Workshop on Algebraic Development Techniques WADT’98, volume 1589 of Lecture Notes in Computer Science, pages 276–291, Lisbon, Portugal, 1999. Springer-Verlag.

    Google Scholar 

  13. Pascal Poizat, Christine Choppy, and Jean-Claude Royer. From Informal Requirements to COOP: a Concurrent Automata Approach. In J.M. Wing, J. Woodcock, and J. Davies, editors, FM’99-Formal Methods, World Congress on Formal Methods in the Development of Computing Systems, volume 1709 of Lecture Notes in Computer Science, pages 939–962, Toulouse, France, 1999. Springer-Verlag.

    Google Scholar 

  14. Gianna Reggio and Mauro Larosa. A graphic notation for formal specifications of dynamic systems. In John Fitzgerald, Cliff B. Jones, and Peter Lucas, editors, FME’97: Industrial Applications and Strengthened Foundations of Formal Methods (Proc. 4th Intl. Symposium of Formal Methods Europe, Graz, Austria, September 1997), volume 1313 of Lecture Notes in Computer Science, pages 40–61. Springer-Verlag, September 1997. ISBN 3-540-63533-5.

    Google Scholar 

  15. Carron Shankland, Muffy Thomas, and Ed Brinksma. Symbolic Bisimulation for Full LOTOS. In Algebraic Methodology and Software Technology AMAST’97, volume 1349 of Lecture Notes in Computer Science, pages 479–493. Springer-Verlag.

    Chapter  Google Scholar 

  16. Graeme Smith. A Semantic Integration of Object-Z and CSP for the Specification of Concurrent Systems. In J. Fitzgerald, C.B. Jones, and P. Lucas, editors, Formal Methods Europe (FME’97), volume 1313 of Lecture Notes in Computer Science, pages 62–81. Springer-Verlag, 1997.

    Google Scholar 

  17. Rational Software. Unified Modeling Language, Version 1.1. Technical report, Rational Software Corp, http://www.rational.com/uml, September 1997.

  18. Martin Wirsing. Algebraic Specification, volume B of Handbook of Theoretical Computer Science, chapter 13, pages 675–788. Elsevier, 1990. Jan Van Leeuwen, Editor.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. LIPN, Institut Galilée, Université Paris XIII, Avenue Jean-Baptiste Clément, F-93430, Villetaneuse, France

    Christine Choppy

  2. IRIN, Université de Nantes, 2 rue de la Houssinière, B.P. 92208, F-44322, Nantes cedex 3, France

    Pascal Poizat & Jean-Claude Royer

Authors
  1. Christine Choppy
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Pascal Poizat
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Jean-Claude Royer
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Department of Computer Science, The University of Iowa, Iowa City, IA, 52242, USA

    Teodor Rus

Rights and permissions

Reprints and permissions

Copyright information

© 2000 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Choppy, C., Poizat, P., Royer, JC. (2000). A Global Semantics for Views. In: Rus, T. (eds) Algebraic Methodology and Software Technology. AMAST 2000. Lecture Notes in Computer Science, vol 1816. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-45499-3_13

Download citation

  • DOI: https://doi.org/10.1007/3-540-45499-3_13

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

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

  • Online ISBN: 978-3-540-45499-1

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation