×

On process equivalence = equation solving in CCS. (English) Zbl 1191.68443

Summary: Unique Fixpoint Induction (UFI) is the chief inference rule to prove the equivalence of recursive processes in the Calculus of Communicating Systems (CCS). It plays a major role in the equational approach to verification. Equational verification is of special interest as it offers theoretical advantages in the analysis of systems that communicate values, have infinite state space or show parameterised behaviour. We call these kinds of systems VIPSs. VIPSs is the acronym of Value-passing, Infinite-State and Parameterised Systems. Automating the application of UFI in the context of VIPSs has been neglected. This is both because many VIPSs are given in terms of recursive function symbols, making it necessary to carefully apply induction rules other than UFI, and because proving that one VIPS process constitutes a fixpoint of another involves computing a process substitution, mapping states of one process to states of the other, that often is not obvious. Hence, VIPS verification is usually turned into equation solving. Existing tools for this proof task, such as VPAM, are highly interactive. We introduce a method that automates the use of UFI. The method uses middle-out reasoning and, so, is able to apply the rule even without elaborating the details of the application. The method introduces meta-variables to represent those bits of the processes’ state space that, at application time, were not known, hence, changing from equation verification to equation solving. Adding this method to the equation plan developed by R. Monroy, A. Bundy and I. Green [Autom. Softw. Eng. 7, No. 3, 263–304 (2000; Zbl 1034.68646)], we have implemented an automatic verification planner. This planner increases the number of verification problems that can be dealt with fully automatically, thus improving upon the current degree of automation in the field.

MSC:

68Q85 Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.)

Citations:

Zbl 1034.68646

Software:

Oyster; fc2tools; CLAM
PDFBibTeX XMLCite
Full Text: DOI Link

References:

[1] Bergstra, J.A., Klop, J.W.: Algebra of communicating processes with abstraction. Theor. Comp. Sci. 37(1), 77–121 (1985) · Zbl 0579.68016 · doi:10.1016/0304-3975(85)90088-X
[2] Bouali, A., Ressouche, A., Roy, V., de Simone, R.: The FC2TOOLS set. In: Alur, R., Henzinger, T. (eds.) Proceedings of the 8th Conference on Computer-Aided Verification, CAV’96. Lecture Notes in Computer Science, vol. 1102, pp. 441–45. Springer, New York (1996)
[3] Boulton, R., Slind, K., Bundy, A., Gordon, M.: An interface between CLAM and HOL. In: Grundy, J., Newey, M. (eds.) 11th International Conference on Theorem Proving in Higher-Order Logics (TPHOLs’98). Lecture Notes in Computer Science, vol. 1479, pp. 87–104. Springer, Camberra (1998)
[4] Bruns, G.: A language for value-passing CCS. LFCS report series ECS-LFCS-91-175, department of computer science. University of Edinburgh (1991)
[5] Bundy, A.: The use of explicit plans to guide inductive proofs. In: Lusk, R., Overbeek, R. (eds.) Proceedings of the 9th Conference on Automated Deduction, pp. 111–120. Springer, Argonne (1988) (Also available from Edinburgh as DAI Research Paper No. 349) · Zbl 0656.68106
[6] Bundy, A., Smaill, A., Hesketh, J.: Turning eureka steps into calculations in automatic program synthesis. In: Clarke, S.L. (ed.) Proceedings of UK IT 90, pp. 221–6 (1990a) (Also available from Edinburgh as DAI Research Paper 448)
[7] Bundy, A., Stevens, A., van Harmelen, F., Ireland, A., Smaill, A.: Rippling: a heuristic for guiding inductive proofs. Artif. Intell. 62, 185–253 (1993) (Also available from Edinburgh as DAI Research Paper No. 567) · Zbl 0789.68121
[8] Bundy, A., van Harmelen, F., Hesketh, J., Smaill, A.: Experiments with proof plans for induction. J. Autom. Reason. 7, 303–324 (1991) (Earlier version available from Edinburgh as DAI Research Paper No 413) · Zbl 0733.68069
[9] Bundy, A., van Harmelen, F., Hesketh, J., Smaill, A., Stevens, A.: A rational reconstruction and extension of recursion analysis. In: Sridharan, N.S. (ed.): Proceedings of the 11th International Joint Conference on Artificial Intelligence, pp. 359–365. Morgan Kaufmann, San Francisco (1989) (Also available from Edinburgh as DAI Research Paper No. 419) · Zbl 0708.68061
[10] Bundy, A., van Harmelen, F., Horn, C., Smaill, A: The oyster-clam system. In: Stickel, M.E. (ed.) Proceedings of the 10th International Conference on Automated Deduction, pp. 647–648. Springer, New York (1990b) (Also available from Edinburgh as DAI Research Paper No. 507)
[11] Cleaveland, R.P.J., Steffen, B.: The concurrency workbench: a semantics-based verification tool for finite-state systems. In: Proceedings of the Workshop on Automated Verification Methods for Finite-State Systems. Springer, New York (1989)
[12] Cleaveland, R., Lewis, P., Smolka, S., Sokolsky, O.: The concurrency factory: a development environment for concurrent systems. In: Alur,R., Henzinger, T. (eds.) Proceedings of the 8th Conference on Computer-Aided Verification, CAV’96. Lecture Notes in Computer Science, vol. 1102, pp. 398–401. Springer, New York (1996)
[13] Cleaveland, R., Panangaden, P.: Type theory and concurrency. Int. J. Parallel Program. 17(2), 153–206 (1988) · Zbl 0678.68017 · doi:10.1007/BF01383954
[14] Gallier, J.: Logic for Computer Science. Harper & Row, New York (1986) · Zbl 0605.03004
[15] Groote, J., Ponse, A.: Proof theory for {\(\mu\)}CRL. In: Andrews, D. et al (ed.) Proceedings of the International Workshop on Semantics of Specification Languages, pp. 231–250. Springer, New York (1994) · Zbl 0813.68135
[16] Groote, J., Ponse, A.: The syntax and semantics of {\(\mu\)}CRL. In: Ponse, A., Verhoef, C., van Vlijmen, S. (eds.) Algebra of Communicating Processes 1994. pp. 26–62, Springer, New York (1995)
[17] Groote, J.F., Reniers, M.A.: Algebraic process verification. In: Bergstra, J.A., Ponse, A., Smolka, S. (eds.): Handbook of Process Algebra, pp. 1–66. Elsevier, Amsterdam (2001) · Zbl 1035.68069
[18] Groote, J.F., Springintveld, J.: Focus points and convergent processes operators: a proof strategy for protocol verification. J. Log. Algebr. Program. 49, 31–60 (2001) · Zbl 1015.68175 · doi:10.1016/S1567-8326(01)00010-8
[19] Hennessy, M., Lin, H.: Symbolic bisimulations. Theoret. Comput. Sci. 138, 353–389 (1995) (Also available from Sussex as Computing Science Technical Report 1/92) · Zbl 0874.68187
[20] Hennessy, M., Lin, H.: Unique fixpoint induction for message-passing process calculi. In: Computing: The Australasian Theory Symposium (CATS’97), Sydney, February 1997 (Also available from Sussex as Computing Science Technical Report 6/95)
[21] Ireland, A.: The use of planning critics in mechanizing inductive proofs. In: Voronkov, A. (ed.) International Conference on Logic Programming and Automated Reasoning–LPAR 92, St. Petersburg. Lecture Notes in Artificial Intelligence, vol. 624, pp. 178–89. Springer, New York (1992). Also available from Edinburgh as DAI Research Paper No. 592
[22] ISO: Information processing systems–Open Systems Interconnection–LOTOS–A formal description technique based on the temporal ordering of observational behaviour. ISO 8807 (1989)
[23] Korver, H., Springintveld, J.: A computer-checked verification of Milner’s scheduler. In: Proceedings of the International Symposium on Theoretical Aspects of Computer Software (TACS’94). Lecture Notes in Computer Science, vol. 789, pp. 161–78. Springer, Sendai (1994) · Zbl 0942.68710
[24] Kurshan, R.P., McMillan, K.: A structural induction theorem for processes. In: 8th ACM Symposium on Principles Of Distributed Computing (PODC), pp. 239–47. ACM, New York (1989) · Zbl 0828.68096
[25] Lin, H.: A verification tool for value-passing processes. In: Proceedings of 13th International Symposium on Protocol Specification, Testing and Verification. North-Holland, Amsterdam (1993) (Also available from Sussex as Computing Science Technical Report 8/93)
[26] Lin, H.: On implementing unique fixpoint induction for value- passing processes. In: Proceedings of TACAS’95 Workshop on Tools and Algorithms for the Construction and Analysis of Systems, Aarhus, 19–20 May 1995a
[27] Lin, H.: PAM: a process algebra manipulator. Form. Methods Syst. Des. 7(3), 243–259 (1995b) · Zbl 05479850 · doi:10.1007/BF01384078
[28] Milner, R.: Communication and Concurrency. Prentice Hall, London (1989) · Zbl 0683.68008
[29] Milner, R., Parrow, J., Walker, D.: Mobile logics for mobile processes. Theoret. Comput. Sci. 114, 149–71 (1993) (Also available from Edinburgh, as Research Report ECS-LFCS-91-136) · Zbl 0778.68033
[30] Monroy, R.: Planning Proofs of Correctness of CCS Systems. Ph.D. thesis, Edinburgh University (1998)
[31] Monroy, R., Bundy, A., Green, I.: Planning equational verification in CCS. In: Redmiles, D., Nuseibeh, B. (eds.) 13th Conference on Automated Software Engineering, ASE’98, pp. 43–52, Hawaii, 13–16 October 1998 (Candidate to best paper award)
[32] Monroy, R., Bundy, A., Green, I.: Planning proofs of equations in CCS. Autom. Softw. Eng. 7(3), 263–304 (2000a) · Zbl 1034.68646 · doi:10.1023/A:1008770222354
[33] Monroy, R., Bundy, A., Green, I.: Searching for a solution to program verification = equation solving in CCS. In: Cairó, O., Sucar, L., Cantú, F. (eds.) Mexican Internation Conference on Artificial Intelligence, MICAI’00. Lecture Notes in Artificial Intelligence, vol. 1793, pp. 1–12. Springer-Verlag, Acapulco (2000b)
[34] Nesi, M.: Mechanizing a proof by induction of process algebra specifications in higher-order logic. In: Larsen, K.G., Skou, A. (eds.) Proceedings of the 3rd International Workshop in Computer Aided Verification (CAV’91). Lecture Notes in Computer Science No. 575. Springer, New York (1992)
[35] Nesi, M.: Formalising a value-passing calculus in HOL. Form. Asp. Comput. 11, 160–199 (1999) · Zbl 0937.68112 · doi:10.1007/s001650050046
[36] Park, D.: Concurrency and automata on infinite sequences. In: Deussen, P. (ed.) Proceedings of the 5th GI-Conference on Theoretical Computer Science, LNCS 104, pp. 167–183, Karlsruhe, 23–25 March 1981
[37] Rathke, J.: Unique fixpoint induction for value-passing processes (Extended Abstract). In: Proceedings of the 12th Annual IEEE Symposium on Logic in Computer Science, pp. 140–8. IEEE Computer Society, Warsaw (1997)
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.