2019
Conference article
Open Access
Compositional verification of concurrent systems by combining bisimulations
Lang F., Mateescu R., Mazzanti F.
temporal logic Hardware and Architecture Concurrency theory [INFO.INFO-SE]Computer Science [cs]/Software Engineering [cs.SE] RERS model checking state space reduction CADP labelled transition system Theoretical Computer Science modal mu-calculus Branching bisimulation Software Compositional verification
Compositional verification is a promising technique for analyzing action-based temporal properties of concurrent systems. One approach to verify a property expressed as a modal ?-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 Ldsbr fragment of ?-calculus (consistingofweakmodalitiesonly),individual processes can be minimized modulo divergence-sensitive 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 minimiza- tion on concurrent processes depending whether they contain or not the actions occurring in the strong modalities of the formula. We extend the existing Ldsbr fragment 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.
Source: FM 2019 -International Symposium on Formal Methods. Third World Congress, pp. 196–213, Porto, Portugal, 7-11 October 2019
Publisher: Springer, Berlin, DEU
1. Henrik Reif Andersen. Partial Model Checking. In Proceedings of the 10th Annual IEEE Symposium on Logic in Computer Science LICS (San Diego, California, USA), pages 398{407. IEEE Computer Society Press, June 1995.
2. Stephen D. Brookes, C. A. R. Hoare, and A. W. Roscoe. A Theory of Communicating Sequential Processes. Journal of the ACM, 31(3):560{599, July 1984.
3. David Champelovier, Xavier Clerc, Hubert Garavel, Yves Guerte, Christine McKinty, Vincent Powazny, Frederic Lang, Wendelin Serwe, and Gideon Smeding. Reference Manual of the LNT to LOTOS Translator (Version 6.7). INRIA, Grenoble, France, July 2017.
4. S. C. Cheung and J. Kramer. 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), pages 115{125. ACM Press, December 1993.
5. E. M. Clarke, E. A. Emerson, and A. P. Sistla. Automatic Veri cation of FiniteState Concurrent Systems using Temporal Logic Speci cations. ACM Transactions on Programming Languages and Systems, 8(2):244{263, April 1986.
6. Pepijn Crouzen and Frederic Lang. Smart Reduction. In Dimitra Giannakopoulou and Fernando Orejas, editors, Proceedings of Fundamental Approaches to Software Engineering (FASE'11), Saarbrucken, Germany, volume 6603 of Lecture Notes in Computer Science, pages 111{126. Springer, March 2011.
7. Sander de Putter, Anton Wijs, and Frederic Lang. Compositional Model Checking is Lively | Extended Version, 2018. Submitted to Science of Computer Programming.
8. Alessandro Fantechi, Stefania Gnesi, and Gioia Ristori. From ACTL to -calculus (extended abstract). In Proceedings of the Workshop on Theory and Practice in Veri cation. ERCIM, 1992.
9. Michael J. Fischer and Richard E. Ladner. Propositional Dynamic Logic of Regular Programs. Journal of Computer and System Sciences, 18(2):194{211, September 1979.
10. Hubert Garavel and Frederic Lang. SVL: a Scripting Language for Compositional Veri cation. In Myungchul Kim, Byoungmoon Chin, Sungwon Kang, and Danhyung Lee, editors, Proceedings of the 21st IFIP WG 6.1 International Conference on Formal Techniques for Networked and Distributed Systems (FORTE'01), Cheju Island, Korea, pages 377{392. Kluwer Academic Publishers, August 2001. Full version available as INRIA Research Report RR-4223.
11. Hubert Garavel, Frederic Lang, and Radu Mateescu. Compositional Veri cation of Asynchronous Concurrent Systems Using CADP. Acta Informatica, 52(4):337{392, April 2015.
12. Hubert Garavel, Frederic Lang, Radu Mateescu, and Wendelin Serwe. CADP 2011: A Toolbox for the Construction and Analysis of Distributed Processes. Springer International Journal on Software Tools for Technology Transfer (STTT), 15(2):89{ 107, April 2013.
13. Hubert Garavel and Damien Thivolle. Veri cation of GALS Systems by Combining Synchronous Languages and Process Calculi. In Corina Pasareanu, editor, Proceedings of the 16th International SPIN Workshop on Model Checking of Software (SPIN'09), Grenoble, France, volume 5578 of Lecture Notes in Computer Science, pages 241{260. Springer, June 2009.
14. Susanne Graf and Bernhard Ste en. Compositional Minimization of Finite State Systems. In Edmund M. Clarke and Robert P. Kurshan, editors, Proceedings of the 2nd Workshop on Computer-Aided Veri cation (CAV'90), Rutgers, New Jersey, USA, volume 531 of Lecture Notes in Computer Science, pages 186{196. Springer, June 1990.
15. Jan Friso Groote and Alban Ponse. The Syntax and Semantics of 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. D. Kozen. Results on the Propositional -calculus. Theoretical Computer Science, 27:333{354, 1983.
19. Jean-Pierre Krimm and Laurent Mounier. Compositional State Space Generation from LOTOS Programs. In Ed Brinksma, editor, Proceedings of the 3rd International Workshop on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'97), University of Twente, Enschede, The Netherlands, volume 1217 of Lecture Notes in Computer Science. Springer, April 1997. Extended version with proofs available as Research Report VERIMAG RR97-01.
20. Frederic Lang. EXP.OPEN 2.0: A Flexible Tool Integrating Partial Order, Compositional, and On-the- y Veri cation Methods. In Judi Romijn, Graeme Smith, and Jaco van de Pol, editors, Proceedings of the 5th International Conference on Integrated Formal Methods (IFM'05), Eindhoven, The Netherlands, volume 3771 of Lecture Notes in Computer Science, pages 70{88. Springer, November 2005. Full version available as INRIA Research Report RR-5673.
21. Frederic Lang and Radu Mateescu. Partial Model Checking using Networks of Labelled Transition Systems and Boolean Equation Systems. Logical Methods in Computer Science, 9(4):1{32, October 2013.
22. J. Malhotra, S. A. Smolka, A. Giacalone, and R. Shapiro. A Tool for Hierarchical Design and Simulation of Concurrent Systems. In Proceedings of the BCS-FACS Workshop on Speci cation and Veri cation of Concurrent Systems, Stirling, Scotland, UK, pages 140{152. British Computer Society, July 1988.
23. Radu Mateescu and Damien Thivolle. A Model Checking Language for Concurrent Value-Passing Systems. In Jorge Cuellar, Tom Maibaum, and Kaisa Sere, editors, Proceedings of the 15th International Symposium on Formal Methods (FM'08), Turku, Finland, volume 5014 of Lecture Notes in Computer Science, pages 148{ 164. Springer, May 2008.
24. Radu Mateescu and Anton Wijs. Property-Dependent Reductions Adequate with Divergence-Sensitive Branching Bisimilarity. Science of Computer Programming, 96(3):354{376, 2014.
25. Robin Milner. Communication and Concurrency. Prentice-Hall, 1989.
26. R. De Nicola and F. W. Vaandrager. Action versus State Based Logics for Transition Systems. In Semantics of Concurrency, volume 469 of Lecture Notes in Computer Science, pages 407{419. Springer, 1990.
27. David Park. Concurrency and Automata on In nite Sequences. In Peter Deussen, editor, Theoretical Computer Science, volume 104 of Lecture Notes in Computer Science, pages 167{183. Springer, March 1981.
28. Amir Pnueli. In Transition from Global to Modular Temporal Reasoning about Programs. Logic and Models of Concurrent Systems, 13:123{144, 1984.
29. Krishan K. Sabnani, Aleta M. Lapone, and M. Umit Uyar. An Algorithmic Procedure for Checking Safety Properties of Protocols. IEEE Transactions on Communications, 37(9):940{948, September 1989.
30. R. Streett. Propositional Dynamic Logic of Looping and Converse. Information and Control, (54):121{141, 1982.
31. Kuo-Chung Tai and Pramod V. Koppol. An Incremental Approach to Reachability Analysis of Distributed Programs. In Proceedings of the 7th International Workshop on Software Speci cation and Design, Los Angeles, CA, USA, pages 141{150, Piscataway, NJ, December 1993. IEEE Press.
32. Kuo-Chung Tai and Pramod V. Koppol. Hierarchy-Based Incremental Reachability Analysis of Communication Protocols. In Proceedings of the IEEE International Conference on Network Protocols, San Francisco, CA, USA, pages 318{325, Piscataway, NJ, October 1993. IEEE Press.
33. Antti Valmari. Compositional State Space Generation. In Grzegorz Rozenberg, editor, Advances in Petri Nets 1993 { Papers from the 12th International Conference on Applications and Theory of Petri Nets (ICATPN'91), Gjern, Denmark, volume 674 of Lecture Notes in Computer Science, pages 427{457. Springer, 1993.
34. R. J. van Glabbeek and W. Peter Weijland. Branching-Time and Abstraction in Bisimulation Semantics (extended abstract). CS R8911, Centrum voor Wiskunde en Informatica, Amsterdam, 1989. Also in proc. IFIP 11th World Computer Congress, San Francisco, 1989.
35. Rob J. van Glabbeek and W. Peter Weijland. Branching Time and Abstraction in Bisimulation Semantics. Journal of the ACM, 43(3):555{600, 1996.
36. Wei Jen Yeh and Michal Young. Compositional Reachability Analysis Using Process Algebra. In Proceedings of the ACM SIGSOFT Symposium on Testing, Analysis, and Veri cation (SIGSOFT'91), Victoria, British Columbia, Canada, pages 49{59. ACM Press, October 1991.
2. Stephen D. Brookes, C. A. R. Hoare, and A. W. Roscoe. A Theory of Communicating Sequential Processes. Journal of the ACM, 31(3):560{599, July 1984.
3. David Champelovier, Xavier Clerc, Hubert Garavel, Yves Guerte, Christine McKinty, Vincent Powazny, Frederic Lang, Wendelin Serwe, and Gideon Smeding. Reference Manual of the LNT to LOTOS Translator (Version 6.7). INRIA, Grenoble, France, July 2017.
4. S. C. Cheung and J. Kramer. 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), pages 115{125. ACM Press, December 1993.
5. E. M. Clarke, E. A. Emerson, and A. P. Sistla. Automatic Veri cation of FiniteState Concurrent Systems using Temporal Logic Speci cations. ACM Transactions on Programming Languages and Systems, 8(2):244{263, April 1986.
6. Pepijn Crouzen and Frederic Lang. Smart Reduction. In Dimitra Giannakopoulou and Fernando Orejas, editors, Proceedings of Fundamental Approaches to Software Engineering (FASE'11), Saarbrucken, Germany, volume 6603 of Lecture Notes in Computer Science, pages 111{126. Springer, March 2011.
7. Sander de Putter, Anton Wijs, and Frederic Lang. Compositional Model Checking is Lively | Extended Version, 2018. Submitted to Science of Computer Programming.
8. Alessandro Fantechi, Stefania Gnesi, and Gioia Ristori. From ACTL to -calculus (extended abstract). In Proceedings of the Workshop on Theory and Practice in Veri cation. ERCIM, 1992.
9. Michael J. Fischer and Richard E. Ladner. Propositional Dynamic Logic of Regular Programs. Journal of Computer and System Sciences, 18(2):194{211, September 1979.
10. Hubert Garavel and Frederic Lang. SVL: a Scripting Language for Compositional Veri cation. In Myungchul Kim, Byoungmoon Chin, Sungwon Kang, and Danhyung Lee, editors, Proceedings of the 21st IFIP WG 6.1 International Conference on Formal Techniques for Networked and Distributed Systems (FORTE'01), Cheju Island, Korea, pages 377{392. Kluwer Academic Publishers, August 2001. Full version available as INRIA Research Report RR-4223.
11. Hubert Garavel, Frederic Lang, and Radu Mateescu. Compositional Veri cation of Asynchronous Concurrent Systems Using CADP. Acta Informatica, 52(4):337{392, April 2015.
12. Hubert Garavel, Frederic Lang, Radu Mateescu, and Wendelin Serwe. CADP 2011: A Toolbox for the Construction and Analysis of Distributed Processes. Springer International Journal on Software Tools for Technology Transfer (STTT), 15(2):89{ 107, April 2013.
13. Hubert Garavel and Damien Thivolle. Veri cation of GALS Systems by Combining Synchronous Languages and Process Calculi. In Corina Pasareanu, editor, Proceedings of the 16th International SPIN Workshop on Model Checking of Software (SPIN'09), Grenoble, France, volume 5578 of Lecture Notes in Computer Science, pages 241{260. Springer, June 2009.
14. Susanne Graf and Bernhard Ste en. Compositional Minimization of Finite State Systems. In Edmund M. Clarke and Robert P. Kurshan, editors, Proceedings of the 2nd Workshop on Computer-Aided Veri cation (CAV'90), Rutgers, New Jersey, USA, volume 531 of Lecture Notes in Computer Science, pages 186{196. Springer, June 1990.
15. Jan Friso Groote and Alban Ponse. The Syntax and Semantics of 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. D. Kozen. Results on the Propositional -calculus. Theoretical Computer Science, 27:333{354, 1983.
19. Jean-Pierre Krimm and Laurent Mounier. Compositional State Space Generation from LOTOS Programs. In Ed Brinksma, editor, Proceedings of the 3rd International Workshop on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'97), University of Twente, Enschede, The Netherlands, volume 1217 of Lecture Notes in Computer Science. Springer, April 1997. Extended version with proofs available as Research Report VERIMAG RR97-01.
20. Frederic Lang. EXP.OPEN 2.0: A Flexible Tool Integrating Partial Order, Compositional, and On-the- y Veri cation Methods. In Judi Romijn, Graeme Smith, and Jaco van de Pol, editors, Proceedings of the 5th International Conference on Integrated Formal Methods (IFM'05), Eindhoven, The Netherlands, volume 3771 of Lecture Notes in Computer Science, pages 70{88. Springer, November 2005. Full version available as INRIA Research Report RR-5673.
21. Frederic Lang and Radu Mateescu. Partial Model Checking using Networks of Labelled Transition Systems and Boolean Equation Systems. Logical Methods in Computer Science, 9(4):1{32, October 2013.
22. J. Malhotra, S. A. Smolka, A. Giacalone, and R. Shapiro. A Tool for Hierarchical Design and Simulation of Concurrent Systems. In Proceedings of the BCS-FACS Workshop on Speci cation and Veri cation of Concurrent Systems, Stirling, Scotland, UK, pages 140{152. British Computer Society, July 1988.
23. Radu Mateescu and Damien Thivolle. A Model Checking Language for Concurrent Value-Passing Systems. In Jorge Cuellar, Tom Maibaum, and Kaisa Sere, editors, Proceedings of the 15th International Symposium on Formal Methods (FM'08), Turku, Finland, volume 5014 of Lecture Notes in Computer Science, pages 148{ 164. Springer, May 2008.
24. Radu Mateescu and Anton Wijs. Property-Dependent Reductions Adequate with Divergence-Sensitive Branching Bisimilarity. Science of Computer Programming, 96(3):354{376, 2014.
25. Robin Milner. Communication and Concurrency. Prentice-Hall, 1989.
26. R. De Nicola and F. W. Vaandrager. Action versus State Based Logics for Transition Systems. In Semantics of Concurrency, volume 469 of Lecture Notes in Computer Science, pages 407{419. Springer, 1990.
27. David Park. Concurrency and Automata on In nite Sequences. In Peter Deussen, editor, Theoretical Computer Science, volume 104 of Lecture Notes in Computer Science, pages 167{183. Springer, March 1981.
28. Amir Pnueli. In Transition from Global to Modular Temporal Reasoning about Programs. Logic and Models of Concurrent Systems, 13:123{144, 1984.
29. Krishan K. Sabnani, Aleta M. Lapone, and M. Umit Uyar. An Algorithmic Procedure for Checking Safety Properties of Protocols. IEEE Transactions on Communications, 37(9):940{948, September 1989.
30. R. Streett. Propositional Dynamic Logic of Looping and Converse. Information and Control, (54):121{141, 1982.
31. Kuo-Chung Tai and Pramod V. Koppol. An Incremental Approach to Reachability Analysis of Distributed Programs. In Proceedings of the 7th International Workshop on Software Speci cation and Design, Los Angeles, CA, USA, pages 141{150, Piscataway, NJ, December 1993. IEEE Press.
32. Kuo-Chung Tai and Pramod V. Koppol. Hierarchy-Based Incremental Reachability Analysis of Communication Protocols. In Proceedings of the IEEE International Conference on Network Protocols, San Francisco, CA, USA, pages 318{325, Piscataway, NJ, October 1993. IEEE Press.
33. Antti Valmari. Compositional State Space Generation. In Grzegorz Rozenberg, editor, Advances in Petri Nets 1993 { Papers from the 12th International Conference on Applications and Theory of Petri Nets (ICATPN'91), Gjern, Denmark, volume 674 of Lecture Notes in Computer Science, pages 427{457. Springer, 1993.
34. R. J. van Glabbeek and W. Peter Weijland. Branching-Time and Abstraction in Bisimulation Semantics (extended abstract). CS R8911, Centrum voor Wiskunde en Informatica, Amsterdam, 1989. Also in proc. IFIP 11th World Computer Congress, San Francisco, 1989.
35. Rob J. van Glabbeek and W. Peter Weijland. Branching Time and Abstraction in Bisimulation Semantics. Journal of the ACM, 43(3):555{600, 1996.
36. Wei Jen Yeh and Michal Young. Compositional Reachability Analysis Using Process Algebra. In Proceedings of the ACM SIGSOFT Symposium on Testing, Analysis, and Veri cation (SIGSOFT'91), Victoria, British Columbia, Canada, pages 49{59. ACM Press, October 1991.
Metrics
Back to previous page
BibTeX entry
@inproceedings{oai:it.cnr:prodotti:408348,
title = {Compositional verification of concurrent systems by combining bisimulations},
author = {Lang F. and Mateescu R. and Mazzanti F.},
publisher = {Springer, Berlin, DEU},
doi = {10.1007/978-3-030-30942-8_13 and 10.1007/s10703-021-00360-w},
booktitle = {FM 2019 -International Symposium on Formal Methods. Third World Congress, pp. 196–213, Porto, Portugal, 7-11 October 2019},
year = {2019}
}CNR authorsLaboratories
0000-0003-4562-8777
