Advertisement

Verifying hardware components with JACK

  • R. De Nicola
  • A. Fantechi
  • S. Gnesi
  • S. Larosa
  • G. Ristori
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 987)

Abstract

JACK (the acronym for Just Another Concurrency Kit) is a workbench integrating a set of verification tools for concurrent system specifications, supported by a graphical interface offering facilities to use these tools separately or in combination. The environment offers several functionalities to support the design, analysis and verification of systems specified using process algebras. In this paper we use JACK to formally specify the hardware components of a buffer system. Then we verify, by using the checking capabilities of JACK, the correctness of the specification with respect to some safety requirements, expressed in the action based temporal logic ACTL.

Keywords

Model Check Temporal Logic Label Transition System Process Algebra Concurrent System 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.

References

  1. 1.
    A. Bouali and R. de Simone. Symbolic bisimulation minimisation. In Fourth Workshop on Computer-Aided Verification, Montreal, 1992, LNCS 663, Springer-Verlag.Google Scholar
  2. 2.
    A. Bouali, S. Gnesi, S. Larosa. The integration Project for the JACK Environment. Bulletin of the EATCS, n.54, October 1994, pp. 207–223.Google Scholar
  3. 3.
    E.M. Clarke, E.A. Emerson, A.P. Sistla: Automatic Verification of Finite State Concurrent Systems using Temporal Logic Specifications, ACM Toplas, 8 (2), 1986, pp. 244–263.Google Scholar
  4. 4.
    R. Cleaveland, J. Parrow, and B. Steffen. The concurrency workbench. In Automatic Verification Methods for Finite State Systems, LNCS 407, Springer-Verlag, 1989, pp. 24–37.Google Scholar
  5. 5.
    M. Danelutto, G. DiCaprio, and A. Masini. Parallelizing a Model Checker. submitted for publication, 1995.Google Scholar
  6. 6.
    N. De Francesco, A. Fantechi, S. Gnesi, P. Inverardi. Model Checking of non-finite state processes by Finite Approximations. TACAS Workshop, LNCS, Springer-Verlag. May 1994.Google Scholar
  7. 7.
    R. De Nicola, A. Fantechi, S. Gnesi, G. Ristori. An action-based framework for verifying logical and behavioural properties of concurrent systems. Computer Network and ISDN systems, Vol. 25, No.7, North Holland, 1993, pp. 761–778.Google Scholar
  8. 8.
    R. De Nicola, P. Inverardi, and M. Nesi. Equational reasoning about LOTOS specifications: A rewriting approach. In Sixth International Workshop on Software Specification and Design, 1991, pp. 54–67.Google Scholar
  9. 9.
    R. De Nicola and F.W. Vaandrager. Action versus state based logics for transition systems. In I. Guessarian, editor, Semantics of Systems of Concurrent Processes, Proceedings LITP Spring School on Theoretical Computer Science, LNCS 469, Springer-Verlag, 1990, pp. 407–419.Google Scholar
  10. 10.
    R. De Nicola and F.W. Vaandrager. Three Logics for Branching Bisimulation. Journal of ACM, Vol. 42, N. 2, 1995, pp. 458–487.Google Scholar
  11. 11.
    E. A. Emerson, J. Y. Halpern. ”Sometimes” and ”Not Never” Revisited: on Branching Time versus Linear Time Temporal Logic. Journal of ACM, 33 (1),1986, pp. 151–178.Google Scholar
  12. 12.
    A. Fantechi, S. Gnesi, G. Ristori, M. Carenini, M. Vanocchi, and P. Moreschini. Assisting requirement formalization by means of natural language translation. Formal Methods in Systems Design, 4(2), Elsevier Science Publisher, 1994, pp. 243–263.Google Scholar
  13. 13.
    G. Ferro. AMC: ACTL Model Checker. Reference Manual. IEI-Internal Report, B4–47 December 1994.Google Scholar
  14. 14.
    M. Hennessy and R. Milner. Algebraic Laws for Nondeterminism and Concurrency. Journal of ACM, 32, 1985, pp. 137–161.Google Scholar
  15. 15.
    C.A.R. Hoare. Communicating Sequential Processes. Prentice Hall, London, 1985.Google Scholar
  16. 16.
    P. Inverardi, C. Priami, and D. Yankelevich. Verifing concurrent systems in SML. In SIGPLAN ML Workshop, San Francisco, June 1992.Google Scholar
  17. 17.
    E. Madelaine and R. De Simone. The fc2 reference manual. Technical report, INRIA, 1993.Google Scholar
  18. 18.
    R. Milner. Communication and Concurrency. Prentice-Hall International, Englewood Cliffs, 1989.Google Scholar
  19. 19.
    V. Roy and R. de Simone. AUTO and autograph. In R. Kurshan, editor, Workshop on Computer Aided Verification, New-Brunswick, June 1990. LNCS 531, Springer-Verlag, pp. 65–75.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1995

Authors and Affiliations

  • R. De Nicola
    • 1
  • A. Fantechi
    • 2
  • S. Gnesi
    • 3
  • S. Larosa
    • 3
  • G. Ristori
    • 4
  1. 1.Dip. di Scienze dell'InformazioneUniv. di Roma“La Sapienza”Italy
  2. 2.Dip. di Ingegneria dell'InformazioneUniv. di PisaItaly
  3. 3.Istituto di Elaborazione dell'InformazioneC.N.R.PisaItaly
  4. 4.Dip. di InformaticaUniv. di PisaItaly

Personalised recommendations