Advertisement

A partial-order approach to the verification of concurrent systems: Checking liveness properties

  • Dominique Bolignano
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 987)

Abstract

We present the foundations of an approach for exploiting the partial ordering of events in the verification of concurrent systems. The main objective of the approach is to avoid the state explosion that is due to the use of the standard interleaving semantics of concurrency. The approach has been applied successfully to the verification of complex hardware and software systems such as a shared memory with multicache for a multi-processor architecture. The technique is described for finite state systems and applied to the checking of liveness properties using a model-checking approach. Most existing approaches use the partial ordering of events as a means of reducing the number of traces to check: checking is in particular done on normal totally ordered traces and the reduction (i.e. the selection of representatives) is dependent on the property at hand. We strongly differ from these approaches by directly performing the checking on the partial order graphs themselves, not on particular linearizations. These partial order graphs are not dependent on the property to check: only the checking is. For this we introduce models based on tuples to represent partial orders, and a special kind of automaton that we call partial order automaton which generates the set of all possible partial ordering that can result from the execution of a system.

Keywords

Partial Order Model Check Transitive Closure Parallel Composition 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.
    Schneider F.B. Alpern B. Recognizing safety and liveness. Distributed Computing, 1987.Google Scholar
  2. 2.
    D. Bolignano. An approach to the verification of concurrent systems. Technical report, Bull Research, December 1994.Google Scholar
  3. 3.
    A. Bouajjani, J.C. Fernandez, S. Graf, C. Rodriguez, and J. Sifakis. Safety for branching semantics. In Springer Verlag, editor, LNCS, 12th Colloquium on Automata, Languages, and Programming, 1991.Google Scholar
  4. 4.
    S. Eilenberg. Automata, Languages, and Machines (Vol. A). Academic Press, 1974.Google Scholar
  5. 5.
    P. Godefroid. Using partial orders to improve automatic verification methods. In Proc. 1990 Computer-Aided Verification Workshop, June 1990.Google Scholar
  6. 6.
    P. Godefroid and P. Wolper. A partial approach to model checking. In Proc. 6th IEEE Symp on Logic in Computer Science, July 1991.Google Scholar
  7. 7.
    Katz and Peled. Verification of distributed programs using representative interleaving sequences. Distributed Computing, 6, 1992.Google Scholar
  8. 8.
    A. Mazurkiewicz. Trace theory. In Petri Nets: Applications and Relationship to Other Models of Concurrency, Advances in Petri Nets 1986, PART II, Advanced Course, pages 279–324, Bad Honnefs, September 1986. Berlin, West Germany: Springer-Verlag. LNCS-255.Google Scholar
  9. 9.
    K.I. McMillan. Using unfoldings to avoid state explosion problem in the verification of asynchronous circuits. In Proceedings of the 4th International Conference, CAV'92, 1992.Google Scholar
  10. 10.
    D. Peled. All from one, one for all: On model checking using representatives. In Proceedings of the 5th International Conference, CAV'93, 1993.Google Scholar
  11. 11.
    A. Valmari. Stubborn sets forreduced state space generation, 10th international conference on application and theory of petri nets. In Vol 2, 1989.Google Scholar
  12. 12.
    A. Valmari. On-the-fly verification with stubborn sets. In Proceedings of the 5th International Conference, CAV'93, 1993.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1995

Authors and Affiliations

  • Dominique Bolignano
    • 1
  1. 1.BullLes Clayes-sous-BoisFrance

Personalised recommendations