Skip to main content
SpringerLink
Log in

A solution relying on the model checking of boolean transition systems

  • Conference paper
  • First Online:
Formal Systems Specification

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

Abstract

In this paper we present the Temporal Language of Transitions (TLT) solution to the RPC Memory Specification Problem posed by Lamport for a Dagstuhl seminar. TLT is a framework for the compositional specification and verification of distributed systems. In our solution we show how the TLT specifications can be factorized to extract their finite-state control parts. This leads to straightforward refinement checks. We address all parts of the original problem statement.

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.

References

  1. Robert Allen and David Garlan. Formal Connectors. Technical Report CMU-CS-94-115, School of Computer Science, Carnegie Mellon University, Pittsburgh, PA, March 1994.

    Google Scholar 

  2. Andre Arnold. Finite Transition Systems. Prentice Hall, 1994.

    Google Scholar 

  3. Dieter Barnard and Simon Crosby. The Specification and Verification of an ATM Signalling Protocol. In Proc. of 15th IFIP PSTV'95, Warsaw, June 1995.

    Google Scholar 

  4. M. Broy, L. Lamport. The RPC Memory Specification Problem. This Volume.

    Google Scholar 

  5. Manfred Broy. A Functional Solution to the RPC-Memory Specification Problem. Submitted as a Final Solution to Dagstuhl Seminar of Broy/Lamport, 1994, Faculty of Informatics, Technical University of Munich, D-80290 Munich, Germany, 1996.

    Google Scholar 

  6. H. Busch. A Practical Method for Reasoning About Distributed Systems in a Theorem Prover. In Higher Order Logic Theorem Proving and its Applications — 8th International Workshop, Aspen Grove, UT, USA, Proceedings, pages 106–121. Springer-Verlag, LNCS 971, September 1995.

    Google Scholar 

  7. Jorge Cuéllar, Dieter Barnard, and Martin Huber. Dealing with Actions in Assertional Reasoning. Internal report, available by e-mail, ZFE T SE 1, Siemens AG, October 1995.

    Google Scholar 

  8. Jorge Cuéllar, Dieter Barnard, and Martin Huber. Rapid Protyping for an Assertional Specification Language. TACAS'96, LNCS 1055, March 1996.

    Google Scholar 

  9. C. Courcoubetis, S. Graf, and J. Sifakis. An Algebra of Boolean Processes. In Proc. of CAV'91, pages 454–465, 1991.

    Google Scholar 

  10. Jorge Cuéllar and Martin Huber. The FZI Production Cell Case Study: A distributed solution using TLT. In Formal Development of Reactive Systems: Case Study Production Cell, volume 891 of LNCS. Springer-Verlag, 1995.

    Google Scholar 

  11. K. Mani Chandy and J. Misra. Parallel Program Design — A Foundation. Addison-Wesley, Reading, Massachusetts, 1988.

    Google Scholar 

  12. Jorge Cuéllar and Isolde Wildgruber. The Steam Boiler Problem — A TLT Solution (Presented at a Dagstuhl Seminar). In Proc. of a Dagstuhl Seminar, 1996.

    Google Scholar 

  13. J. R. Cuéllar, I. Wildgruber, and D. Barnard. Combining the Design of Industrial Systems with Effective Verification Techniques. In M. Naftalin, T. Denvir, and M. Betran, editors, Proc. of FME'94, volume 873 of LNCS, pages 639–658, Barcelona, Spain, October 1994. Springer-Verlag.

    Google Scholar 

  14. Y. Gurevich. Evolving Algebras: A Tutorial Introduction. In Bulletin of the EATCS, volume 43, pages 264–284. EATCS, 1991.

    Google Scholar 

  15. R.P. Kurshan. Analysis of Discrete Event Systems. LNCS, 430:414–453, 1990.

    Google Scholar 

  16. R.P. Kurshan. Computer Aided Verification of Coordinating Processes. Princeton University Press, 1994.

    Google Scholar 

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

    Article  Google Scholar 

  18. Stephan Merz. From TLT modules to stream processing functions. Internal paper, Faculty of Informatics, Technical University of Munich, D-80290 Munich, March 1996.

    Google Scholar 

  19. R. Milner. Communication and Concurrency. Prentice-Hall, London, 1989.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Siemens R&D, ZT SE 1, D-81730, Munich, Germany

    Jorge Cuéllar, Dieter Barnard & Martin Huber

Authors
  1. Jorge Cuéllar
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Dieter Barnard
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Martin Huber
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Manfred Broy Stephan Merz Katharina Spies

Rights and permissions

Reprints and permissions

Copyright information

© 1996 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Cuéllar, J., Barnard, D., Huber, M. (1996). A solution relying on the model checking of boolean transition systems. In: Broy, M., Merz, S., Spies, K. (eds) Formal Systems Specification. Lecture Notes in Computer Science, vol 1169. Springer, Berlin, Heidelberg. https://doi.org/10.1007/BFb0024431

Download citation

  • DOI: https://doi.org/10.1007/BFb0024431

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-61984-0

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

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation