Skip to main content
SpringerLink
Log in

A Proof Assistant for Mobile Processes

  • Conference paper
Advanced Parallel Processing Technologies (APPT 2003)

Part of the book series: Lecture Notes in Computer Science ((LNCS,volume 2834))

Included in the following conference series:

  • 537 Accesses

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

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 84.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 109.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. 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)

    Google Scholar 

  2. 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)

    Chapter  Google Scholar 

  3. Dam, M.: Model checking mobile processes. In: Best, E. (ed.) CONCUR 1993. LNCS, vol. 715, Springer, Heidelberg (1993)

    Google Scholar 

  4. 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)

    Google Scholar 

  5. Hennessy, M., Lin, H.: Symbolic bisimulations. Technical Report 1/92, Computer Science, University of Sussex (1992)

    Google Scholar 

  6. Hennessy, M., Lin, H.: Proof systems for message-passing process algebras. Technical Report 5/93, Computer Science, University of Sussex (1993)

    Google Scholar 

  7. 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)

    Google Scholar 

  8. 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)

    Google Scholar 

  9. Milner, R.: Communication and Concurrency. Prentice Hall, Englewood Cliffs (1989)

    MATH  Google Scholar 

  10. 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)

    Google Scholar 

  11. 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)

    Google Scholar 

  12. Montanari, U., Pistore, M.: Checking bisimilarity for finitary π-calculus. In: Lee, I., Smolka, S.A. (eds.) CONCUR 1995. LNCS, vol. 962, Springer, Heidelberg (1995)

    Google Scholar 

  13. De Simone, R., Vergamimi, D.: Aboard auto. Technical Report RT111, INRIA (1989)

    Google Scholar 

  14. Xutao, D., Zhoujun, L.: Proving the ab-protocol in PiM. Technical Report. National University of Defence Technology (2001)

    Google Scholar 

  15. Xutao, D., Zhoujun, L.: On formulating the unique fixpoint induction for the π-calculus. Technical Report. National University of Defence Technology (2001)

    Google Scholar 

  16. Parrow, J., Milner, R., Walker, D.: A calculus of mobile processes, part I and II. Information and Computation 100, 1–77 (1992)

    Article  MATH  MathSciNet  Google Scholar 

  17. Zhoujun, L.: The Verification Theory and Algorithms for the Value-Passing CCS and π-Calculus. PhD Thesis, National University of Defence Technology (1999)

    Google Scholar 

  18. 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)

    Google Scholar 

  19. 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)

    Google Scholar 

  20. 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)

    Google Scholar 

  21. Hennessy, M., Lin, H.: Unique fixpoint induction for messing-passing process calculi. In: Proceedings of CATS 1997 Computing: Australian Theory Symposium (1997)

    Google Scholar 

  22. Rathke, J.: Unique fixpoint induction for value-passing processes (Extended Abstract). In: Proceedings of the 12th Symposium on Logic in Computer Science (1997)

    Google Scholar 

  23. 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)

    Chapter  Google Scholar 

  24. 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)

    Chapter  Google Scholar 

  25. 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)

    Chapter  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. School of Computer Science, National University of Defence Technology, Changsha, 410073, P.R.China

    Xutao Du & Zhoujun Li

Authors
  1. Xutao Du
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Zhoujun Li
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. PDL, National University of Defense Technology, 410073, Changsha, China

    Xingming Zhou

  2. Department of Network Engineering, School of Computer Science, National University of Defense Technology, 410073, Changsha, China

    Ming Xu

  3. Fraunhofer FIRST, Kekuléstr. 7, D-12489, Berlin, Germany

    Stefan Jähnichen

  4. Department of Computing, Hong Kong Polytechnic University, Kowloon, Hong Kong, China

    Jiannong Cao

Rights and permissions

Reprints 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

Publish with us

Policies and ethics

Search

Navigation