Abstract
Symmetry reduction is a technique to alleviate state explosion in model checking by replacing a model of replicated processes with a bisimilar quotient model. The size of the quotient depends strongly on the set of applicable symmetries, which in many practical cases allows only polynomial reduction. We introduce architectural symmetry, a concept that exploits architectural system features to compensate for a lack of symmetry in the system model. We show that the standard symmetry quotient of an architecturally symmetric and well-architected model preserves arbitrary Boolean combinations and nestings of reachability properties. This quotient can be exponentially smaller than the model, even in cases where traditional symmetry reduction is nearly ineffective. Our technique thus extends the benefits of symmetry reduction to systems that are in fact not symmetric. Finally, we generalize our results to all architecturally symmetric models, including those that are not well-architected. We illustrate our method through examples and experimental data.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Asanovic, K., et al.: The landscape of parallel computing research: A view from Berkeley. Technical Report UCB/EECS-2006-183, EECS Department, University of California, Berkeley (2006)
Wahl, T., Blanc, N., Emerson, E.A.: SVISS: Symbolic verification of symmetric systems. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 459–462. Springer, Heidelberg (2008)
Candea, G., Cutler, J., Fox, A.: Improving availability with recursive microreboots: a soft-state system case study. Performance Evaluation (2004)
Chen, X., German, S., Gopalakrishnan, G.: Transaction based modeling and verification of hardware protocols. In: Formal Methods in Computer-Aided Design (FMCAD) (2007)
Clarke, E., Enders, R., Filkorn, T., Jha, S.: Exploiting symmetry in temporal logic model checking. In: Formal Methods in System Design (FMSD) (1996)
Emerson, A., Havlicek, J., Trefler, R.: Virtual symmetry reduction. In: Logic in Computer Science (LICS) (2000)
Emerson, A., Sistla, P.: Symmetry and model checking. Formal Methods in System Design (FMSD) (1996)
Emerson, A., Trefler, R.: From asymmetry to full symmetry: New techniques for symmetry reduction in model checking. In: Pierre, L., Kropf, T. (eds.) CHARME 1999. LNCS, vol. 1703, pp. 142–157. Springer, Heidelberg (1999)
Emerson, A., Wahl, T.: On combining symmetry reduction and symbolic representation for efficient model checking. In: Geist, D., Tronci, E. (eds.) CHARME 2003. LNCS, vol. 2860, pp. 216–230. Springer, Heidelberg (2003)
The FlexRay Consortium, FlexRay—The communication system for advanced automotive control applications, http://www.flexray.com
Heiner, G., Thurner, T.: Time-triggered architecture for safety-related distributed real-time systems in transportation systems. In: Fault-Tolerant Computing Symposium (FTCS) (1998)
Ip, N., Dill, D.: Better verification through symmetry. Formal Methods in System Design (FMSD) (1996)
Milner, R.: Operational and algebraic semantics of concurrent processes. In: Handbook of Theoretical Computer Science, Volume B: Formal Models and Semantics. MIT Press, Cambridge (1990)
Pnueli, A., Xu, J., Zuck, L.D.: Liveness with (0,1, ∞ )-counter abstraction. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol. 2404, p. 107. Springer, Heidelberg (2002)
Sistla, P., Godefroid, P.: Symmetry and reduced symmetry in model checking. Transactions on Programming Languages and Systems (TOPLAS) (2004)
Somenzi, F.: The CU Decision Diagram Package, release 2.3.1. University of Colorado at Boulder, http://vlsi.colorado.edu/~fabio/CUDD/
Wahl, T.: Adaptive symmetry reduction. In: Damm, W., Hermanns, H. (eds.) CAV 2007. LNCS, vol. 4590, pp. 393–405. Springer, Heidelberg (2007)
Wei, O., Gurfinkel, A., Chechik, M.: Identification and counter abstraction for full virtual symmetry. In: Borrione, D., Paul, W. (eds.) CHARME 2005. LNCS, vol. 3725, pp. 285–300. Springer, Heidelberg (2005)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2008 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Trefler, R., Wahl, T. (2008). Extending Symmetry Reduction by Exploiting System Architecture. In: Jones, N.D., Müller-Olm, M. (eds) Verification, Model Checking, and Abstract Interpretation. VMCAI 2009. Lecture Notes in Computer Science, vol 5403. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-93900-9_26
Download citation
DOI: https://doi.org/10.1007/978-3-540-93900-9_26
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-93899-6
Online ISBN: 978-3-540-93900-9
eBook Packages: Computer ScienceComputer Science (R0)