Abstract
Model checking is a powerful and widespread technique for the verification of finite state concurrent systems. However, the main hindrance for wider application of this technique is the well-known state explosion problem. In [16], we proposed an incremental and compositional verification approach where the system model is partitioned according to the actions occurring in the property to be verified and where the environment of a component is taken into account. But the verification at each increment might be costly. On the other hand, Symbolic Observation Graphs provide a compact analysis means for LTL∖X properties. We have shown a purely modular construction of these in [15]. Therefore, in this paper, we combine both techniques to benefit from their pros. Also, we propose a novel approach for incrementally checking the validity of the counter-example.
Access provided by Autonomous University of Puebla. Download to read the full chapter text
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
Ball, T., Rajamani, S.K.: Automatically Validating Temporal Safety Properties of Interfaces. In: Dwyer, M.B. (ed.) SPIN 2001. LNCS, vol. 2057, pp. 103–122. Springer, Heidelberg (2001)
Bryant, R.E.: Symbolic boolean manipulation with ordered binary-decision diagrams. ACM Computing Surveys 24(3), 293–318 (1992)
Clarke, E.M., Grumberg, O., Jha, S., Lu, Y., Veith, H.: Counterexample-Guided Abstraction Refinement. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol. 1855, pp. 154–169. Springer, Heidelberg (2000)
Clarke, E.M., Long, D.E., McMillan, K.L.: Compositional model checking. In: LICS 1989, pp. 353–362 (1989)
Cobleigh, J.M., Avrunin, G.S., Clarke, L.A.: Breaking up is hard to do: An evaluation of automated assume-guarantee reasoning. ACM Trans. Softw. Eng. Methodol. 17(2), 7:1–7:52 (2008)
Das, S., Dill, D.L.: Successive approximation of abstract transition relations. In: Proceedings of the 16th Annual IEEE Symposium on Logic in Computer Science, LICS 2001, p. 51. IEEE Computer Society, Washington, DC (2001)
Duret-Lutz, A., Klai, K., Poitrenaud, D., Thierry-Mieg, Y.: Self-Loop Aggregation Product — A New Hybrid Approach to On-the-Fly LTL Model Checking. In: Bultan, T., Hsiung, P.-A. (eds.) ATVA 2011. LNCS, vol. 6996, pp. 336–350. Springer, Heidelberg (2011)
Goltz, U., Kuiper, R., Penczek, W.: Propositional Temporal Logics and Equivalences. In: Cleaveland, W.R. (ed.) CONCUR 1992. LNCS, vol. 630, pp. 222–236. Springer, Heidelberg (1992)
Haddad, S., Ilié, J.-M., Klai, K.: Design and Evaluation of a Symbolic and Abstraction-Based Model Checker. In: Wang, F. (ed.) ATVA 2004. LNCS, vol. 3299, pp. 196–210. Springer, Heidelberg (2004)
Henzinger, T.A., Jhala, R., Majumdar, R., Sutre, G.: Lazy abstraction. SIGPLAN Not. 37(1), 58–70 (2002)
Hoare, C.A.R.: Communicating sequential process. Communication of the ACM 21(8), 666–677 (1978)
Kaivola, R., Valmari, A.: The Weakest Compositional Semantic Equivalence Preserving Nexttime-less Linear Temporal Logic. In: Cleaveland, W.R. (ed.) CONCUR 1992. LNCS, vol. 630, pp. 207–221. Springer, Heidelberg (1992)
Klai, K., Haddad, S., Ilié, J.-M.: Modular Verification of Petri Nets Properties: A Structure-Based Approach. In: Wang, F. (ed.) FORTE 2005. LNCS, vol. 3731, pp. 189–203. Springer, Heidelberg (2005)
Klai, K., Ochi, H.: Modular verification of inter-enterprise business processes. In: eKNOW, pp. 155–161 (2012)
Klai, K., Petrucci, L.: Modular construction of the symbolic observation graph. In: Billington, J., Duan, Z., Koutny, M. (eds.) ACSD, pp. 88–97. IEEE (2008)
Klai, K., Petrucci, L., Reniers, M.: An Incremental and Modular Technique for Checking LTL∖X Properties of Petri Nets. In: Derrick, J., Vain, J. (eds.) FORTE 2007. LNCS, vol. 4574, pp. 280–295. Springer, Heidelberg (2007)
Klai, K., Poitrenaud, D.: MC-SOG: An LTL Model Checker Based on Symbolic Observation Graphs. In: van Hee, K.M., Valk, R. (eds.) PETRI NETS 2008. LNCS, vol. 5062, pp. 288–306. Springer, Heidelberg (2008)
Lakos, C., Petrucci, L.: Modular analysis of systems composed of semiautonomous subsystems. In: ACSD, pp. 185–194. IEEE Computer Society Press (2004)
Lehmann, A., Lohmann, N., Wolf, K.: Stubborn Sets for Simple Linear Time Properties. In: Haddad, S., Pomello, L. (eds.) PETRI NETS 2012. LNCS, vol. 7347, pp. 228–247. Springer, Heidelberg (2012)
Manna, Z., Pnueli, A.: The temporal logic of reactive and concurrent systems. Springer-Verlag New York, Inc., New York (1992)
Peled, D., Valmari, A., Kokkarinen, I.: Relaxed visibility enhances partial order reduction. Formal Methods in System Design 19(3), 275–289 (2001)
Pnueli, A.: In transition from global to modular temporal reasoning about programs. In: Logics and Models of Concurrent Systems, pp. 123–144. Springer-Verlag New York, Inc. (1985)
Puhakka, A., Valmari, A.: Weakest-Congruence Results for Livelock-Preserving Equivalences. In: Baeten, J.C.M., Mauw, S. (eds.) CONCUR 1999. LNCS, vol. 1664, pp. 510–524. Springer, Heidelberg (1999)
Saïdi, H.: Model Checking Guided Abstraction and Analysis. In: Palsberg, J. (ed.) SAS 2000. LNCS, vol. 1824, pp. 377–396. Springer, Heidelberg (2000)
Valmari, A.: On-the-fly Verification with Stubborn Sets. In: Courcoubetis, C. (ed.) CAV 1993. LNCS, vol. 697, pp. 397–408. Springer, Heidelberg (1993)
Valmari, A.: Compositionality in State Space Verification Methods. In: Billington, J., Reisig, W. (eds.) ICATPN 1996. LNCS, vol. 1091, pp. 29–56. Springer, Heidelberg (1996)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2012 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
André, É., Klai, K., Ochi, H., Petrucci, L. (2012). A Counterexample-Based Incremental and Modular Verification Approach. In: Calinescu, R., Garlan, D. (eds) Large-Scale Complex IT Systems. Development, Operation and Management. Monterey Workshop 2012. Lecture Notes in Computer Science, vol 7539. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-34059-8_15
Download citation
DOI: https://doi.org/10.1007/978-3-642-34059-8_15
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-34058-1
Online ISBN: 978-3-642-34059-8
eBook Packages: Computer ScienceComputer Science (R0)