nach oben

Erschienen in:

2019 | OriginalPaper | Buchkapitel

Compositional Verification of Concurrent Systems by Combining Bisimulations

verfasst von : Frédéric Lang, Radu Mateescu, Franco Mazzanti

Erschienen in: Formal Methods – The Next 30 Years

Verlag: Springer International Publishing

Einloggen

Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.

search-config

KI-gestützte Suche

Aus

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.

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

über 102.000 Bücher
über 537 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Finance + Banking
Management + Führung
Marketing + Vertrieb
Maschinenbau + Werkstoffe
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 390 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Maschinenbau + Werkstoffe

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 340 Zeitschriften

aus folgenden Fachgebieten:

Bauwesen + Immobilien
Business IT + Informatik
Finance + Banking
Management + Führung
Marketing + Vertrieb
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Vorheriges Kapitel Verifying Correctness of Persistent Concurrent Data Structures

Nächstes Kapitel Towards a Model-Checker for Circus

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\}\).

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.

\(\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.

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.

Otherwise, our approach coincides with the mono-bisimulation approach of [24]. In all the examples addressed in this section, there is always a unique minimal set \(A_s\), whose identification is made easy using Lemma 1.

Specification available at ftp://ftp.inrialpes.fr/pub/vasy/demos/demo_05.

http://rers-challenge.org.

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)MathSciNetCrossRef

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)CrossRef

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_9CrossRef

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)MathSciNetCrossRef

10.

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_24CrossRef

11.

Garavel, H., Lang, F., Mateescu, R.: Compositional verification of asynchronous concurrent systems using CADP. Acta Informatica 52(4), 337–392 (2015)MathSciNetCrossRef

12.

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)CrossRef

13.

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_20CrossRef

14.

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/BFb0023732CrossRef

15.

Groote, J.F., Ponse, A.: The Syntax and Semantics of \(\mu \)CRL. CS-R 9076. Centrum voor Wiskunde en Informatica, Amsterdam (1990)

16.

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

17.

ISO/IEC. Enhancements to LOTOS (E-LOTOS). International Standard 15437:2001, International Organization for Standardization - Information Technology, Geneva, September 2001

18.

Kozen, D.: Results on the propositional \(\mu \)-calculus. Theoret. Comput. Sci. 27, 333–354 (1983)MathSciNetCrossRef

19.

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/BFb0035392CrossRef

20.

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_6CrossRef

21.

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)MathSciNetMATH

22.

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

23.

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_12CrossRef

24.

Mateescu, R., Wijs, A.: Property-dependent reductions adequate with divergence-sensitive branching bisimilarity. Sci. Comput. Program. 96(3), 354–376 (2014)CrossRef

25.

Milner, R.: Communication and Concurrency. Prentice-Hall, Upper Saddle River (1989)MATH

26.

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_17CrossRef

27.

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/BFb0017309CrossRef

28.

Pnueli, A.: In transition from global to modular temporal reasoning about programs. Log. Models Concurr. Syst. 13, 123–144 (1984)MathSciNet

29.

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)CrossRef

30.

Streett, R.: Propositional dynamic logic of looping and converse. Inf. Control 54, 121–141 (1982)MathSciNetCrossRef

31.

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)

32.

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)

33.

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_54CrossRef

34.

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)

35.

van Glabbeek, R.J., Weijland, W.P.: Branching time and abstraction in bisimulation semantics. J. ACM 43(3), 555–600 (1996)MathSciNetCrossRef

36.

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)

Titel: Compositional Verification of Concurrent Systems by Combining Bisimulations
verfasst von: Frédéric Lang
Radu Mateescu
Franco Mazzanti
Verlag: Springer International Publishing
Buch: Formal Methods – The Next 30 Years
Print ISBN: 978-3-030-30941-1

Electronic ISBN: 978-3-030-30942-8

Copyright-Jahr: 2019
DOI: https://doi.org/10.1007/978-3-030-30942-8_13

Springer Professional

Abstract

Bitte loggen Sie sich ein, um Zugang zu Ihrer Lizenz zu erhalten.

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Springer Professional "Technik"

Springer Professional "Wirtschaft"

Premium Partner