Abstract
The π-calculus is invented for modelling mobility (the ability to dynamically change the communication structures) within systems. It can conveniently represents hardware or software concurrent systems with evolving communication structures. After modelling those systems with the π-calculus, we can formally verify the correctness of them. The verification process is error-prone since there are many details. Hence some mechanical support is necessary. We have developed an interactive proof assistant for the monadic π-calculus, namely PiM(for the Pi-calculus Manipulator). It is based on symbolic style proof systems with respect to different bisimulation congruences. And we have generalized a version of the unique fixpoint induction to deal with recursions. Using PiM users can check different bisimulation congruences between π-calculus agents by directly manipulating syntactic terms of them.
This work is supported by National Natural Science Foundation of China (No.90104026 and No.60073001), 863 Project(2002AA144040) and Visiting Scholar Foundation of Key Lab. In University.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
Cleaveland, R., Parrow, J., Steffen, B.: A semantic based verification tool for finite state systems. In: Proceedings of the 9th International symposium on Protocol Specification, Testing and Verification, North Holland, Amsterdam (1989)
Lin, H.: Complete proof systems for observation congruences in finite-control π- calculus. In: Larsen, K.G., Skyum, S., Winskel, G. (eds.) ICALP 1998. LNCS, vol. 1443, pp. 443–454. Springer, Heidelberg (1998)
Dam, M.: Model checking mobile processes. In: Best, E. (ed.) CONCUR 1993. LNCS, vol. 715, Springer, Heidelberg (1993)
Mavw, S., Veltink, G.: A proof assistant PSF. In: Larsen, K.G., Skou, A. (eds.) CAV 1991. LNCS, vol. 575, pp. 158–168. Springer, Heidelberg (1992)
Hennessy, M., Lin, H.: Symbolic bisimulations. Technical Report 1/92, Computer Science, University of Sussex (1992)
Hennessy, M., Lin, H.: Proof systems for message-passing process algebras. Technical Report 5/93, Computer Science, University of Sussex (1993)
Lin, H.: PAM: A process algebra manipulator. In: Larsen, K.G., Skou, A. (eds.) CAV 1991. LNCS, vol. 575, pp. 136–146. Springer, Heidelberg (1992)
Lin, H.: A verification tool for value-passing processes. In: Proceedings of 13th International Symposium on Protocol Specification, Testing and Verification, IFIP Transactions, North Holland, Amsterdam (1993)
Milner, R.: Communication and Concurrency. Prentice Hall, Englewood Cliffs (1989)
Victor, B., Moller, F.: The Mobility Workbench – a tool for the π-calculus. In: Dill, D.L. (ed.) CAV 1994. LNCS, vol. 818, pp. 428–440. Springer, Heidelberg (1994)
Gnesi, S., Montanari, U., Pistore, M., Ferrari, G., Ferro, G., Risori, G.: An automata-based verification environment for mobile processes. In: Brinksma, E. (ed.) TACAS 1997. LNCS, vol. 1217, Springer, Heidelberg (1997)
Montanari, U., Pistore, M.: Checking bisimilarity for finitary π-calculus. In: Lee, I., Smolka, S.A. (eds.) CONCUR 1995. LNCS, vol. 962, Springer, Heidelberg (1995)
De Simone, R., Vergamimi, D.: Aboard auto. Technical Report RT111, INRIA (1989)
Xutao, D., Zhoujun, L.: Proving the ab-protocol in PiM. Technical Report. National University of Defence Technology (2001)
Xutao, D., Zhoujun, L.: On formulating the unique fixpoint induction for the π-calculus. Technical Report. National University of Defence Technology (2001)
Parrow, J., Milner, R., Walker, D.: A calculus of mobile processes, part I and II. Information and Computation 100, 1–77 (1992)
Zhoujun, L.: The Verification Theory and Algorithms for the Value-Passing CCS and π-Calculus. PhD Thesis, National University of Defence Technology (1999)
Lin, H.: Complete inference systems for weak bisimulation equivalences in the π- calculus. In: Mosses, P.D., Schwartzbach, M.I., Nielsen, M. (eds.) CAAP 1995, FASE 1995, and TAPSOFT 1995. LNCS, vol. 915, pp. 187–201. Springer, Heidelberg (1995)
Lin, H.: Unique fixpoint induction for mobile processes. In: Lee, I., Smolka, S.A. (eds.) CONCUR 1995. LNCS, vol. 962, pp. 88–192. Springer, Heidelberg (1995)
Lin, H.: On implementing unique fixpoint induction for value-passing processes. In: Brinksma, E., Steffen, B., Cleaveland, W.R., Larsen, K.G., Margaria, T. (eds.) TACAS 1995. LNCS, vol. 1019, Springer, Heidelberg (1995)
Hennessy, M., Lin, H.: Unique fixpoint induction for messing-passing process calculi. In: Proceedings of CATS 1997 Computing: Australian Theory Symposium (1997)
Rathke, J.: Unique fixpoint induction for value-passing processes (Extended Abstract). In: Proceedings of the 12th Symposium on Logic in Computer Science (1997)
Lin, H.: Complete proof systems for observation congruences in finite-control π- calculus. In: Larsen, K.G., Skyum, S., Winskel, G. (eds.) ICALP 1998. LNCS, vol. 1443, pp. 443–454. Springer, Heidelberg (1998)
Li, Z., Chen, H.: Checking strong/weak bisimulation equivalences and observation congruence for the π-calculus. In: Larsen, K.G., Skyum, S., Winskel, G. (eds.) ICALP 1998. LNCS, vol. 1443, pp. 707–718. Springer, Heidelberg (1998)
Li, Z., Chen, H.: Computing strong/weak bisimulation equivalences and observation congruence for value-passing processes. In: Cleaveland, W.R. (ed.) TACAS 1999. LNCS, vol. 1579, pp. 300–314. Springer, Heidelberg (1999)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2003 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Du, X., Li, Z. (2003). A Proof Assistant for Mobile Processes. In: Zhou, X., Xu, M., Jähnichen, S., Cao, J. (eds) Advanced Parallel Processing Technologies. APPT 2003. Lecture Notes in Computer Science, vol 2834. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-39425-9_26
Download citation
DOI: https://doi.org/10.1007/978-3-540-39425-9_26
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-20054-3
Online ISBN: 978-3-540-39425-9
eBook Packages: Springer Book Archive