research-article

Efficient Verification of Concurrent Systems Using Synchronisation Analysis and SAT/SMT Solving

Authors:
Pedro Antonino

Department of Computer Science, University of Oxford, Oxford, Oxfordshire, UK

Department of Computer Science, University of Oxford, Oxford, Oxfordshire, UK
View Profile

,
Thomas Gibson-Robinson

Department of Computer Science, University of Oxford, Oxford, Oxfordshire, UK

Department of Computer Science, University of Oxford, Oxford, Oxfordshire, UK
View Profile

,
A. W. Roscoe

Department of Computer Science, University of Oxford, Oxford, Oxfordshire, UK

Department of Computer Science, University of Oxford, Oxford, Oxfordshire, UK
View Profile

ACM Transactions on Software Engineering and Methodology Volume 28 Issue 3Article No.: 18pp 1–43https://doi.org/10.1145/3335149

Published:18 July 2019Publication History

ACM Transactions on Software Engineering and Methodology

Abstract

This article investigates how the use of approximations can make the formal verification of concurrent systems scalable. We propose the idea of synchronisation analysis to automatically capture global invariants and approximate reachability. We calculate invariants on how components participate on global system synchronisations and use a notion of consistency between these invariants to establish whether components can effectively communicate to reach some system state. Our synchronisation-analysis techniques try to show either that a system state is unreachable by demonstrating that components cannot agree on the order they participate in system rules or that a system state is unreachable by demonstrating components cannot agree on the number of times they participate on system rules. These fully automatic techniques are applied to check deadlock and local-deadlock freedom in the PairStatic framework. It extends Pair (a recent framework where we use pure pairwise analysis of components and SAT checkers to check deadlock and local-deadlock freedom) with techniques to carry out synchronisation analysis. So, not only can it compute the same local invariants that Pair does, it can leverage global invariants found by synchronisation analysis, thereby improving the reachability approximation and tightening our verifications. We implement PairStatic in our DeadlOx tool using SAT/SMT and demonstrate the improvements they create in checking (local) deadlock freedom.

References

Pedro Antonino. 2018. Verifying Concurrent Systems by Approximations. Ph.D. Thesis. University of Oxford, Oxford, UK. Retrieved from: https://ora.ox.ac.uk/objects/uuid:f75c782c-a168-49b3-bfed-e2715f027157.Google Scholar
Pedro Antonino, Thomas Gibson-Robinson, and A. W. Roscoe. 2016. Efficient deadlock-freedom checking using local analysis and SAT solving. In Proceedings of the IFM (LNCS). Springer, 345--360. Google ScholarDigital Library
Pedro Antonino, Thomas Gibson-Robinson, and A. W. Roscoe. 2016. Tighter reachability criteria for deadlock freedom analysis. In Proceedings of the FM (LNCS). Springer.Google Scholar
Pedro Antonino, Thomas Gibson-Robinson, and A. W. Roscoe. 2018. Experiment package. Retrieved from: www.cs.ox.ac.uk/people/pedro.antonino/tosempkg.zip.Google Scholar
Pedro Antonino, Thomas Gibson-Robinson, and A. W. Roscoe. 2017. Checking static properties using conservative SAT approximations for reachability. In Proceedings of the SBMF. 233--250.Google Scholar
Pedro Antonino, Thomas Gibson-Robinson, and A. W. Roscoe. 2019. Efficient verification of concurrent systems using local-analysis-based approximations and SAT solving. Form. Asp. Comput. 31, 3 (June 2019), 375--409. Google ScholarCross Ref
Pedro Antonino, Marcel Medeiros Oliveira, Augusto Sampaio, Klaus Kristensen, and Jeremy Bryans. 2014. Leadership election: An industrial SoS application of compositional deadlock verification. In Proceedings of the NFM (LNCS), Vol. 8430. 31--45. Google ScholarDigital Library
Pedro Antonino, Augusto Sampaio, and Jim Woodcock. 2014. A refinement based strategy for local deadlock analysis of networks of CSP processes. In Proceedings of the FM (LNCS), Vol. 8442. 62--77. Retrieved from: Google ScholarDigital Library
Krzysztof R. Apt, Nissim Francez, and Willem P. De Roever. 1980. A proof system for communicating sequential processes. ACM Trans. Prog. Lang. Syst. 2, 3 (1980), 359--385. Google ScholarDigital Library
Paul C. Attie, Saddek Bensalem, Marius Bozga, Mohamad Jaber, Joseph Sifakis, and Fadi A. Zaraket. 2013. An abstract framework for deadlock prevention in BIP. In Proceedings of the FORTE (LNCS). Vol. 7892. Springer, 161--177.Google Scholar
Paul C. Attie, Saddek Bensalem, Marius Bozga, Mohamad Jaber, Joseph Sifakis, and Fadi A. Zaraket. 2018. Global and local deadlock freedom in BIP. ACM Trans. Softw. Eng. Methodol. 26, 3 (2018), 9:1--9:48. Google ScholarDigital Library
Paul C. Attie and Hana Chockler. 2005. Efficiently verifiable conditions for deadlock-freedom of large concurrent programs. In Proceedings of the VMCAI. Springer, 465--481. Google ScholarDigital Library
Gilles Audemard and Laurent Simon. 2009. Predicting learnt clauses quality in modern SAT solvers. In Proceedings of the IJCAI. 399--404. Google ScholarDigital Library
Christel Baier and Joost-Pieter Katoen. 2008. Principles of Model Checking (Representation and Mind Series). The MIT Press, Cambridge, MA. Google ScholarDigital Library
A. Basu, B. Bensalem, M. Bozga, J. Combaz, M. Jaber, T. H. Nguyen, and J. Sifakis. 2011. Rigorous component-based system design using the BIP framework. IEEE Software 28, 3 (2011), 41--48. Google ScholarDigital Library
Ananda Basu, Marius Bozga, and Joseph Sifakis. 2006. Modeling heterogeneous real-time components in BIP. In Proceedings of the SEFM. IEEE Computer Society, 3--12. Google ScholarDigital Library
Richard Bellman. 1958. On a routing problem. Quart. Appl. Math. 16, 1 (1958), 87--90.Google ScholarCross Ref
Saddek Bensalem, Marius Bozga, Axel Legay, Thanh-Hung Nguyen, Joseph Sifakis, and Rongjie Yan. 2016. Component-based verification using incremental design and invariants. Softw. Syst. Model. 15, 2 (2016), 427--451. Google ScholarDigital Library
Saddek Bensalem, Andreas Griesmayer, Axel Legay, Thanh-Hung Nguyen, Joseph Sifakis, and Rongjie Yan. 2011. D-Finder 2: Towards efficient correctness of incremental design. In Proceedings of the NFM. 453--458. Google ScholarDigital Library
Saddek Bensalem and Yassine Lakhnech. 1999. Automatic generation of invariants. Form. Methods Syst. Des. 15, 1 (July 1999), 75--92. Google ScholarDigital Library
Dirk Beyer and M. Erkan Keremoglu. 2011. CPAchecker: A tool for configurable software verification. In Proceedings of the CAV, Ganesh Gopalakrishnan and Shaz Qadeer (Eds.). Springer, Berlin, 184--190. Google ScholarDigital Library
Armin Biere, Alessandro Cimatti, Edmund Clarke, and Yunshan Zhu. 1999. Symbolic model checking without BDDs. Tools and Algorithms for the Construction and Analysis of Systems (1999), 193--207. Google ScholarDigital Library
Bruno Blanchet, Patrick Cousot, Radhia Cousot, Jérome Feret, Laurent Mauborgne, Antoine Miné, David Monniaux, and Xavier Rival. 2003. A static analyzer for large safety-critical software. In Proceedings of the PLDI. ACM, 196--207. Google ScholarDigital Library
Luboš Brim, Ivana Černá, Pavlína Vařeková, and Barbora Zimmerova. 2005. Component-interaction automata as a verification-oriented component-based system specification. ACM SIGSOFT Softw. Eng. Notes, Vol. 31. ACM, 4. Google ScholarDigital Library
Stephen D. Brookes and A. W. Roscoe. 1991. Deadlock analysis in networks of communicating processes. Distrib. Comput. 4 (1991), 209--230. Google ScholarDigital Library
Jerry R. Burch, Edmund M. Clarke, Kenneth L. McMillan, David L. Dill, and Lain-Jinn Hwang. 1992. Symbolic model checking: 1020 states and beyond. Inform. Comput. 98, 2 (1992), 142--170. Google ScholarDigital Library
Gerardo Canfora and Massimiliano Di Penta. 2006. Service-oriented architectures testing: A survey. Softw. Eng. Springer, 78--105.Google Scholar
Ana Cavalcanti. 2017. Formal methods for robotics: RoboChart, RoboSim, and more. In Formal Methods: Foundations and Applications, Simone Cavalheiro and José Fiadeiro (Eds.). Springer International Publishing, Cham, 3--6.Google Scholar
Sagar Chaki, Edmund Clarke, Joël Ouaknine, Natasha Sharygina, and Nishant Sinha. 2005. Concurrent software verification with states, events, and deadlocks. Form. Asp. Comput. 17, 4 (2005), 461--483.Google ScholarCross Ref
Shing Chi Cheung and J. Kramer. 1994. Tractable dataflow analysis for distributed systems. IEEE Trans. Softw. Eng. 20, 8 (Aug. 1994), 579--593. Google ScholarDigital Library
Edmund Clarke, Orna Grumberg, Somesh Jha, Yuan Lu, and Helmut Veith. 2000. Counterexample-guided abstraction refinement. In Proceedings of the CAV. Springer, 154--169. Google ScholarDigital Library
Edmund M. Clarke, Orna Grumberg, and Doron Peled. 1999. Model Checking. The MIT Press, Cambridge, MA. Google ScholarDigital Library
Edmund M. Clarke and Jeannette M. Wing. 1996. Formal methods: State of the art and future directions. ACM Comput. Surv. 28, 4 (1996), 626--643. Google ScholarDigital Library
J. W. Coleman, A. K. Malmos, P. G. Larsen, J. Peleska, R. Hains, Z. Andrews, R. Payne, S. Foster, A. Miyazawa, C. Bertolini, and A. Didierk. 2012. COMPASS tool vision for a system of systems collaborative development environment. In Proceedings of the SoSE. 451--456.Google Scholar
Thomas H. Cormen, Charles E. Leiserson, Ronald L. Rivest, and Clifford Stein. 2009. Introduction to Algorithms, Third Edition. The MIT Press, Cambridge, MA. Google ScholarDigital Library
Patrick Cousot and Radhia Cousot. 1977. Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints. In Proceedings of the POPL. 238--252. Google ScholarDigital Library
Patrick Cousot and Radhia Cousot. 1979. Systematic design of program analysis frameworks. In Proceedings of the POPL. 269--282. Google ScholarDigital Library
G. Csertan, G. Huszerl, I. Majzik, Z. Pap, A. Pataricza, and D. Varro. 2002. VIATRA - visual automated transformations for formal verification and validation of UML models. In Proceedings of the ASE. 267--270. Google ScholarDigital Library
Naiem Dathi. 1989. Deadlock and Deadlock Freedom. Ph.D. Thesis. University of Oxford, Oxford, UK. Google ScholarDigital Library
Luca De Alfaro and Thomas A. Henzinger. 2001. Interface automata. ACM SIGSOFT Softw. Eng. Notes, Vol. 26. ACM, 109--120. Google ScholarDigital Library
Luca de Alfaro and Thomas A. Henzinger. 2001. Interface theories for component-based design. In Embedded Software (LNCS), Thomas A. Henzinger and Christoph M. Kirsch (Eds.). Springer, Berlin, 148--165. Google ScholarDigital Library
Leonardo Mendonça de Moura and Nikolaj Bjørner. 2008. Z3: An efficient SMT solver. In Proceedings of the TACAS. 337--340. Google ScholarDigital Library
Vijay D’silva, Daniel Kroening, and Georg Weissenbacher. 2008. A survey of automated techniques for formal software verification. IEEE Trans. Comput.-Aided Design Integ. Circ. Syst. 27, 7 (2008), 1165--1178. Google ScholarDigital Library
Matthew B. Dwyer, Lori A. Clarke, Jamieson M. Cobleigh, and Gleb Naumovich. 2004. Flow analysis for verifying properties of concurrent software systems. ACM Trans. Softw. Eng. Methodol. 13, 4 (Oct. 2004), 359--430. Google ScholarDigital Library
Madiel S. Conserva Filho, Marcel Vinicius Medeiros Oliveira, Augusto Sampaio, and Ana Cavalcanti. 2016. Local livelock analysis of component-based models. In Proceedings of the ICFEM. 279--295.Google Scholar
John Fitzgerald, Jeremy Bryans, and Richard Payne. 2012. A formal model-based approach to engineering systems-of-systems. In Collaborative Networks in the Internet of Services, Luis M. Camarinha-Matos, Lai Xu, and Hamideh Afsarmanesh (Eds.). Springer, Berlin, 53--62.Google Scholar
D. R. Ford and D. R. Fulkerson. 2010. Flows in Networks. Princeton University Press, Princeton, NJ. Google ScholarDigital Library
Robert France and Bernhard Rumpe. 2007. Model-driven development of complex software: A research roadmap. In Proceedings of the FOSE. 37--54. Google ScholarDigital Library
Thomas Gibson-Robinson, Philip Armstrong, Alexandre Boulgakov, and A. W. Roscoe. 2014. FDR3—a modern refinement checker for CSP. In Proceedings of the TACAS (LNCS), Vol. 8413. 187--201.Google Scholar
Thomas Gibson-Robinson, Henri Hansen, A. W. Roscoe, and Xu Wang. 2015. Practical partial order reduction for CSP. In Proceedings of the NFM (LNCS), Vol. 9058. Springer, 188--203.Google ScholarCross Ref
Patrice Godefroid and Pierre Wolper. 1993. Using partial orders for the efficient verification of deadlock freedom and safety properties. In FMSD 2, 2 (1993), 149--164. Google ScholarDigital Library
Stefan Gruner and T. J. Steyn. 2010. Deadlock-freeness of hexagonal systolic arrays. Inf. Process. Lett. 110, 14--15 (2010), 539--543. Google ScholarDigital Library
C. A. R. Hoare. 1985. Communicating Sequential Processes. Prentice Hall, Upper Saddle River, NJ. Google ScholarDigital Library
Daniel Kroening and Ofer Strichman. 2008. Decision Procedures: An Algorithmic Point of View (1st ed.). Springer Publishing Company, Incorporated, New York, NY. Google Scholar
Christian Lambertz and Mila Majster-Cederbaum. 2011. Analyzing component-based systems on the basis of architectural constraints. In Proceedings of the FSEN. Springer, 64--79. Google ScholarDigital Library
Leslie Lamport. 1977. Proving the correctness of multiprocess programs. IEEE Trans. Softw. Eng., 2 (1977), 125--143. Google ScholarDigital Library
Diego Latella, Istvan Majzik, and Mieke Massink. 1999. Automatic verification of a behavioural subset of UML statechart diagrams using the SPIN model-checker. Form. Asp. Comput. 11, 6 (Dec. 1999), 637--664.Google ScholarCross Ref
J. Lilius and I. P. Paltor. 1999. vUML: A tool for verifying UML models. In Proceedings of the ASE. 255--258. Google ScholarDigital Library
Lucas Lima, Alvaro Miyazawa, Ana Cavalcanti, Márcio Cornélio, Juliano Iyoda, Augusto Sampaio, Ralph Hains, Adrian Larkham, and Vaughan Lewis. 2017. An integrated semantics for reasoning about SysML design models using refinement. Softw. Syst. Model. 16, 3 (2017), 875--902. Google ScholarDigital Library
Nancy A. Lynch and Mark R. Tuttle. 1988. An introduction to input/output automata. (1988).Google Scholar
J. M. R. Martin and S. A. Jassim. 1997. An efficient technique for deadlock analysis of large scale process networks. In Proceedings of the FME. 418--441. Google ScholarDigital Library
Jeremy M. R. Martin. 1996. The Design and Construction of Deadlock-Free Concurrent Systems. Ph.D. Dissertation. University of Buckingham, Buckingham, UK.Google Scholar
Robin Milner. 1989. Communication and Concurrency. Prentice Hall, Upper Saddle River, NJ. Google ScholarDigital Library
A. Miyazawa, P. Ribeiro, W. Li, A. Cavalcanti, and J. Timmis. 2017. Automatic property checking of robotic applications. In Proceedings of the IROS. 3869--3876.Google Scholar
T. Murata. 1989. Petri nets: Properties, analysis and applications. Proc. IEEE 77, 4 (Apr. 1989), 541--580.Google ScholarCross Ref
Flemming Nielson, Hanne R. Nielson, and Chris Hankin. 1999. Principles of Program Analysis. Springer-Verlag, New York, Inc. Google ScholarDigital Library
M. V. M. Oliveira, P. Antonino, R. Ramos, A. Sampaio, A. Mota, and A. W. Roscoe. 2016. Rigorous development of component-based systems using component metadata and patterns. Formal Aspects of Computing 28, 6 (2016), 937--1004. Google ScholarCross Ref
Rodrigo Otoni, Ana Cavalcanti, and Augusto Sampaio. 2017. Local analysis of determinism for CSP. In Proceedings of the SBMF. 107--124.Google ScholarCross Ref
Joël Ouaknine, Hristina Palikareva, A. W. Roscoe, and James Worrell. 2013. A static analysis framework for livelock freedom in CSP. Logic. Meth. Comput. Sci. 9, 3 (2013).Google Scholar
Robert Paige and Robert E. Tarjan. 1987. Three partition refinement algorithms. SIAM J. Comput. 16, 6 (1987), 973--989. Google ScholarDigital Library
Hristina Palikareva, Joël Ouaknine, and A. W. Roscoe. 2012. SAT-solving in CSP trace refinement. Sci. Comput. Prog. 77, 10 (2012), 1178--1197. Google ScholarDigital Library
Doron Peled. 1993. All from one, one for all: On model checking using representatives. In Proceedings of the CAV. Springer, 409--423. Google ScholarDigital Library
G. D. Plotkin. 1981. A Structural Approach to Operational Semantics. Technical Report. DAIMI FN-19, Computer Science Dept., Aarhus University, Aarhus, Denmark.Google Scholar
Rodrigo Teixeira Ramos. 2011. Systematic Development of Trustworthy Component-based Systems. Ph.D. Dissertation. Universidade Federal de Pernambuco, Recife, Brazil.Google Scholar
John H. Reif and Scott A. Smolka. 1990. Data flow analysis of distributed communicating processes. Int. J. Parallel Prog. 19, 1 (Feb. 1990), 1--30. Google ScholarDigital Library
A. W. Roscoe. 2010. Understanding Concurrent Systems. Springer. Google ScholarDigital Library
A. W. Roscoe. 1987. Routing messages through networks: An exercise in deadlock avoidance. In Programming of Transputer Based Machines: Proceedings of 7th occam User Group Technical Meeting, Muntean et al. (Eds.). IOS B.V., Amsterdam. Retrieved from: http://www.cs.ox.ac.uk/people/bill.roscoe/publications/21.ps.Google Scholar
A. W. Roscoe. 1998. The Theory and Practice of Concurrency. Prentice Hall, Upper Saddle River, NJ. Google ScholarDigital Library
A. W. Roscoe and Naiem Dathi. 1987. The pursuit of deadlock freedom. Inf. Comput. 75, 3 (1987), 289--327. Google ScholarDigital Library
A. W. Roscoe, Paul H. B. Gardiner, Michael Goldsmith, J. R. Hulance, D. M. Jackson, and J. B. Scattergood. 1995. Hierarchical compression for model-checking CSP or how to check 10<sup>20</sup> dining philosophers for deadlock. In Proceedings of the TACAS. 133--152. Google ScholarDigital Library
C. S. Scholten and Edsger W. Dijkstra. 1982. A Class of Simple Communication Patterns. Springer New York, New York, NY, 334--337.Google Scholar
B. Selic. 2003. The pragmatics of model-driven development. IEEE Software 20, 5 (2003), 19--25. Google ScholarDigital Library
Alfred Tarski. 1955. A lattice-theoretical fixpoint theorem and its applications. Pacific J. Math. 5, 2 (1955), 285--309.Google ScholarCross Ref
Antti Valmari. 1992. A stubborn attack on state explosion. Form. Meth. Syst. Des. 1, 4 (1992), 297--322. Google ScholarDigital Library
Jim Woodcock, Peter Gorm Larsen, Juan Bicarregui, and John S. Fitzgerald. 2009. Formal methods: Practice and experience. ACM Comput. Surv. 41, 4 (2009). Google ScholarDigital Library
Wei Jen Yeh and Michal Young. 1991. Compositional reachability analysis using process algebra. In Proceedings of the TAV. ACM, 49--59. Google ScholarDigital Library

Index Terms

Efficient Verification of Concurrent Systems Using Synchronisation Analysis and SAT/SMT Solving
1. Software and its engineering
  1. Software organization and properties
    1. Software functional properties
      1. Formal methods
        Automated static analysis
        Model checking
2. Theory of computation
  1. Models of computation
    1. Concurrency
  2. Semantics and reasoning
    1. Program reasoning
      1. Invariants

Recommendations

Efficient verification of concurrent systems using local-analysis-based approximations and SAT solving
Abstract
This work develops a type of local analysis that can prove concurrent systems deadlock free. As opposed to examining the overall behaviour of a system, local analysis consists of examining the behaviour of small parts of the system to yield a ...
Read More
Approximate verification of concurrent systems using token structures and invariants
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 ...
Read More
Efficient Verification of Sequential and Concurrent C Programs

There has been considerable progress in the domain of software verification over the last few years. This advancement has been driven, to a large extent, by the emergence of powerful yet automated abstraction techniques such as predicate abstraction. ...
Read More

Comments

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Article

Published in
ACM Transactions on Software Engineering and Methodology Volume 28, Issue 3
July 2019
278 pages
ISSN:1049-331X
EISSN:1557-7392
DOI:10.1145/3343019
Editor:
Mauro Pezzè
Università della Svizzera italiana and Università di Milano-Bicocca, Switzerland
Issue’s Table of Contents
Copyright © 2019 ACM
Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]
Sponsors
In-Cooperation
Publisher
Association for Computing Machinery
New York, NY, United States
Publication History
- Published: 18 July 2019
- Accepted: 1 May 2019
- Revised: 1 January 2019
- Received: 1 August 2018
Published in tosem Volume 28, Issue 3

Permissions
Request permissions about this article.
Request Permissions

Check for updates
Author Tags
SAT solving
SMT solving
Synchronisation analysis
approximate verification
concurrent systems
deadlock freedom
invariants
local-deadlock freedom
reachability approximation
Qualifiers
- research-article
- Research
- Refereed
Conference
Funding Sources
Other Metrics
View Article Metrics

Article Metrics
- 6
  Total Citations
  View Citations
- 258
  Total Downloads
- Downloads (Last 12 months)15
- Downloads (Last 6 weeks)0
Other Metrics
View Author Metrics
Cited By
View all

PDF Format

View or Download as a PDF file.

PDF

eReader

View online with eReader.

eReader

HTML Format

View this article in HTML Format .

View HTML Format

Efficient Verification of Concurrent Systems Using Synchronisation Analysis and SAT/SMT Solving

ACM Transactions on Software Engineering and Methodology

Abstract

References

Cited By

Index Terms

Recommendations

Efficient verification of concurrent systems using local-analysis-based approximations and SAT solving

Approximate verification of concurrent systems using token structures and invariants

Efficient Verification of Sequential and Concurrent C Programs