An Automata-Based Approach to Property Testing in Event Traces
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.
Keywordsmonitoring passive testing distributed traces property checking SDL
- 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
- 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.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
- 6.B. Charron-Bost, F. Mattern, and G. Tel. “Synchronous, Asynchronous, and Causally Ordered Communications”. Distributed Computing, 1995.Google Scholar
- 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.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.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.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.Q. Fan. “Formalizing Properties for Distributed System Testing”, Master Thesis in Preparation.Google Scholar
- 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.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.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
- 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.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.KLOCwork. Corporate website, http://www.KLOCwork.com/.
- 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.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.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.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.Pattern Specification System http://www.cis.ksu.edu/santos/spec-patterns.
- 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.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.The SMV System http://www-2.cs.cmu.edu/~modelcheck/smv.html.
- 28.A. Tanenbaum. “Computer Networks”. Prentice Hall, 1996.Google Scholar
- 29.Telelogic, “ObjectGEODE SDL Simulator Reference Manual”.Google Scholar
- 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.P. A. S. Ward, “A Framework Algorithm for Dynamic Centralized Dimension-Bounded Timestamps”, In Proc. of CASCON 2000, Mississauga, Ontario, Canada.Google Scholar