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

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