×

zbMATH — the first resource for mathematics

Automatic symmetry detection for Promela. (English) Zbl 1191.68411
Summary: We introduce a specification language, Promela-Lite, which captures the essential features of Promela but which, unlike Promela, has a formally defined semantics. We show how we can detect symmetry in specifications defined in Promela-lite by constructing a directed, coloured bipartite digraph called a static channel diagram, and applying computational group theoretic techniques. We extend our approach to Promela and introduce a tool, SymmExtractor, for automatically detecting symmetries of Promela specifications. We demonstrate the effectiveness of our approach via experimental results for a suite of Promela specifications. Unlike previous approaches our technique is fully automatic, and not restricted to fully symmetric systems.

MSC:
68Q60 Specification and verification (program logics, model checking, etc.)
PDF BibTeX XML Cite
Full Text: DOI
References:
[1] Aho, A., Sethi, R., Ullman, J.: Compilers–Principles, Techniques and Tools. Addison-Wesley, Reading (1986) · Zbl 1155.68020
[2] Bosnacki, D., Dams, D., Holenderski, L.: Symmetric spin. Int. J. Softw. Tools Technol. Transf. 4(1), 65–80 (2002) · Zbl 02178179 · doi:10.1007/s100090200074
[3] Cameron, P.: Permutation groups. London Mathematical Society Student Texts, vol. 45. Cambridge University Press, Cambridge (1999) · Zbl 0922.20003
[4] Cardelli, L.: Type systems. In: Tucker, A. (ed.) The Computer Science and Engineering Handbook, New York, USA, pp. 2208–2236. CRC, Boca Raton (1997)
[5] Clarke, E., Emerson, E.: Synthesis of synchronization skeletons for branching time temporal logic. In: Proceedings of the Workshop in Logic of Programs. Lecture Notes in Computer Science, Yorktown Heights, N.Y., vol. 131. Springer, New York (1981) · Zbl 0546.68014
[6] Clarke, E., Emerson, E., Jha, S., Sistla, A.: Symmetry reductions in model-checking. In: Hu, A., Vardi, M. (eds.) Proceedings of the 10th International Conference on Computer-aided Verification (CAV ’98). Lecture Notes in Computer Science, Vancouver, British Columbia, Canada, vol. 1427, pp. 147–158. Springer, New York (1998)
[7] Clarke, E., Emerson, E., Sistla, A.P.: Automatic verification of finite-state concurrent systems using temporal logic specifications. ACM Trans. Program. Lang. Syst. 8(2), 244–263 (1986) · Zbl 0591.68027 · doi:10.1145/5397.5399
[8] Clarke, E., Enders, R., Filkorn, T., Jha, S.: Exploiting symmetry in temporal logic model checking. Form. Methods Syst. Des. 9(1–2), 77–104 (1996) · Zbl 05475431 · doi:10.1007/BF00625969
[9] Clarke, E., Grumberg, O., Long, D.: Model checking and abstraction. ACM Trans. Program. Lang. Syst. 16(5), 1512–1542 (1994) · doi:10.1145/186025.186051
[10] Clarke, E., Grumberg, O., Peled, D.: Model Checking. MIT, Cambridge (1999)
[11] Cohn, P.: Algebra. Wiley, New York (1982)
[12] Darga, P., Liffiton, M., Sakallah, K., Markov, I.: Exploiting structure in symmetry detection for CNF. In: Proceedings of the 41st Annual Conference on Design Automation, San Diego, CA, USA, pp. 530–534. ACM, New York (2004)
[13] Derepas, F., Gastin, P.: Model checking systems of replicated processes with Spin. In: Dwyer, M.B. (ed.) Proceedings of the 8th International SPIN Workshop (SPIN 2001). Lecture Notes in Computer Science, Toronto, Canada, vol. 2057, pp. 235–251. Springer, New York (2001) · Zbl 0985.68521
[14] Dill, D., Drexler, A., Hu, A., Yang, C.H.: Protocol verification as a hardware design aid. In: Proceedings 1992 IEEE International Conference on Computer Design: VLSI in Computer & Processors (ICCD’92), Cambridge, MA, USA, pp. 522–525. IEEE Computer Society, Los Alamitos (1992)
[15] Donaldson, A.: Thesis website. http://www.dcs.gla.ac.uk/people/personal/ally/thesis/
[16] Donaldson, A., Miller, A., Calder, M.: Finding symmetry in models of concurrent systems by static channel diagram analysis. Electron. Notes Theor. Comp. Sci. 128(6), 161–177 (2005) · Zbl 05415159 · doi:10.1016/j.entcs.2005.04.010
[17] Donaldson, A.F.: Automatic Techniques for Detecting and Exploiting Symmetry in Model Checking. PhD Thesis. Department of Computing Science, University of Glasgow, UK (2007)
[18] Donaldson, A.F., Gay, S.: ETCH: an enhanced type checking tool for Promela. In: Godefroid, P. (ed.) Proceedings of the 12th International SPIN Workshop (SPIN 2005). Lecture Notes in Computer Science, Barcelona, Spain, vol. 3639, pp. 237–242. Springer, New York (2005)
[19] Donaldson, A.F., Miller, A.: Automatic symmetry detection for model checking using computational group theory. In: Fitzgerald, J., Hayes, I., Tarlecki, A. (eds.) Proceedings of the 13th International Symposium on Formal Methods (FM 2005). Lecture Notes in Computer Science, Newcastle, UK, vol. 3582, pp. 481–496. Springer, New York (2005) · Zbl 1120.68414
[20] Donaldson, A.F., Miller, A.: A computational group theoretic symmetry reduction package for the SPIN model checker. In: Proceedings of the 11th International Conference on Algebraic Methodology and Software Technology (AMAST’06). Lecture Notes in Computer Science, Kuressaare, Estonia, vol. 4019, pp. 374–380. Springer, New York (2006)
[21] Donaldson, A.F., Miller, A.: Exact and approximate strategies for symmetry reduction in model checking. In: Misra, J., Nipkow, T., Sekerinski, E. (eds.) Proceedings of the 14th International Symposium on Formal Methods (FM 2006). Lecture Notes in Computer Science, Hamilton, Ontario, Canada, vol. 4085, pp. 541–556. Springer, New York (2006)
[22] Donaldson, A.F., Miller, A.: Extending symmetry reduction techniques to a realistic model of computation. Electron. Notes Theor. Comput. Sci. 185, 63–76 (2007) · Zbl 05417753 · doi:10.1016/j.entcs.2007.05.029
[23] Emerson, E., Havlicek, J., Trefler, R.: Virtual symmetry reduction. In: Proceedings of the 15th Annual IEEE Symposium on Logic in Computer Science, Santa Barbara, CA, USA, pp. 121–131. IEEE Computer Society Press, Silver Spring (2000)
[24] Emerson, E., Sistla, A.: Symmetry and model checking. Form. Methods Syst. Des. 9(1–2), 105–131 (1996) · Zbl 05475432 · doi:10.1007/BF00625970
[25] Gaggnon, E., Handren, L.: SableCC, an object-oriented compiler framework. In: Proceedings of TOOLS USA, pp. 140–154. IEEE Computer Society, Los Alamitos (1998)
[26] Gap Group: GAP– Groups Algorithms and Programming, Version 4.4. Aachen, St. Andrews. http://www.gap-system.org/ (2006)
[27] Godefroid, P.: Exploiting symmetry when model-checking software (extended abstract). In: Wu, J., Chanson, S., Gao, Q. (eds.) Proceedings of the Joint International Conference on Formal Description Techniques for Distributed Systems and Communication Protocols and Protocol Specification, Testing and Verification (FORTE/PSTV ’99 ). International Federation For Information Processing, Beijing, China, vol. 156, pp. 257–275. Kluwer, Deventer (1999) · Zbl 0953.68520
[28] Holzmann, G.: The SPIN Model Checker: Primer and Reference Manual. Addison Wesley, Boston (2003)
[29] Igarashi, A., Pierce, B., Wadler, P.: Featherweight Java: a minimal core calculus for Java and GJ. ACM Trans. Prog. Lang. Syst. 23(3), 396–450 (2001) · Zbl 05459286 · doi:10.1145/503502.503505
[30] Ip, C., Dill, D.: Better verification through symmetry. Form. Methods Syst. Des. 9, 41–75 (1996) · Zbl 05475430 · doi:10.1007/BF00625968
[31] Larson, K., Pettersson, P., Yi, W.: UPPAAL in a nutshell. Softw. Tools Technol. Transf. 1(1/2), 134–152 (1997) · Zbl 1060.68577 · doi:10.1007/s100090050010
[32] McKay, B.: Nauty user’s guide (version 1.5). Technical Report TR-CS-90-02. Australian National University, Computer Science Department (1990)
[33] McMillan, K.L.: Symbolic Model Checking. Kluwer, Boston (1993) · Zbl 0784.68004
[34] Miller, A., Donaldson, A., Calder, M.: Symmetry in temporal logic model checking. Comput. Surv. 36(3), September (2006)
[35] Nalumasu, R., Gopalakrishnan, G.: Explicit-enumeration based verification made memory-efficient. In: Johnston, S. (ed.) Proceedings of the 12th IFIP International Conference on Computer Hardware Description Languages and their Applications (CHDL’95). IFIP, Chiba, Japan, pp. 617–622. Elsevier, Amsterdam (1995)
[36] Queille, J.P., Sifakis, J.: Specification and verification of concurrent systems in CÆSAR. In: Dezani-Ciancaglini, M., Montanari, U. (eds.) Proceedings of the 5th International Symposium on Programming. Lecture Notes in Computer Science, Torino, Italy, vol. 137, pp. 195–220. Springer, New York (1982) · Zbl 0482.68028
[37] Rose, J.: A Course in Group Theory. Dover, New York (1994) · Zbl 0818.11001
[38] Saffrey, P.: Optimising Communication Structure for Model Checking. PhD Thesis. Department of Computing Science, University of Glasgow, July (2003) · Zbl 1129.68448
[39] Sistla, A., Godefroid, P.: Symmetry and reduced symmetry in model checking. In: Berry, G., Comon, H., Finkel, A. (eds.) Proceedings of the 13th International Conference on Computer-aided Verification (CAV 2001). Lecture Notes in Computer Science, Paris, France, vol. 2102, pp. 91–103. Springer, New York (2001) · Zbl 0991.68543
[40] Sistla, A., Gyuris, V., Emerson, E.: SMC: a symmetry-based model checker for verification of safety and liveness properties. ACM Trans. Softw. Eng. Methodol. 9, 133–166 (2000) · doi:10.1145/350887.350891
[41] Tanenbaum, A., van Steen, M.: Distributed Systems Principles and Paradigms. Prentice Hall, Englewood Cliffs (2002) · Zbl 1157.68324
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. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.