Advertisement

Detecting Temporal Logic Predicates in Distributed Programs Using Computation Slicing

  • Alper Sen
  • Vijay K. Garg
Part of the Lecture Notes in Computer Science book series (LNCS, volume 3144)

Abstract

Detecting whether a finite execution trace (or a computation) of a distributed program satisfies a given predicate, called predicate detection, is a fundamental problem in distributed systems. To solve this problem, we generalize an effective abstraction technique called computation slicing. We present polynomial-time algorithms to compute slices with respect to temporal logic predicates from a “regular” subset of CTL, that contains temporal operators EF, EG, and AG. Furthermore, we show that these slices contain precisely those global states of the original computation that satisfy the predicate. Using temporal predicate slices, we give an efficient (polynomial in the number of processes) predicate detection algorithm for a subset of CTL that we call regular CTL. Regular CTL contains nested temporal predicates for which, to the best of our knowledge, there did not previously exist efficient predicate detection algorithms. Then we show that we can enlarge the subset of CTL and still obtain effective results. Our algorithm has been implemented as part of a tool for analysis of distributed programs. We illustrate the effectiveness of our techniques on several protocols achieving speedups of over three orders of magnitude in one example, compared to partial order state-space search of SPIN. Furthermore, we were able to complete the verification for 250 processes for a partial order trace.

Keywords

Partial Order Temporal Logic Global State Atomic Proposition Execution Trace 
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.

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. 1.
    Clarke, E.M., Emerson, E.A.: Design and Synthesis of Synchronization Skeletons using Branching Time Temporal Logic. In: Kozen, D. (ed.) Logic of Programs 1981. LNCS, vol. 131, Springer, Heidelberg (1982)CrossRefGoogle Scholar
  2. 2.
    Davey, B.A., Priestley, H.A.: Introduction to Lattices and Order. Cambridge University Press, Cambridge (1990)zbMATHGoogle Scholar
  3. 3.
    Fidge, C.: Logical Time in Distributed Computing Systems. IEEE Computer 24(8), 28–33 (1991)Google Scholar
  4. 4.
    Garg, V.K.: Elements of Distributed Computing. John Wiley & Sons, Chichester (2002)Google Scholar
  5. 5.
    Garg, V.K., Mittal, N.: On Slicing a Distributed Computation. In: Proc. of the 15th Int’l. Conference on Distributed Computing Systems, ICDCS (2001)Google Scholar
  6. 6.
    Godefroid, P., Wolper, P.: A partial approach to model checking. In: Proc. of the 6th IEEE Symposium on Logic in Computer Science, pp. 406–415 (1991)Google Scholar
  7. 7.
    Havelund, K., Rosu, G.: Monitoring Java Programs with Java Path Explorer. In: Runtime Verification 2001. ENTCS, vol. 55 (2001)Google Scholar
  8. 8.
    Holzmann, G.J.: The Model Checker SPIN. IEEE Transactions on Software Engineering 23(5) (May 1997)Google Scholar
  9. 9.
    Hurfin, M., Mizuno, M., Raynal, M., Singhal, M.: Efficient detection of conjunctions of local predicates. IEEE Transactions on Software Engineering 24(8), 664–677 (1998)CrossRefGoogle Scholar
  10. 10.
    ISO. Specification of the Asynchronous Transfer Mode Ring Protocol (ATMR) (1993) Google Scholar
  11. 11.
    Kim, M., Kannan, S., Lee, I., Sokolsky, O., Viswanathan, M.: Java-MaC: A Run-time Assurance Tool for Java Programs. In: Runtime Verification 2001. ENTCS, vol. 55 (2001)Google Scholar
  12. 12.
    Lamport, L.: Time, Clocks, and the Ordering of Events in a Distributed System. Communications of the ACM 21(7), 558–565 (1978)zbMATHCrossRefGoogle Scholar
  13. 13.
    Mattern, F.: Virtual Time and Global States of Distributed Systems. In: Proc. of the Int’l Workshop on Parallel and Distributed Algorithms (1989)Google Scholar
  14. 14.
    McMillan, K.L.: Symbolic Model Checking. Kluwer Academic Publishers, Dordrecht (1993)zbMATHGoogle Scholar
  15. 15.
    Mittal, N., Garg, V.K.: Computation Slicing: Techniques and Theory. In: Proc. of the 15th Int’l. Symposium on Distributed Computing, DISC (2001)Google Scholar
  16. 16.
    Mittal, N., Garg, V.K.: On Detecting Global Predicates in Distributed Computations. In: Proc. of the 15th Int’l. Conference on Distributed Computing Systems, ICDCS (2001)Google Scholar
  17. 17.
    Peng, H., Tahar, S., Khendek, F.: Comparison of SPIN and VIS for Protocol Verification. Software Tools for Technology Transfer 4(2), 234–245 (2003)CrossRefGoogle Scholar
  18. 18.
    Sen, A., Garg, V.K.: Detecting Temporal Logic Predicates on the Happened-Before Model. In: Proc. of the Int’l Parallel and Distributed Processing Symposium, IPDPS (2002)Google Scholar
  19. 19.
    Sen, A., Garg, V.K.: Automatic Generation of Slices for Temporal Logic Predicate Detection. Technical Report TR-PDS-2003-001, PDSL, ECE Dept. Univ. of Texas at Austin (2003), Available at http://maple.ece.utexas.edu/
  20. 20.
    Sen, A., Garg, V.K.: Partial Order Trace Analyzer, POTA (2003), http://maple.ece.utexas.edu/~sen/POTA.html
  21. 21.
    Sen, A., Garg, V.K.: Partial Order Trace Analyzer (POTA) for Distributed Programs. In: Runtime Verification 2003. ENTCS, vol. 89 (2003)Google Scholar
  22. 22.
    Sen, K., Rosu, G., Agha, G.: Runtime Safety Analysis of Multithreaded Programs. In: Proc. of the 11th ACM Symposium on the Foundations of Software Engineering (2003)Google Scholar
  23. 23.
    Valmari, A.: A Stubborn Attack On State Explosion. In: Clarke, E., Kurshan, R.P. (eds.) CAV 1990. LNCS, vol. 531, pp. 156–165. Springer, Heidelberg (1991)CrossRefGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2004

Authors and Affiliations

  • Alper Sen
    • 1
  • Vijay K. Garg
    • 1
  1. 1.Dept. of Electrical and Computer EngineeringThe University of Texas at AustinAustinUSA

Personalised recommendations