Abstract
The observation of a distributed system’s finite execution can be abstracted as a partial ordered set of events generally called finite (partial order) trace. In practice, this trace can be obtained through a standard code instrumentation, which takes advantage of existing communications between processes to partially order events of different processes. We show that testing that such a distributed execution satisfies some global property amounts therefore to model check the corresponding trace. This work can be time consuming; we therefore provide an efficient symbolic Ctl model-checking algorithm for traces. This method is based on a symbolic data structure, called Interval Sharing Trees, allowing to efficiently represent and manipulate sets of k-uples of naturals. Efficient symbolic operations are defined on this data structure in order to deal with all Ctl modalities. We show that in practice this data structure is well adapted for Ctl model checking of traces.
Chapter PDF
Similar content being viewed by others
Keywords
References
De Wachter, B., Massart, T., Meuter, C.: dSL: An Environment with Automatic Code Distribution for Industrial Control Systems. In: Papatriantafilou, M., Hunel, P. (eds.) OPODIS 2003. LNCS, vol. 3144, pp. 132–145. Springer, Heidelberg (2004)
De Wachter, B., Genon, A., Massart, T., Meuter, C.: The Formal Design of Distributed Controllers with dSL and Spin. Formal Aspects of Computing 17(2), 177–200 (2005)
Massart, T.: A Calculus to Define Correct Tranformations of LOTOS Specifications. In: FORTE ’91, pp. 281–296. North-Holland, Amsterdam (1992)
Holzmann, G.J.: The Model Checker SPIN. IEEE Trans. Software Eng. 23(5), 279–295 (1997)
McMillan, K.: The SMV System. Technical Report CMU-CS-92-131, Carnegie Mellon University (1992)
Cimatti, A., Clarke, E.M., Giunchiglia, E., Giunchiglia, F., Pistore, M., Roveri, M., Sebastiani, R., Tacchella, A.: NuSMV 2: An OpenSource Tool for Symbolic Model Checking. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol. 2404, pp. 359–364. Springer, Heidelberg (2002)
Godefroid, P.: Partial-Order Methods for the Verification of Concurrent Systems - An Approach to the State-Explosion Problem. In: Godefroid, P. (ed.) Partial-Order Methods for the Verification of Concurrent Systems. LNCS, vol. 1032, Springer, Heidelberg (1996)
Valmari, A.: On-the-fly verification with stubborn sets. In: Courcoubetis, C. (ed.) CAV 1993. LNCS, vol. 697, pp. 397–408. Springer, Heidelberg (1993)
Clarke, E., Grumberg, O., Peled, D.: Model Checking. The MIT Press, Cambridge (1999)
McMillan, K.L.: Symbolic model checking: an approach to the state explosion problem. Carnegie Mellon University (1992)
Bryant, R.E.: Symbolic boolean manipulation with ordered binary-decision diagrams. ACM Comput. Surv. 24(3), 293–318 (1992)
Lamport, L.: Time, clocks, and the ordering of events in a distributed system. Commun. ACM 21(7), 558–565 (1978)
Mattern, F.: Virtual time and global states of distributed systems. In: Proc. Workshop on Parallel and Distributed Algorithms, North-Holland / Elsevier, pp. 215–226 (1989)
Chase, C.M., Garg, V.K.: Detection of global predicates: Techniques and their limitations. Distributed Computing 11(4), 191–201 (1998)
Sen, A., Garg, V.K.: Detecting temporal logic predicates in distributed programs using computation slicing. In: OPODIS, pp. 171–183 (2003)
Clarke, E.M., Emerson, E.A.: Design and synthesis of synchronization skeletons using branching-time temporal logic. In: Logic of Programs, pp. 52–71 (1981)
Mittal, N., Garg, V.K.: Computation slicing: Techniques and theory. In: DISC, pp. 78–92 (2001)
Ganty, P., Meuter, C., Begin, L.V., Kalyon, G., Raskin, J.F., Delzanno, G.: Symbolic data structure for sets of k-uples of integers. Technical Report 570, Département d’Informatique - Université Libre de Bruxelles (2006)
Ganty, P.: Algorithmes et structures de données efficaces pour la manipulation de contraintes sur les intervalles. Master’s thesis, Université Libre de Bruxelles (2002)
Mazurkiewicz, A.W.: Trace theory. In: Advances in Petri Nets, pp. 279–324 (1986)
Thiagarajan, P.S.: A trace based extension of linear time temporal logic. In: Abramsky, S. (ed.) LICS 1994. Proceedings of the Ninth Annual IEEE Symp. on Logic in Computer Science, pp. 438–447. IEEE Computer Society Press, Los Alamitos (1994)
Alur, R., Peled, D., Penczek, W.: Model checking of causality properties. In: Proceedings of the 10th Annual IEEE Symposium on Logic in Computer Science (LICS’95), San Diego, California, pp. 90–100 (1995)
Niebert, P., Peled, D.: Efficient model checking for ltl with partial order snapshots. In: Hermanns, H., Palsberg, J. (eds.) TACAS 2006 and ETAPS 2006. LNCS, vol. 3920, pp. 272–286. Springer, Heidelberg (2006)
Thiagarajan, P.S., Walukiewicz, I.: An expressively complete linear time temporal logic for mazurkiewicz traces. Inf. Comput. 179(2), 230–249 (2002)
Diekert, V., Gastin, P.: LTL is expressively complete for Mazurkiewicz traces. Journal of Computer and System Sciences 64(2), 396–418 (2002)
Nielsen, M., Plotkin, G.D., Winskel, G.: Petri nets, event structures and domains, part i. Theor. Comput. Sci. 13, 85–108 (1981)
Chandy, K.M., Lamport, L.: Distributed snapshots: Determining global states of distributed systems. ACM Trans. Comput. Syst. 3(1), 63–75 (1985)
Charron-Bost, B., Delporte-Gallet, C., Fauconnier, H.: Local and temporal predicates in distributed systems. ACM Trans. Program. Lang. Syst. 17(1) (1995)
Garg, V.K., Waldecker, B.: Detection of weak unstable predicates in distributed programs. IEEE Trans. Parallel Distrib. Syst. 5(3), 299–307 (1994)
Garg, V.K., Waldecker, B.: Detection of strong unstable predicates in distributed programs. IEEE Trans. Parallel Distrib. Syst. 7(12), 1323–1333 (1996)
Garg, V.K., Mittal, N.: On slicing a distributed computation. In: ICDCS, pp. 322–329 (2001)
Jard, C., Jéron, T., Jourdan, G.V., Rampon, J.X.: A general approach to trace-checking in distributed computing systems. In: ICDCS, pp. 396–403 (1994)
Sen, K., Rosu, G., Agha, G.: Online efficient predictive safety analysis of multithreaded programs. In: Jensen, K., Podelski, A. (eds.) TACAS 2004. LNCS, vol. 2988, pp. 123–138. Springer, Heidelberg (2004)
Sen, K., Rosu, G., Agha, G.: Detecting errors in multithreaded programs by generalized predictive analysis of executions. In: Steffen, M., Zavattaro, G. (eds.) FMOODS 2005. LNCS, vol. 3535, pp. 211–226. Springer, Heidelberg (2005)
Genon, A., Massart, T., Meuter, C.: Monitoring distributed controllers: When an efficient ltl algorithm on sequences is needed to model-check traces. In: Misra, J., Nipkow, T., Sekerinski, E. (eds.) FM 2006. LNCS, vol. 4085, pp. 557–572. Springer, Heidelberg (2006)
Zampunieris, D., Le Charlier, B.: Efficient handling of large sets of tuples with sharing trees. In: Proceedings of the 5th Data Compression Conference (DCC’95), p. 428. IEEE Computer Society Press, Los Alamitos (1995)
Ammirati, P., Delzanno, G., Ganty, P., Geeraerts, G., Raskin, J.F., Van Begin, L.: Babylon: An integrated toolkit for the specification and verification of parameterized systems. In: 2nd workshop on Specification, Analysis and Validation for Emerging technologies (SAVE02) (2002)
Kalyon, G., Massart, T., Meuter, C., Van Begin, L.: Testing Distributed System through Symbolic Model Checking. Technical Report 571, Département d’Informatique - Université Libre de Bruxelles (2007)
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 2007 IFIP International Federation for Information Processing
About this paper
Cite this paper
Kalyon, G., Massart, T., Meuter, C., Van Begin, L. (2007). Testing Distributed Systems Through Symbolic Model Checking. In: Derrick, J., Vain, J. (eds) Formal Techniques for Networked and Distributed Systems – FORTE 2007. FORTE 2007. Lecture Notes in Computer Science, vol 4574. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-73196-2_17
Download citation
DOI: https://doi.org/10.1007/978-3-540-73196-2_17
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-73195-5
Online ISBN: 978-3-540-73196-2
eBook Packages: Computer ScienceComputer Science (R0)