Advertisement

An Automata-Based Approach to Property Testing in Event Traces

  • Hesham Hallal
  • Sergiy Boroday
  • Andreas Ulrich
  • Alexandre Petrenko
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 2644)

Abstract

We present a framework for property testing where a partially ordered execution trace of a distributed system is modeled by a collection of communicating automata. We prove that the model exactly characterizes the causality relation between the events in the observed trace. We present the implementation of this approach in SDL, where ObjectGEODE is used to verify properties, and illustrate the approach with an industrial case study.

Keywords

monitoring passive testing distributed traces property checking SDL 

References

  1. 1.
    B. Algayres, Y. Lejeune, E. Hugonnet, “GOAL: Observing SDL behaviors with GEODE”, in SDL’95 with MSC in CASE (ed. R. Braek, A. Sarma), Proc. of the 7 th SDL Forum, Oslo, Norway, Sept. 1995, Elsevier Science Publishers B. V. (North Holland), pp. 359–372.Google Scholar
  2. 2.
    R. Alur and M. Yannakakis. “Model Checking of Message Sequence Charts”. In CONCUR’99: Concurrency Theory, Tenth International Conference, LNCS 1664, pages 114–129, 1999.CrossRefGoogle Scholar
  3. 3.
    J. P. Black, M. H. Coffin, D. J. Taylor, T. Kunz, A. A. Basten, “Linking Specifications, Abstraction, and Debugging,” CCNG Technical Report E-232, Computer Communications and Network Group, University of Waterloo, Nov. 1993.Google Scholar
  4. 4.
    R. Bonnet and M. Pouzet. “Linear Extensions of Ordered Sets”. In I. Rival, editor, Ordered Sets, pages 125–170, D. Reidel Publishing Company, 1982.Google Scholar
  5. 5.
    K. Chandy, L. Lamport, “Distributed Snapshots: Determining Global States of Distributed Systems”, ACM Transactions on Computing Systems 3(1), pp. 63–75, Feb. 1985.CrossRefGoogle Scholar
  6. 6.
    B. Charron-Bost, F. Mattern, and G. Tel. “Synchronous, Asynchronous, and Causally Ordered Communications”. Distributed Computing, 1995.Google Scholar
  7. 7.
    F. Dietrich, X. Logean, S. Koppenhoefer, J.-P. Hubaux, “Testing Temporal Logic Properties in Distributed Systems” In Proc. of the 11 th International Workshop on Testing of Communicating Systems, Tomsk, Russia, Aug. 1998.Google Scholar
  8. 8.
    M. Dwyer, G. Avrunin, and J. Corbett, “Patterns in Property Specifications for Finite-state Verification”, In Proc. 21 st International Conference on Software Engineering, May 1999.Google Scholar
  9. 9.
    M. Dwyer, L. Clarke, “Data Flow Analysis for Verifying Properties of Concurrent Programs”, In Proc. of ACM SIGSOFT’94, New Orleans, LA, USA, 1994.Google Scholar
  10. 10.
    A. Engels, S. Mauw, and M.A. Reniers. “A Hierarchy of Communication Models for Message Sequence Charts”. In T. Mizuno, N. Shiratori, T. Higashino, and A. Togashi, editors, FORTE/PSTV’ 97, pages 75–90, Osaka, Japan Nov. 1997. Chapman & Hall. To appear in Science of Computer Programming, 2002.Google Scholar
  11. 11.
    Q. Fan. “Formalizing Properties for Distributed System Testing”, Master Thesis in Preparation.Google Scholar
  12. 12.
    E. Fromentin, M. Raynal, V. Garg, and A. Tomlinson, “On the Fly Testing of Regular Patterns in Distributed Computations”, Internal Publication # 817, IRISA, Rennes, France, 1994.Google Scholar
  13. 13.
    R. Groz, “Unrestricted Verification of Protocol Properties on a Simulation Using an Observer Approach”, Protocol Specification, Testing and Verification, VI, Montréal, Canada, North-Holland, 1986, pp. 255–266.Google Scholar
  14. 14.
    H. Hallal, A. Petrenko, A. Ulrich, S. Boroday, “Using SDL Tools to Test Properties of Distributed Systems”, In proc. of Workshop on Formal Approaches to Testing of Software (FATES) in affiliation with CONCUR’01; Aalborg, Denmark; BRICS Technical Report NS-01-4, Aug. 2001.Google Scholar
  15. 15.
    G.J. Holzmann. “The Model Checker SPIN”. IEEE Transactions on Software Engineering, 23(5):279–295, 1997.CrossRefMathSciNetGoogle Scholar
  16. 16.
    B. E. Jackl, “Event-Predicate Detection in the Debugging of Distributed Applications”, Master’s Thesis. Department of Computer Science, University of Waterloo, 1996.Google Scholar
  17. 17.
    C. Jard, T. Jeron, G. V. Jourdan, and J. X. Rampon, “A General Approach to Trace-checking in Distributed Computing Systems”, In Proc. IEEE Int. Conf. on Distributed Computing Systems, Poznan, Poland, Jun. 1994.Google Scholar
  18. 18.
    KLOCwork. Corporate website, http://www.KLOCwork.com/.
  19. 19.
    P. B. Ladkin and Stefan Leue. “Interpreting Message Flow Graphs”. Formal Aspects of Computing 7(5), p. 473–509, Sept./Oct. 1995.zbMATHCrossRefGoogle Scholar
  20. 20.
    Leue and P.B. Ladkin. “Implementing and Verifying MSC Specifications Using Promela/Xspin”. In J.-C. Grégoire, G. Holzmann and D. Peled (eds.), Procs of the DIMACS Workshop SPIN96, the 2nd Intl Workshop on the SPIN Verification System. DIMACS Series Volume 32, American Mathematical Society, Providence, R.I., 1997Google Scholar
  21. 21.
    D. Luckham and B. Frasca, “Complex Event Processing in Distributed Systems”, Stanford University Technical Report CSL-TR-98-754, Mar. 1998, 28 pages.Google Scholar
  22. 22.
    N. Mansurov, D. Zhukov “Automatic Synthesis of SDL models in Use Case Methodology”. In R. Dssouli, G. v. Bochmann, and Y. Lahav (eds.), SDL’99: The Next Millenium, Proc. of the ninth SDL Forum, Montreal, Québec, Canada, Jun. 21–25, 1999.Google Scholar
  23. 23.
    B. Miller, J. Choi, “Breakpoints and Halting in Distributed Programs”, In Proc. of the 8 th IEEE Int. Conf. on Distributed Computing Systems, San Jose, Jul. 1988.Google Scholar
  24. 24.
    Pattern Specification System http://www.cis.ksu.edu/santos/spec-patterns.
  25. 25.
    G. Robert, F. Khendek and P. Grogono “Deriving an SDL Specification with a Given Architecture from a Set of MSCs”, In A. Cavalli and A. Sarma (eds.), SDL’97: Time for Testing — SDL, MSC and Trends, Proc. of the eight SDL Forum, Evry, France, Sept. 22–26, 1997.Google Scholar
  26. 26.
    R. L. Smith, G. S. Avrunin, L. Clarke, and L.J. Osterweil. “An Approach Supporting Property Elucidation”. In Proc. of the 24th International Conference on Software Engineering, Orlando, FL, May 2002, pages 11–21.Google Scholar
  27. 27.
  28. 28.
    A. Tanenbaum. “Computer Networks”. Prentice Hall, 1996.Google Scholar
  29. 29.
    Telelogic, “ObjectGEODE SDL Simulator Reference Manual”.Google Scholar
  30. 30.
    A. Ulrich, H. Hallal, A. Petrenko, S. Boroday, “Verifying Trustworthiness Requirements in Distributed Systems with Formal Log-file Analysis”. In Proc. of the thirty-sixth Hawaii International Conference on System Sciences (HICSS-36), 2003.Google Scholar
  31. 31.
    P. A. S. Ward, “A Framework Algorithm for Dynamic Centralized Dimension-Bounded Timestamps”, In Proc. of CASCON 2000, Mississauga, Ontario, Canada.Google Scholar

Copyright information

© IFIP 2003

Authors and Affiliations

  • Hesham Hallal
    • 1
  • Sergiy Boroday
    • 1
  • Andreas Ulrich
    • 2
  • Alexandre Petrenko
    • 1
  1. 1.CRIMMontrealCanada
  2. 2.Corporate Technology SE1Siemens AGMünchenGermany

Personalised recommendations