Symmetry and partial order reduction techniques in model checking Rebeca. (English) Zbl 1185.68142
Summary: Rebeca is an actor-based language with formal semantics which is suitable for modeling concurrent and distributed systems and protocols. Due to its object model, partial order and symmetry detection and reduction techniques can be efficiently applied to dynamic Rebeca models. We present two approaches for detecting symmetry in Rebeca models: One that detects symmetry in the topology of inter-connections among objects and another one which exploits specific data structures to reflect internal symmetry in the internal structure of an object. The former approach is novel in that it does not require any input from the modeler and can deal with the dynamic changes of topology. This approach is potentially applicable to a wide range of modeling languages for distributed and reactive systems. We have also developed a model checking tool that implements all of the above-mentioned techniques. The evaluation results show significant improvements in model size and model-checking time.
MSC:
| 68N15 | Theory of programming languages |
References:
| [1] | Abdulla, P.A., Jonsson, B., Kindahl, M., Peled, D.: A general approach to partial order reductions in symbolic verification (extended abstract). In: Hu, A.J., Vardi, M.Y. (eds.) [37], pp. 379–390 (1998) |
| [2] | Agha, G.: The structure and semantics of actor languages. In: Proceedings of the REX Workshop, pp. 1–59 (1990) |
| [3] | Alur, R., Brayton, R.K., Henzinger, T.A., Qadeer, S., Rajamani, S.K. (1997) Partial-order reduction in symbolic state space exploration. In: Grumberg, O. (ed.) Proceedings of Computer Aided Verification, 9th International Conference, CAV ’97, Haifa, Israel, June 22–25, LNCS, vol. 1254, pp. 340–351. Springer, Berlin (1997) · Zbl 1001.68080 |
| [4] | Behjati, R., Sabouri, H., Razavi, N., Sirjani, M.: An effective approach for model checking SystemC designs. In: Proceedings of International Conference on Application of Concurrency to System Design (ACSD’08), pp. 56–61 (2008) |
| [5] | Bosnacki, D.: A light-weight algorithm for model checking with symmetry reduction and weak fairness. In: Ball, T., Rajamani, S.K. (eds.) Proceedings of Model Checking Software, 10th International SPIN Workshop. Portland, OR, USA, May 9–10, LNCS, vol. 2648, pp. 89–103. Springer, Berlin (2003) |
| [6] | Bosnacki, D., Dams, D., Holenderski, L.: A heuristic for symmetry reductions with scalarsets. In: Proceedings of the International Symposium of Formal Methods Europe (FM’01), Lecture Notes in Computer Science, vol. 2021, pp. 518–533. Springer, Berlin (2001) · Zbl 0977.68585 |
| [7] | Bosnacki D., Dams D., Holenderski L.: Symmetric SPIN. Int. J. Softw. Tools Technol. Transf. (STTT) 4(1), 92–106 (2002) · doi:10.1007/s100090200074 |
| [8] | Bosnacki, D., Donaldson, A.F., Leuschel, M., Massart, T.: Efficient approximate verification of promela models via symmetry markers. In: Proceedings of the 5th International Symposium on Automated Technology for Verification and Analysis (ATVA’07), Lecture Notes in Computer Science, vol. 4762, pp. 300–315. Springer, Berlin (2007) · Zbl 1141.68453 |
| [9] | Bosnacki, D., Edelkamp, S. (eds.): In: Proceedings of Model Checking Software, 14th International SPIN Workshop, Berlin, Germany, July 1–3, LNCS, vol. 4595. Springer, Berlin (2007) |
| [10] | Chang, P.H., Agha, G.: Supporting reconfigurable object distribution for customized web applications. In: The 22nd Annual ACM Symposium on Applied Computing (SAC), pp. 1286–1292 (2007) |
| [11] | Chang, P.H., Agha, G.: Towards context-aware web applications. In: 7th IFIP International Conference on Distributed Applications and Interoperable Systems (DAIS), pp. 239–252 (2007) |
| [12] | Cheong, E., Lee, E.A., Zhao, Y.: Viptos: a graphical development and simulation environment for tinyos-based wireless sensor networks. In: Proceedings of the 3rd International Conference on Embedded Networked Sensor Systems, SenSys 2005, pp. 302–302 (2005) |
| [13] | Clarke, E.M., Emerson, E.A., Jha, S., Sistla, A.P.: Symmetry reductions in model checking. In: Hu, A.J., Vardi, M.Y. (eds.) [37], pp. 147–158 (1986) |
| [14] | Clarke E.M., Grumberg O., Peled D.A.: Model Checking. MIT Press, Cambridge (1999) |
| [15] | Clarke E.M., Jha S., Enders R., Filkorn T.: Exploiting symmetry in temporal logic model checking. Formal Methods Syst. Des. 9(1/2), 77–104 (1996) · doi:10.1007/BF00625969 |
| [16] | Clarke, E.M., Kurshan, R.P. (eds.): In: Proceedings of Computer Aided Verification, 2nd International Workshop, CAV ’90, New Brunswick, NJ, USA, June 18–21, LNCS, vol. 531. Springer, Berlin (1990) |
| [17] | Donaldson, A.F., Miller, A.: Automatic symmetry detection for model checking using computational group theory. In: Proceedings of the International Symposium of Formal Methods Europe (FM’05), Lecture Notes in Computer Science, vol. 3582, pp. 481–496. Springer, Berlin (2005) · Zbl 1120.68414 |
| [18] | Donaldson A.F., Miller A.: Extending symmetry reduction techniques to a realistic model of computation. Electron. Notes Theor. Comput. Sci. 185, 63–76 (2007) · doi:10.1016/j.entcs.2007.05.029 |
| [19] | Donaldson A.F., Miller A., Calder M.: Finding symmetry in models of concurrent systems by static channel diagram analysis. Electron. Notes Theor. Comput. Sci. 128(6), 161–177 (2005) · doi:10.1016/j.entcs.2005.04.010 |
| [20] | Donaldson A.F., Miller A., Calder M.: Spin-to-Grape: A tool for analysing symmetry in Promela models. Electron. Notes Theor. Comput. Sci. 139(1), 3–23 (2005) · doi:10.1016/j.entcs.2005.09.007 |
| [21] | Emerson E., Sistla A.: Symmetry and model checking. Formal Methods Syst. Des. 9(1–2), 105–131 (1996) · doi:10.1007/BF00625970 |
| [22] | Emerson, E.A., Jha, S., Peled, D.: Combining partial order and symmetry reductions. In: Brinksma, E. (ed.) Proceedings of Tools and Algorithms for Construction and Analysis of Systems, Third International Workshop, TACAS ’97, Enschede, The Netherlands, April 2–4, LNCS, vol. 1217, pp. 19–34. Springer, Berlin (1997) |
| [23] | Emerson, E.A., Sistla, A.P.: Utilizing symmetry when model checking under fairness assumptions: An automata-theoretic approach. In: Wolper, P. (ed.) Proceedings of Computer Aided Verification, 7th International Conference, Liege, Belgium, July, 3–5, LNCS, vol. 939, pp. 309–324. Springer, Berlin (1995) |
| [24] | Emerson, E.A., Wahl, T.: On combining symmetry reduction and symbolic representation for efficient model checking. In: Geist, D., Tronci, E. (eds.) Proceedings of the 12th IFIP WG 10.5 Advanced Research Working Conference, CHARME ’03, LNCS, vol. 2860, pp. 216–230. Springer, Berlin (2003) · Zbl 1179.68082 |
| [25] | Evangelista, S., Pajault, C.: Some solutions to the ignoring problem. In: Bosnacki, D., Edelkamp, S. (eds.) [9], pp. 76–94 (2007) |
| [26] | Flanagan, C., Godefroid, P.: Dynamic partial-order reduction for model checking software. In: Proceedings of the 32nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pp. 110–121. ACM Press, New York (2005) · Zbl 1369.68135 |
| [27] | Godefroid, P.: Using partial orders to improve automatic verification methods. In: Clarke, E.M., Kurshan, R.P. (eds.) [16], pp. 176–185 (1996) · Zbl 0765.68122 |
| [28] | Gueta, G., Flanagan, C., Yahav, E., Sagiv, M.: Cartesian partial-order reduction. In: Bosnacki, D., Edelkamp, S. (eds.) [9], pp. 95–112 (2009) |
| [29] | Hendriks, M., Behrmann, G., Larsen, K.G., Niebert, P., Vaandrager, F.W.: Adding symmetry reduction to UPPAAL. In: Larsen, K.G., Niebert, P. (eds.) Proceedings of Formal Modeling and Analysis of Timed Systems: First International Workshop, FORMATS ’03, Marseille, France, September 6–7, LNCS, vol. 2791, pp. 46–59. Springer, Berlin (2003) · Zbl 1099.68657 |
| [30] | Herstein, I.: Topics in Algebra. Xerox (1964) · Zbl 0122.01301 |
| [31] | Hewitt, C.: Procedural embedding of knowledge in planner. In: Proceedings of the 2nd International Joint Conference on Artificial Intelligence, pp. 167–184 (1971) |
| [32] | Hewitt, C.: What is commitment? physical, organizational, and social (revised). In: Proceedings of Coordination, Organizations, Institutions, and Norms in Agent Systems II, Lecture Notes in Computer Science, pp. 293–307. Springer, Berlin (2007) |
| [33] | Hojjat, H., Nokhost, H., Sirjani, M.: Formal verification of the IEEE 802.1D spanning tree protocol using extended Rebeca. In: Proceedings of the First International Conference on Fundamentals of Software Engineering (FSEN’05), ENTCS, vol. 159, pp. 139–159. Elsevier, Amsterdam (2006) |
| [34] | Holzmann G.J.: The model checker SPIN. IEEE Trans. Softw. Eng. 23(5), 279–295 (1997) · doi:10.1109/32.588521 |
| [35] | Holzmann, G.J., Peled, D.: An improvement in formal verification. In: Hogrefe, D. Leue, S. (eds.) Proceedings of the 7th IFIP WG6.1 International Conference on Formal Description Techniques, vol. 6, pp. 197–211. Chapman & Hall, London (1995) |
| [36] | Holzmann, G.J., Peled, D., Yannakakis, M.: On nested depth first search. In: Proceedings of the Second SPIN Workshop, pp. 23–32. American Mathematical Society, Providence, RI (1996) · Zbl 0880.68084 |
| [37] | Hu, A.J., Vardi, M.Y. (eds.): In: Proceedings of Computer Aided Verification, 10th International Conference, CAV ’98, Vancouver, BC, Canada, June 28–July 2, LNCS, vol. 1427. Springer, Berlin (1998) |
| [38] | Iosif, R.: Symmetry reduction criteria for software model checking. In: Bosnacki, D. Leue S. (eds.) Proceedings of Model Checking of Software, 9th International SPIN Workshop, Grenoble, France, April 11–13, LNCS, vol. 2318, pp. 22–41. Springer, Berlin (2002) · Zbl 1077.68686 |
| [39] | Ip C., Dill D.: Better verification through symmetry. Formal Methods Syst. Des. 9(1–2), 41–75 (1996) · doi:10.1007/BF00625968 |
| [40] | Ip, C.N.: State reduction methods for automatic formal verification. Ph.D. Thesis, Department of Computer Science, Stanford University (1996) |
| [41] | Jaghoori, M.M., Movaghar, A., Sirjani, M.: Modere: the model-checking engine of Rebeca. In: Haddad, H. (ed.) Proceedings of ACM Symposium on Applied Computing (SAC ’06), Dijon, France, April 23–27, pp. 1810–1815. ACM, New york (2006) |
| [42] | Jaghoori, M.M., Sirjani, M., Mousavi, M.R., Movaghar, A.: Efficient symmetry reduction for an actor-based model. In: Chakraborty, G. (ed.) Proceedings of Distributed Computing and Internet Technology, Second International Conference, ICDCIT ’05, Bhubaneswar, India, December 22–24, LNCS, vol. 3816, pp. 494–507. Springer, Berlin (2005) |
| [43] | Kakoee, M.R., Shojaei, H., Ghasemzadeh, H., Sirjani, M., Navabi, Z.: A new approach for design and verification of transaction level models. In: Proceedings of IEEE International Symposium on Circuit and Sytems (ISCAS ’07), pp. 3760–3763 (2007) |
| [44] | Kurshan, R.P., Levin, V., Minea, M., Peled, D., Yenigün, H.: Static partial order reduction. In: Steffen, B. (ed.) Proceedings of Tools and Algorithms for Construction and Analysis of Systems, 4th International Conference, TACAS ’98, Lisbon, Portugal, March 28–April 4, LNCS, vol. 1384, pp. 345–357. Springer, Berlin (1998) |
| [45] | Lee E.A., Neuendorffer S., Wirthlin M.J.: Actor-oriented design of embedded hardware and software systems. J. Circuits, Syst., Comput. 12(3), 231–260 (2003) · doi:10.1142/S0218126603000751 |
| [46] | Leuschel, M., Massart, T.: Efficient approximate verification of B via symmetry markers. In: Proceedings of the International Symmetry Conference, Edinburgh, UK, pp. 71v–85 (2007) · Zbl 1141.68453 |
| [47] | McMillan K.: Symbolic Model Checking. Kluwer Academic, Boston (1993) · Zbl 0784.68004 |
| [48] | Miller, A., Donaldson, A.F., Calder, M.: Symmetry in temporal logic model checking. ACM Comput. Surv. 38(3), Article no. 8 (2006) |
| [49] | Nalumasu R., Gopalakrishnan G.: An efficient partial order reduction algorithm with an alternate proviso implementation. Formal Methods Syst. Des. 20(3), 231–247 (2002) · Zbl 1017.68069 · doi:10.1023/A:1014728912264 |
| [50] | Peled, D.: All from one, one for all: on model checking using representatives. In: Courcoubetis, C. (ed.) CAV, LNCS, vol. 697, pp. 409–423. Springer, Berlin (1993) |
| [51] | Saboori, H., Sirjani, M.: Slicing-based reductions for Rebeca. In: Proceedings of FACS’08, ENTCS, pp. 57–71. Elsevier, Amsterdam (2008). To be published |
| [52] | Saïdi, H.: Discovering symmetries. In: 11th International Workshop on Formal Methods: Applications and Technology (FMICS/PDMC’06), LNCS, vol. 4346, pp. 67–83. Springer, Berlin (2006) |
| [53] | Schneider, S.: The B-Method: An Introduction. Palgrave (2001) |
| [54] | Shahriari, H.R., Makarem, M.S., Sirjani, M., Jalili, R., Movaghar, A.: Modeling and verification of complex network attacks using an actor-based language. In: Proceedings of the 11th Annual International CSI Computer Conference, pp. 152–158 (2006) |
| [55] | Sirjani M., Movaghar A., Shali A., de Boer F.S.: Modeling and verification of reactive systems using Rebeca. Fundamamenta Informaticae 63(4), 385–410 (2004) · Zbl 1082.68007 |
| [56] | Sirjani M., Movaghar A., Shali A., de Boer F.S.: Model checking, automated abstraction and compositional verification of Rebeca models. J Univers. Comput. Sci. (JUCS) 11(6), 1054–1082 (2005) |
| [57] | Sirjani M., SeyedRazi H., Movaghar A., Jaghoori M.M., Forghanizadeh S., Mojdeh M.: Model checking CSMA/CD protocol using an actor-based language. WSEAS Trans. Circuits Syst. 3(4), 1052–1057 (2004) |
| [58] | Sirjani, M., Shali, A., Jaghoori, M.M., Iravanchi, H., Movaghar, A.: A front-end tool for automated abstraction and modular verification of actor-based models. In: Proceedings of International Conference on Application of Concurrency to System Design (ACSD ’04), pp. 145–150. IEEE Computer Society, Silver Spring (2004) |
| [59] | Sistla A.P., Gyuris V., Emerson E.A.: SMC: a symmetry-based model checker for verification of safety and liveness properties. ACM Trans. Softw. Eng. Methodol. 9(2), 133–166 (2000) · doi:10.1145/350887.350891 |
| [60] | Valmari, A.: A stubborn attack on state explosion. In: Clarke, E.M., Kurshan R.P. (eds.) [16], pp. 156–165 (1996) · Zbl 0765.68147 |
| [61] | Vardi, M.Y.: Automata-theoretic model checking revisited. In: Proceedings of the 8th VMCAI, LNAI, vol. 4349, pp. 137–150 (2007) · Zbl 1132.68483 |
| [62] | Vardi, M.Y., Wolper, P.: An automata theoretic approach to automatic program verification. In: Kozen, D. (ed.) Proceedings of Symposium on Logic in Computer Science, pp. 322–331. IEEE Computer Society, Silver Spring (1986) |
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.
