Automated refinement checking of concurrent systems

ABSTRACT

Stepwise refinement is at the core of many approaches to synthesis and optimization of hardware and software systems. For instance, it can be used to build a synthesis approach for digital circuits from high level specifications. It can also be used for post-synthesis modification such as in Engineering Change Orders (ECOs). Therefore, checking if a system, modeled as a set of concurrent processes, is a refinement of another is of tremendous value. In this paper, we focus on concurrent systems modeled as Communicating Sequential Processes (CSP) and show their refinements can be validated using insights from translation validation, automated theorem proving and relational approaches to reasoning about programs. The novelty of our approach is that it handles infinite state spaces in a fully automated manner. We have implemented our refinement checking technique and have applied it to a variety of refinements. We present the details of our algorithm and experimental results. As an example, we were able to automatically check an infinite state space buffer refinement that cannot be checked by current state of the art tools such as FDR. We were also able to check the data part of an industrial case study on the EP2 system.

REFERENCES

• 1: EP2. www.eftpos2000.ch.
• 2: Failures-divergence refinement: FDR2 user manual. Formal Systems (Europe) Ltd., Oxford, England, June 2005.
• 3: Thomas Ball , Rupak Majumdar , Todd Millstein , Sriram K. Rajamani, Automatic predicate abstraction of C programs, Proceedings of the ACM SIGPLAN 2001 conference on Programming language design and implementation, p.203-213, June 2001, Snowbird, Utah, United States
• 4: Nick Benton, Simple relational correctness proofs for static analyses and program transformations, Proceedings of the 31st ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.14-25, January 14-16, 2004, Venice, Italy
• 5: A. Benveniste, L. Carloni, P. Caspi, and A. Sangiovanni-Vincentelli. Heterogeneous reactive systems modeling and correct-by-construction deployment, 2003.
• 6: J. R. Burch, E. M. Clarke, K. L. McMillan, D. L. Dill, and L. J. Hwang. Symbolic model checking: 10²⁰ states and beyond. In Proceedings of LICS 1990, 1990.
• 7: Doran Bustan , Orna Grumberg, Simulation Based Minimization, Proceedings of the 17th International Conference on Automated Deduction, p.255-270, June 17-20, 2000
• 8: S. Chaki, E. Clarke, J. Ouaknine, N. Sharygina, and N. Sinha. Concurrent software verification with states, events and deadlocks. Formal Aspects of Computing Journal, 17(4):461--483, December 2005.
• 9: Edmund M. Clarke , Orna Grumberg , David E. Long, Verification Tools for Finite-State Concurrent Systems, A Decade of Concurrency, Reflections and Perspectives, REX School/Symposium, p.124-175, June 01-04, 1993
• 10: C. Norris Ip , David L. Dill, Better Verification Through Symmetry, Proceedings of the 11th IFIP WG10.2 International Conference sponsored by IFIP WG10.2 and in cooperation with IEEE COMPSOC on Computer Hardware Description Languages and their Applications, p.97-111, April 26-28, 1993
• 11: David Detlefs , Greg Nelson , James B. Saxe, Simplify: a theorem prover for program checking, Journal of the ACM (JACM), v.52 n.3, p.365-473, May 2005 [doi>10.1145/1066100.1066102]
• 12: Bruno Dutertre , Steve Schneider, Using a PVS Embedding of CSP to Verify Authentication Protocols, Proceedings of the 10th International Conference on Theorem Proving in Higher Order Logics, p.121-136, August 19-22, 1997
• 13: Susanne Graf , Hassen Saïdi, Construction of Abstract State Graphs with PVS, Proceedings of the 9th International Conference on Computer Aided Verification, p.72-83, June 22-25, 1997
• 14: Thomas A. Henzinger , Ranjit Jhala , Rupak Majumdar , Grégoire Sutre, Lazy abstraction, Proceedings of the 29th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.58-70, January 16-18, 2002, Portland, Oregon
• 15: C. A. R. Hoare, Communicating sequential processes, Prentice-Hall, Inc., Upper Saddle River, NJ, 1985
• 16: Yoshinao Isobe and Markus Roggenbach. A generic theorem prover of CSP refinement. In TACAS '05, volume 1503 of Lecture Notes in Computer Science (LNCS), pages 103--123. Springer-Verlag, April 2005.
• 17: Mark B. Josephs. A state-based approach to communicating processes. Distributed Computing, 3(1):9--18, March 1988.
• 18: Kathi Fisler , Moshe Y. Vardi, Bisimulation and Model Checking, Proceedings of the 10th IFIP WG 10.5 Advanced Research Working Conference on Correct Hardware Design and Verification Methods, p.338-341, September 27-29, 1999
• 19: Sudipta Kundu, Sorin Lerner, and Rajesh Gupta. Automated refinement checking of concurrent systems. Technical report, University of California, San Diego, 2007. http://mesl.ucsd.edu/pubs/iccad07-tr.pdf.
• 20: David Lacey , Neil D. Jones , Eric Van Wyk , Carl Christian Frederiksen, Proving correctness of compiler optimizations by temporal logic, Proceedings of the 29th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.283-294, January 16-18, 2002, Portland, Oregon
• 21: Edward A. Lee and Alberto L. Sangiovanni-Vincentelli. A framework for comparing models of computation. IEEE Trans. on CAD of Integrated Circuits and Systems, 17(12):1217--1229, 1998.
• 22: Stan Liao , Steve Tjiang , Rajesh Gupta, An efficient implementation of reactivity for modeling hardware in the scenic design environment, Proceedings of the 34th annual conference on Design automation, p.70-75, June 09-13, 1997, Anaheim, California, United States [doi>10.1145/266021.266037]
• 23: Panagiotis Manolios , Kedar S. Namjoshi , Robert Summers, Linking Theorem Proving and Model-Checking with Well-Founded Bisimulation, Proceedings of the 11th International Conference on Computer Aided Verification, p.369-379, July 06-10, 1999
• 24: Panagiotis Manolios , Sudarshan K. Srinivasan, Automatic Verification of Safety and Liveness for XScale-Like Processor Models Using WEB Refinements, Proceedings of the conference on Design, automation and test in Europe, p.10168, February 16-20, 2004
• 25: K. L. McMillan, A methodology for hardware verification using compositional model checking, Science of Computer Programming, v.37 n.1-3, p.279-309, May 2000 [doi>10.1016/S0167-6423(99)00030-1]
• 26: George C. Necula, Translation validation for an optimizing compiler, Proceedings of the ACM SIGPLAN 2000 conference on Programming language design and implementation, p.83-94, June 18-21, 2000, Vancouver, British Columbia, Canada
• 27: Sam Owre , John M. Rushby , Natarajan Shankar, PVS: A Prototype Verification System, Proceedings of the 11th International Conference on Automated Deduction: Automated Deduction, p.748-752, June 15-18, 1992
• 28: L. C. Paulson. Isabelle: A generic theorem prover, volume 828 of Lecure Notes in Computer Science. Springer Verlag, 1994.
• 29: Doron Peled, Ten Years of Partial Order Reduction, Proceedings of the 10th International Conference on Computer Aided Verification, p.17-28, June 28-July 02, 1998
• 30: Amir Pnueli , Michael Siegel , Eli Singerman, Translation Validation, Proceedings of the 4th International Conference on Tools and Algorithms for Construction and Analysis of Systems, p.151-166, March 28-April 04, 1998
• 31: A. W. Roscoe , Paul H. B. Gardiner , M. H. Goldsmith , J. R. Hulance , D. M. Jackson , J. B. Scattergood, Hierarchical Compression for Model-Checking CSP or How to Check 1020 Dining Philosophers for Deadlock, Proceedings of the First International Workshop on Tools and Algorithms for Construction and Analysis of Systems, p.133-152, May 19-20, 1995
• 32: Ingo Sander and Axel Jantsch. System modeling and transformational design refinement in forsyde {formal system design}. IEEE Trans. on CAD of Integrated Circuits and Systems, 23(1):17--32, 2004.
• 33: Jean-Pierre Talpin , Paul Le Guernic , Sandeep Kumar Shukla , Frédéric Doucet , Rajesh Gupta, Formal Refinement Checking in a System-level Design Methodology, Fundamenta Informaticae, v.62 n.2, p.243-273, April 2004
• 34: Haykal Tej , Burkhart Wolff, A Corrected Failure Divergence Model for CSP in Isabelle/HOL, Proceedings of the 4th International Symposium of Formal Methods Europe on Industrial Applications and Strengthened Foundations of Formal Methods, p.318-337, September 15-19, 1997