Top

International Journal on Software Tools for Technology Transfer

Published in:

07-04-2022 | General

Approximate verification of concurrent systems using token structures and invariants

Authors: Pedro Antonino, Thomas Gibson-Robinson, A. W. Roscoe

Published in: International Journal on Software Tools for Technology Transfer | Issue 4/2022

Activate our intelligent search to find suitable subject content or patents.

search-config

AI-assisted search

Off

Abstract

Distributed systems often rely on token structures to avoid undesired states and behave correctly. While conservative token structures ensure that a fixed number of tokens exist at all times, existential structures guarantee that tokens cannot be completely eliminated. In this paper, we show how a SAT/SMT checker can be used to automatically detect such token structures in concurrent systems and how to derive the natural invariants they preserve. We use these invariants to improve the precision of a deadlock-checking framework that is based on local analysis. Moreover, we conducted some practical experiments to demonstrate that this new framework is as efficient as similar incomplete techniques for deadlock-freedom analysis while handling a different class of systems.

previous article Tools and algorithms for the construction and analysis of systems: a special issue for TACAS 2017

next article From linear temporal logic and limit-deterministic Büchi automata to deterministic parity automata

Dont have a licence yet? Then find out more about our products and how to get one now:

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!

inform now

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!

inform now

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!

inform now

Setting the polarity of SAT variables, so that the solver first decides to assign variables to false, can substantially speed this minimisation process.

We would need to replace \((\bigvee _{\begin{array}{c} i \in \{1 \ldots n\} \\ \wedge {\mathcal {A}}(p_i) \end{array}} t_{i,{\hat{s}}_i})\) by \((\sum _{\begin{array}{c} i \in \{1 \ldots n\} \\ \wedge {\mathcal {A}}(p_i) \end{array}} t_{i,{\hat{s}}_i} > 0)\) in updating \({\mathcal {F}}\) in Minimise.

Agerwala, T., Choed-Amphai, Y.C.: A synthesis rule for concurrent systems. In: Design Automation, 1978. 15th Conference on, pp. 305–311. IEEE (1978)

Andrews, G.R., Schneider, F.B.: Concepts and notations for concurrent programming. ACM Comput. Surv. 15(1), 3–43 (1983)CrossRef

Antonino, P.: Verifying concurrent systems by approximations. DPhil thesis, University of Oxford (2018). https://ora.ox.ac.uk/objects/uuid:f75c782c-a168-49b3-bfed-e2715f027157

Antonino, P., Gibson-Robinson, T., Roscoe, A.: Efficient deadlock-freedom checking using local analysis and SAT solving. In: IFM, no. 9681 in LNCS, pp. 345–360. Springer (2016)

Antonino, P., Gibson-Robinson, T., Roscoe, A.: Tighter reachability criteria for deadlock freedom analysis. In: FM, no. 9995 in LNCS. Springer (2016)

Antonino, P., Gibson-Robinson, T., Roscoe, A.: Experiment package (2018). www.cs.ox.ac.uk/people/pedro.antonino/thepkg.zip

Antonino, P., Gibson-Robinson, T., Roscoe, A.W.: The automatic detection of token structures and invariants using SAT checking. In: TACAS, no. 10206 in LNCS, pp. 249–265. Springer (2017)

Antonino, P., Gibson-Robinson, T., Roscoe, A.W.: Checking static properties using conservative SAT approximations for reachability. LNCS (2017)

Antonino, P., Gibson-Robinson, T., Roscoe, A.W.: Efficient verification of concurrent systems using local-analysis-based approximations and SAT solving. Formal Asp. Comput. 31(3), 375–409 (2019)MathSciNetCrossRef

10.

Antonino, P., Gibson-Robinson, T., Rosco, A..W.: Efficient verification of concurrent systems using synchronisation analysis and SAT/SMT solving. ACM Trans. Softw. Eng. Methodol. 28(3), 18:1-18:43 (2019)CrossRef

11.

Antonino, P., Oliveira, M.M., Sampaio, A., Kristensen, K., Bryans, J.: Leadership election: an industrial SoS application of compositional deadlock verification. NFM, LNCS 8430, 31–45 (2014)

12.

Antonino, P., Sampaio, A., Woodcock, J.: A refinement based strategy for local deadlock analysis of networks of CSP processes. FM, LNCS 8442, 62–77 (2014). https://doi.org/10.1007/978-3-319-06410-9_5MathSciNetCrossRef

13.

Apt, K.R., Francez, N., De Roever, W.P.: A proof system for communicating sequential processes. ACM Trans. Program. Lang. Syst. (TOPLAS) 2(3), 359–385 (1980)CrossRef

14.

Attie, P.C., Bensalem, S., Bozga, M., Jaber, M., Sifakis, J., Zaraket, F.A.: An abstract framework for deadlock prevention in BIP. In: FORTE, no. 7892 in LNCS, pp. 161–177. Springer (2013)

15.

Attie, P.C., Bensalem, S., Bozga, M., Jaber, M., Sifakis, J., Zaraket, F.A.: Global and local deadlock freedom in BIP. ACM Trans. Softw. Eng. Methodol. 26(3), 9:1-9:48 (2018). https://doi.org/10.1145/3152910CrossRef

16.

Attie, P.C., Chockler, H.: Efficiently verifiable conditions for deadlock-freedom of large concurrent programs. In: VMCAI, pp. 465–481. Springer (2005)

17.

Audemard, G., Simon, L.: Predicting Learnt Clauses Quality in Modern SAT Solvers. IJCAI’09, pp. 399–404. San Francisco, CA, USA (2009)

18.

Baier, C., Katoen, J.P.: Principles of Model Checking (Representation and Mind Series). The MIT Press, United States (2008)MATH

19.

Batcher, K.E.: Sorting networks and their applications. In: Proceedings of the April 30–May 2, 1968, Spring Joint Computer Conference, AFIPS ’68 (Spring), pp. 307–314. ACM, New York, NY, USA (1968). 10.1145/1468075.1468121

20.

Bensalem, S., Bozga, M., Legay, A., Nguyen, T., Sifakis, J., Yan, R.: Component-based verification using incremental design and invariants. Softw. Syst. Model. 15(2), 427–451 (2016). https://doi.org/10.1007/s10270-014-0410-8CrossRef

21.

Bensalem, S., Griesmayer, A., Legay, A., Nguyen, T.H., Sifakis, J., Yan, R.: D-finder 2: Towards efficient correctness of incremental design. In: NFM, pp. 453–458 (2011)

22.

Bensalem, S., Lakhnech, Y.: Automatic generation of invariants. Form. Methods Syst. Des. 15(1), 75–92 (1999). https://doi.org/10.1023/A:1008744030390CrossRef

23.

Biere, A., Cimatti, A., Clarke, E., Zhu, Y.: Symbolic model checking without bdds. Tools and Algorithms for the Construction and Analysis of Systems pp. 193–207 (1999)

24.

Brookes, S.D., Roscoe, A.W.: Deadlock analysis in networks of communicating processes. Distrib. Comput. 4, 209–230 (1991)MathSciNetCrossRef

25.

Burch, J.R., Clarke, E.M., McMillan, K.L., Dill, D.L., Hwang, L.J.: Symbolic model checking: 1020 states and beyond. Inform. comput. 98(2), 142–170 (1992)MathSciNetCrossRef

26.

Chaki, S., Clarke, E., Ouaknine, J., Sharygina, N., Sinha, N.: Concurrent software verification with states, events, and deadlocks. Form. Asp. Comput. 17(4), 461–483 (2005)CrossRef

27.

Clarke, E., Grumberg, O., Jha, S., Lu, Y., Veith, H.: Counterexample-guided abstraction refinement. In: Computer aided verification, pp. 154–169. Springer (2000)

28.

Dijkstra, E.W.: The structure of the“the”-multiprogramming system. Commun. ACM 11(5), 341–346 (1968)CrossRef

29.

Eén, N., Sörensson, N.: Translating pseudo-boolean constraints into SAT. JSAT 2(1–4), 1–26 (2006)MATH

30.

Filho, M.S.C., Oliveira, M.V.M., Sampaio, A., Cavalcanti, A.: Local livelock analysis of component-based models. In: ICFEM, pp. 279–295 (2016)

31.

Gibson-Robinson, T., Armstrong, P., Boulgakov, A., Roscoe, A.: FDR3 – A Modern Refinement Checker for CSP. TACAS, LNCS 8413, 187–201 (2014)MATH

32.

Gibson-Robinson, T., Hansen, H., Roscoe, A., Wang, X.: Practical partial order reduction for CSP. NFM, LNCS 9058, 188–203 (2015)

33.

Godefroid, P., Wolper, P.: Using partial orders for the efficient verification of deadlock freedom and safety properties. FMSD 2(2), 149–164 (1993)MATH

34.

Gruner, S., Steyn, T.J.: Deadlock-freeness of hexagonal systolic arrays. Inf. Process. Lett. 110(14–15), 539–543 (2010). https://doi.org/10.1016/j.ipl.2010.04.021MathSciNetCrossRefMATH

35.

Hoare, C.A.R.: Communicating Sequential Processes. Prentice-Hall, United States (1985)MATH

36.

Lambertz, C., Majster-Cederbaum, M.: Analyzing Component-Based Systems on the Basis of Architectural Constraints. In: FSEN, pp. 64–79. Springer (2011)

37.

Lamport, L.: Proving the correctness of multiprocess programs. IEEE Trans. Softw. Eng. 2, 125–143 (1977)MathSciNetCrossRef

38.

Martin, J., Jassim, S.: An efficient technique for deadlock analysis of large scale process networks. In: FME ’97, pp. 418–441 (1997)

39.

Martin, J.M.R.: The design and construction of deadlock-free concurrent systems. Ph.D. thesis, University of Buckingham (1996)

40.

de Moura, L.M., Bjørner, N.: Z3: An efficient smt solver. In: TACAS, pp. 337–340 (2008)

41.

Murata, T.: Petri nets: Properties, analysis and applications. Proceedings of the IEEE 77(4), 541–580 (1989). https://doi.org/10.1109/5.24143

42.

Oliveira, M.V.M., Antonino, P., Ramos, R., Sampaio, A., Mota, A., Roscoe, A.W.: Rigorous development of component-based systems using component metadata and patterns. Form. Asp. Comput. (2016). https://doi.org/10.1007/s00165-016-0375-1MathSciNetCrossRefMATH

43.

Otoni, R., Cavalcanti, A., Sampaio, A.: Local analysis of determinism for CSP. In: Formal Methods: Foundations and Applications - 20th Brazilian Symposium, SBMF 2017, Recife, Brazil, November 29 - December 1, 2017, Proceedings, pp. 107–124 (2017)

44.

Ouaknine, J., Palikareva, H., Roscoe, A.W., Worrell, J.: A static analysis framework for livelock freedom in CSP. LMCS 9(3) (2013)

45.

Palikareva, H., Ouaknine, J., Roscoe, A.: SAT-solving in CSP trace refinement. Sci. Comput. Program. 77(10), 1178–1197 (2012)CrossRef

46.

Peled, D.: All from one, one for all: on model checking using representatives. In: Computer Aided Verification, pp. 409–423. Springer (1993)

47.

Peterson, J.L.: Petri nets. ACM Comput. Surv. 9(3), 223–252 (1977)CrossRef

48.

Plotkin, G.: A structural approach to operational semantics. Tech. rep., DAIMI FN-19, Computer Science Dept, Aarhus University (1981)

49.

Ramos, R.T.: Systematic development of trustworthy component-based systems. Ph.D. thesis, Universidade Federal de Pernambuco (2011)

50.

Roscoe, A.: Understanding Concurrent Systems. Springer, Berlin (2010)CrossRef

51.

Roscoe, A.W.: The theory and practice of concurrency. Prentice Hall, United States (1998)

52.

Roscoe, A.W., Dathi, N.: The pursuit of deadlock freedom. Inf. Comput. 75(3), 289–327 (1987)MathSciNetCrossRef

53.

Roscoe, A.W., Gardiner, P.H.B., Goldsmith, M., Hulance, J.R., Jackson, D.M., Scattergood, J.B.: Hierarchical compression for model-checking CSP or how to check \(10^{{20}}\) dining philosophers for deadlock. In: TACAS, pp. 133–152 (1995)

54.

Valmari, A.: A stubborn attack on state explosion. Form. Methods Syst. Des. 1(4), 297–322 (1992)CrossRef

55.

Yeh, W.J., Young, M.: Compositional reachability analysis using process algebra. In: Proceedings of the symposium on Testing, analysis, and verification, pp. 49–59. ACM (1991)

Title: Approximate verification of concurrent systems using token structures and invariants
Authors: Pedro Antonino
Thomas Gibson-Robinson
A. W. Roscoe
Publication date: 07-04-2022
Publisher: Springer Berlin Heidelberg
Published in: International Journal on Software Tools for Technology Transfer / Issue 4/2022
Print ISSN: 1433-2779
Electronic ISSN: 1433-2787
DOI: https://doi.org/10.1007/s10009-022-00650-6

Springer Professional

Abstract

Please log in to get access to your license.

Dont have a licence yet? Then find out more about our products and how to get one now:

Springer Professional "Wirtschaft+Technik"

Springer Professional "Technik"

Springer Professional "Wirtschaft"

Other articles of this Issue 4/2022

Generating test as a web service (TaaWS) through a method-based attribute grammar

DisCoveR: accurate and efficient discovery of declarative process models

The probabilistic model checker Storm

The Log Skeleton Visualizer in ProM 6.9

Tools and algorithms for the construction and analysis of systems: a special issue for TACAS 2017

Correction to: Reliable benchmarking: requirements and solutions

Premium Partner