Skip to main content
SpringerLink
Log in

Specification of an integrated circuit card protocol application using the B method and linear temporal logic

  • Conference paper
  • First Online:
Book cover B’98: Recent Advances in the Development and Use of the B Method (B 1998)

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

Included in the following conference series:

Abstract

In this paper we propose a construction method of multiformalism specifications based on B and linear temporal logic. We examined this method with a case study of a communication protocol between an integrated circuit card and a device such a terminal. This study has been carried out in collaboration with the Schlumberger company. We show the current advantages and limits in combining many specifications formalisms and the associated toolkits: Atelier B and SPIN. Finally, we draw conclusions about future directions of research on the proof of heterogeneous specifications, incremental verification and ontool cooperation to assist in the verification step (e.g. a prover, a model-checker and an animator).

Specification is available on http://lib.univ-fcomte.fr/RECHERCHE/P5/ICC.html

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. J. R. Abrial-The B Book-Cambridge University Press, 1996-ISBN 0521-496195.

    Google Scholar 

  2. J-R. Abrial-Extending B without Changing it (for Developping Distributed Systems) — 1st Conference on the B method-November 1996. Nantes.

    Google Scholar 

  3. J-R. Abrial, Mussat L-Specification and Design of a transmission protocol by successive refinements using B — to appear in LNCS. 1997.

    Google Scholar 

  4. J. R. Abrial-Constructions d'Automatismes Industriels avec B — Congrés AFADL — ONERA-CERT Toulouse-Mai 1997.

    Google Scholar 

  5. G. Bernot, S. Coudret, P. Le Gall-Heterogeneous formal specifications-Proc. of the 5th Int. Conf. on Algebraic Methodology and Software Technology-AMAST'96-pp 548–472-LNCS 1101.

    Google Scholar 

  6. M. Butler, M. Walden-Distributed System Development in B-1st Conference on the B method-November 1996-Nantes.

    Google Scholar 

  7. C. Courcoubetis, M. Vardi, P. Wolper, M. Yannakakis-Memory efficient algorithms for the vérification of temporal properties-Formal Methods in System Design I-pp 275–288.

    Google Scholar 

  8. European Standard-Identification Cards-Integrated circuit(s) cards with contacts-Electronic Signal and transmission protocols-ISO/CEI 7816-3-1992.

    Google Scholar 

  9. Formal Methods for Industrial Applications: Specifying and Programming the Steam Boiler Control-ISBN 3-540-61929-1-Springer Verlag-1996.

    Google Scholar 

  10. R. Gerth, D. Peled, M. Vardi, P. Wolper-Simple on-the-fly automatic verification of linear temporal logic-Proc. PSTV95 Conference-Warsaw-Poland-1995.

    Google Scholar 

  11. P. Godefroid and G. Holzmann-On the verification of temporal properties-Proc. IFIP/WG6.1 Symp. On Protocols Specification, Testing and Verification-PSTV93-Liege-Belgium-June 1993.

    Google Scholar 

  12. G. Holzmann-Design and validation of protocols-Prentice hall software series-1991.

    Google Scholar 

  13. G. Holzmann, D. Peled and Y. Yannakakis-On the nested depth-first search. Proc. 2nd Spin Workshop-American Mathematical Society-DIMACS/32-1996.

    Google Scholar 

  14. G. Holzmann-State compression in SPIN. Proc. 3rd Spin Workshop-Twente University-April 1997.

    Google Scholar 

  15. G. Holzmann-The model checker SPIN. IEEE Trans. On Software Engineering-Vol. 23, No 5.

    Google Scholar 

  16. K. Lano-Formal Object-Oriented Development-Springer-Verlag-1995.

    Google Scholar 

  17. K. Lano, J. Bicarregui, A. Sanchez-Using B to Design and Verify Controllers for Chemical Processing-1st Conference on the B method-November 1996-Nantes.

    Google Scholar 

  18. Z. Manna, A. Pnueli-The Temporal Logic of Reactive and Cocurrent Systems: Specification. ISBN 0-387-97664-7-Springer-Verlag-1992.

    Google Scholar 

  19. Z. Manna, A. Pnueli-Temporal Verification of Reactive Systems: Safety. ISBN 0-387-94459-1-Springer-Verlag-1995.

    Google Scholar 

  20. Manuel de référence du langage B-Steria Méditerranée-Décembre 1996.

    Google Scholar 

  21. D. A. Peled-Combining partial order reduction with on-the-fly model checking-Proc. 6th Int. Conf. On Computer Aided Verification-CAV94-Stanford-1994.

    Google Scholar 

  22. D. Mery-Machines abstraites temporelles-Analyse comparative de B et de TLA+-1st Conference on the B method-November 1996-Nantes.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Laboratoire d'Informatique, 16 route de Gray, 25030, BesanÇon cedex, France

    Jacques Julliand, Bruno Legeard, Benoit Parreaux & Bruno TatibouËt

  2. Schlumberger Industries, Terminaux Urbains et Systemes, Parc Lafayette, 6 Rue Isaac Newton, 25000, BesanÇon, France

    Thierry Machicoane

Authors
  1. Jacques Julliand
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Bruno Legeard
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Thierry Machicoane
    View author publications

    You can also search for this author in PubMed Google Scholar

  4. Benoit Parreaux
    View author publications

    You can also search for this author in PubMed Google Scholar

  5. Bruno TatibouËt
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Didier Bert

Rights and permissions

Reprints and permissions

Copyright information

© 1998 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Julliand, J., Legeard, B., Machicoane, T., Parreaux, B., TatibouËt, B. (1998). Specification of an integrated circuit card protocol application using the B method and linear temporal logic. In: Bert, D. (eds) B’98: Recent Advances in the Development and Use of the B Method. B 1998. Lecture Notes in Computer Science, vol 1393. Springer, Berlin, Heidelberg. https://doi.org/10.1007/BFb0053367

Download citation

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

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-64405-7

  • Online ISBN: 978-3-540-69769-5

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation