Abstract
One approach to verify a property expressed as a modal \(\mu \)-calculus formula on a system with several concurrent processes is to build the underlying state space compositionally (i.e., by minimizing and recomposing the state spaces of individual processes, keeping visible only the relevant actions occurring in the formula), and check the formula on the resulting state space. It was shown previously that, when checking the formulas of the \(L_{\mu }^{ dsbr }\) fragment of \(\mu \)-calculus (consisting of weak modalities only), individual processes can be minimized modulo divergence-preserving branching (divbranching) bisimulation. In this paper, we refine this approach to handle formulas containing both strong and weak modalities, so as to enable a combined use of strong or divbranching bisimulation minimization on concurrent processes depending whether they contain or not the actions occurring in the strong modalities of the formula. We extend \(L_{\mu }^{ dsbr }\) with strong modalities and show that the combined minimization approach preserves the truth value of formulas of the extended fragment. We implemented this approach on top of the CADP verification toolbox and demonstrated how it improves the capabilities of compositional verification on realistic examples of concurrent systems.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Similar content being viewed by others
Notes
- 1.
For instance, the composition of P and Q where action a of P synchronizes with either b or c of Q, can be written as \(\rho (P)\,|[b, c]|\,Q\), where \(\rho \) maps a onto \(\{b, c\}\).
- 2.
For instance, \(P_1\,|[a]|\,(P_2\,|[]|\,P_3)\) is equivalent to \(\rho _0((\rho _1(P_1)\,|[a_1]|\,\rho _2(P_2))\,|[a_2]|\,\rho _3(P_3))\) —observe the different associativity— where \(\rho _1\) maps a onto \(\{a_1, a_2\}\), \(\rho _2\) renames a into \(a_1\), \(\rho _3\) renames a into \(a_2\), and \(\rho _0\) renames \(a_1\) and \(a_2\) into a.
- 3.
\(\mu \)ACTL\(\setminus \)X denotes ACTL\(\setminus \)X plus fixed points. The authors of [24] claim that \(L_{\mu }^{ dsbr }\) is as expressive as \(\mu \)ACTL\(\setminus \)X, but they omit that the \(\langle \varphi _1?.\alpha _{\tau } \rangle \,@\) weak infinite looping modality cannot be expressed in \(\mu \)ACTL\(\setminus \)X.
- 4.
Theorem 2 generalizes easily to more general compositions \(P\,||\,Q\) (with admissible action mappings) if Q does not contain any action that maps onto a strong action.
- 5.
- 6.
Specification available at ftp://ftp.inrialpes.fr/pub/vasy/demos/demo_05.
- 7.
References
Andersen, H.R.: Partial model checking. In: Proceedings of the 10th Annual IEEE Symposium on Logic in Computer Science LICS, San Diego, California, USA, pp. 398–407. IEEE Computer Society Press, June 1995
Brookes, S.D., Hoare, C.A.R., Roscoe, A.W.: A Theory of communicating sequential processes. J. ACM 31(3), 560–599 (1984)
Champelovier, D., et al.: Reference manual of the LNT to LOTOS translator (Version 6.7), INRIA, Grenoble, France, July 2017
Cheung, S.C., Kramer, J.: Enhancing compositional reachability analysis with context constraints. In: Proceedings of the 1st ACM SIGSOFT International Symposium on the Foundations of Software Engineering, Los Angeles, CA, USA, pp. 115–125. ACM Press, December 1993
Clarke, E.M., Emerson, E.A., Sistla, A.P.: Automatic verification of finite-state concurrent systems using temporal logic specifications. ACM Trans. Program. Lang. Syst. 8(2), 244–263 (1986)
Crouzen, P., Lang, F.: Smart reduction. In: Giannakopoulou, D., Orejas, F. (eds.) FASE 2011. LNCS, vol. 6603, pp. 111–126. Springer, Heidelberg (2011). https://doi.org/10.1007/978-3-642-19811-3_9
de Putter, S., Wijs, A., Lang, F.: Compositional Model Checking is Lively – Extended Version 2018. Submitted to Science of Computer Programming (2018)
Fantechi, A., Gnesi, S., Ristori, G.: From ACTL to \(\mu \)-calculus (extended abstract). In: Proceedings of the Workshop on Theory and Practice in Verification. ERCIM (1992)
Fischer, M.J., Ladner, R.E.: Propositional dynamic logic of regular programs. J. Comput. Syst. Sci. 18(2), 194–211 (1979)
Garavel, H., Lang, F.: SVL: a scripting language for compositional verification. In: Kim, M., Chin, B., Kang, S., Lee, D. (eds.) FORTE 2001. IFIP, vol. 69, pp. 377–392. Springer, Boston, MA (2002). https://doi.org/10.1007/0-306-47003-9_24
Garavel, H., Lang, F., Mateescu, R.: Compositional verification of asynchronous concurrent systems using CADP. Acta Informatica 52(4), 337–392 (2015)
Garavel, H., Lang, F., Mateescu, R., Serwe, W.: CADP 2011: a toolbox for the construction and analysis of distributed processes. Int. J. Softw. Tools Technol. Transf. (STTT) 15(2), 89–107 (2013)
Garavel, H., Thivolle, D.: Verification of GALS systems by combining synchronous languages and process calculi. In: Păsăreanu, C.S. (ed.) SPIN 2009. LNCS, vol. 5578, pp. 241–260. Springer, Heidelberg (2009). https://doi.org/10.1007/978-3-642-02652-2_20
Graf, S., Steffen, B.: Compositional minimization of finite state systems. In: Clarke, E.M., Kurshan, R.P. (eds.) CAV 1990. LNCS, vol. 531, pp. 186–196. Springer, Heidelberg (1991). https://doi.org/10.1007/BFb0023732
Groote, J.F., Ponse, A.: The Syntax and Semantics of \(\mu \)CRL. CS-R 9076. Centrum voor Wiskunde en Informatica, Amsterdam (1990)
ISO/IEC. LOTOS - A Formal Description Technique Based on the Temporal Ordering of Observational Behaviour. International Standard 8807, International Organization for Standardization - Information Processing Systems - Open Systems Interconnection, Geneva, September 1989
ISO/IEC. Enhancements to LOTOS (E-LOTOS). International Standard 15437:2001, International Organization for Standardization - Information Technology, Geneva, September 2001
Kozen, D.: Results on the propositional \(\mu \)-calculus. Theoret. Comput. Sci. 27, 333–354 (1983)
Krimm, J.-P., Mounier, L.: Compositional state space generation from Lotos programs. In: Brinksma, E. (ed.) TACAS 1997. LNCS, vol. 1217, pp. 239–258. Springer, Heidelberg (1997). https://doi.org/10.1007/BFb0035392
Lang, F.: Exp.Open 2.0: a flexible tool integrating partial order, compositional, and on-the-fly verification methods. In: Romijn, J., Smith, G., van de Pol, J. (eds.) IFM 2005. LNCS, vol. 3771, pp. 70–88. Springer, Heidelberg (2005). https://doi.org/10.1007/11589976_6
Lang, F., Mateescu, R.: Partial model checking using networks of labelled transition systems and boolean equation systems. Log. Methods Comput. Sci. 9(4), 1–32 (2013)
Malhotra, J., Smolka, S.A., Giacalone, A., Shapiro, R.: A tool for hierarchical design and simulation of concurrent systems. In: Proceedings of the BCS-FACS Workshop on Specification and Verification of Concurrent Systems, Stirling, Scotland, UK, pp. 140–152. British Computer Society, July 1988
Mateescu, R., Thivolle, D.: A model checking language for concurrent value-passing systems. In: Cuellar, J., Maibaum, T., Sere, K. (eds.) FM 2008. LNCS, vol. 5014, pp. 148–164. Springer, Heidelberg (2008). https://doi.org/10.1007/978-3-540-68237-0_12
Mateescu, R., Wijs, A.: Property-dependent reductions adequate with divergence-sensitive branching bisimilarity. Sci. Comput. Program. 96(3), 354–376 (2014)
Milner, R.: Communication and Concurrency. Prentice-Hall, Upper Saddle River (1989)
De Nicola, R., Vaandrager, F.: Action versus state based logics for transition systems. In: Guessarian, I. (ed.) LITP 1990. LNCS, vol. 469, pp. 407–419. Springer, Heidelberg (1990). https://doi.org/10.1007/3-540-53479-2_17
Park, D.: Concurrency and automata on infinite sequences. In: Deussen, P. (ed.) GI-TCS 1981. LNCS, vol. 104, pp. 167–183. Springer, Heidelberg (1981). https://doi.org/10.1007/BFb0017309
Pnueli, A.: In transition from global to modular temporal reasoning about programs. Log. Models Concurr. Syst. 13, 123–144 (1984)
Sabnani, K.K., Lapone, A.M., Ümit Uyar, M.: An algorithmic procedure for checking safety properties of protocols. IEEE Trans. Commun. 37(9), 940–948 (1989)
Streett, R.: Propositional dynamic logic of looping and converse. Inf. Control 54, 121–141 (1982)
Tai, K.-C., Koppol, P.V.: An incremental approach to reachability analysis of distributed programs. In: Proceedings of the 7th International Workshop on Software Specification and Design, Los Angeles, CA, USA, pp. 141–150, Piscataway, NJ, December 1993. IEEE Press (1993)
Tai, K.-C., Koppol, P.V.: Hierarchy-based incremental reachability analysis of communication protocols. In: Proceedings of the IEEE International Conference on Network Protocols, San Francisco, CA, USA, pp. 318–325. IEEE Press, Piscataway, NJ, October 1993 (1993)
Valmari, A.: Compositional state space generation. In: Rozenberg, G. (ed.) ICATPN 1991. LNCS, vol. 674, pp. 427–457. Springer, Heidelberg (1993). https://doi.org/10.1007/3-540-56689-9_54
van Glabbeek, R.J., Weijland, W.P.: Branching-time and abstraction in bisimulation semantics (extended abstract). CS R8911, Centrum voor Wiskunde en Informatica, Amsterdam 1989. Also in Proceedings IFIP 11th World Computer Congress, San Francisco (1989)
van Glabbeek, R.J., Weijland, W.P.: Branching time and abstraction in bisimulation semantics. J. ACM 43(3), 555–600 (1996)
Yeh, W.J., Young, M.: Compositional reachability analysis using process algebra. In: Proceedings of the ACM SIGSOFT Symposium on Testing, Analysis, and Verification (SIGSOFT 1991), Victoria, British Columbia, Canada, pp. 49–59. ACM Press, October 1991 (1991)
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2019 Springer Nature Switzerland AG
About this paper
Cite this paper
Lang, F., Mateescu, R., Mazzanti, F. (2019). Compositional Verification of Concurrent Systems by Combining Bisimulations. In: ter Beek, M., McIver, A., Oliveira, J. (eds) Formal Methods – The Next 30 Years. FM 2019. Lecture Notes in Computer Science(), vol 11800. Springer, Cham. https://doi.org/10.1007/978-3-030-30942-8_13
Download citation
DOI: https://doi.org/10.1007/978-3-030-30942-8_13
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-030-30941-1
Online ISBN: 978-3-030-30942-8
eBook Packages: Computer ScienceComputer Science (R0)