×

zbMATH — the first resource for mathematics

A process calculus BigrTiMo of mobile systems and its formal semantics. (English) Zbl 07349690
Summary: In this paper, we present a process calculus called BigrTiMo that combines the rTiMo calculus and the Bigraph model. BigrTiMo calculus is capable of specifying a rich variety of properties for structure-aware mobile systems. Compared with rTiMo, our BigrTiMo calculus can specify not only time, mobility and local communication, but also remote communication. We then investigate the operational semantics of the BigrTiMo calculus and develop an executable formal specification of our BigrTiMo calculus in a declarative language called Maude. In addition, we verify safety properties and liveness properties of the mobile systems described by BigrTiMo using state exploration and LTL model checking in Maude. Based on Hoare and He’s Unifying Theories of Programming (UTP), we study the semantic foundation of this highly expressive modelling language and propose a denotational semantic model and a set of algebraic laws for it. The semantic model in this paper covers time, location, communication and global shared variable at the same time. We also demonstrate the proofs of some algebraic laws based on our denotational semantics. Moreover, we explore how the algebraic semantics relates with the operational semantics and denotational semantics, which is conducted by the study of deriving the operational semantics and denotational semantics from algebraic semantics. We prove the equivalence between the derived transition system (e.g., the operational semantics) and the derivation strategy, which indicates that the operational semantics is sound and complete.
MSC:
68-XX Computer science
PDF BibTeX XML Cite
Full Text: DOI
References:
[1] Aman B, Ciobanu G (2007) Mobile ambients with timers and types. In: Theoretical aspects of computing—ICTAC 2007, 4th International colloquium, volume 4711 of lecture notes in computer science, pp 50-63, Macau, China, September 26-28. Springer · Zbl 1147.68586
[2] Agrigoroaiei, O.; Ciobanu, G., Rewriting logic specification of membrane systems with promoters and inhibitors, Electr Notes Theor Comput Sci, 238, 3, 5-22 (2009) · Zbl 1347.68125
[3] Aman B, Ciobanu G (2013) Real-time migration properties of rtimo verified in uppaal. In: Software engineering and formal methods—11th international conference, SEFM 2013, volume 8137 of lecture notes in computer science, pp 31-45, Madrid, Spain, September 25-27. Springer
[4] Alur, R.; Dill, DL, A theory of timed automata, Theor Comput Sci, 126, 2, 183-235 (1994) · Zbl 0803.68071
[5] Abadi, M.; Gordon, AD, A calculus for cryptographic protocols: The spi calculus, Inf Comput, 148, 1, 1-70 (1999) · Zbl 0924.68073
[6] Behrmann G, David A, Guldstrand LK (2004) A tutorial on uppaal. In: Formal methods for the design of real-time systems, international school on formal methods for the design of computer, communication and software systems, SFM-RT 2004, Bertinoro, Italy, September 13-18, 2004, Revised Lectures, pp 200-236
[7] Berger M (2004) Basic theory of reduction congruence fortwo timed asynchronous pi-calculi. In: CONCUR 2004—concurrency theory, 15th international conference, volume 3170 of lecture notes in computer science, pp 115-130, London, UK, August 31-September 3. Springer · Zbl 1099.68064
[8] Bergstra, JA; Klop, JW, Process algebra for synchronous communication, Inf Control, 60, 1-3, 109-137 (1984) · Zbl 0597.68027
[9] Brookes, SD, Full abstraction for a shared-variable parallel language, Inf Comput, 127, 2, 145-163 (1996) · Zbl 0856.68037
[10] Clavel, M., Durán, F., Eker, S., Lincoln, P., Martí -Oliet N, Meseguer J, Quesada JF, : Maude: specification and programming in rewriting logic. Theor Comput Sci 285(2), 187-243 (2002) · Zbl 1001.68059
[11] Clavel M, Durán F, Eker S, Lincoln P, Martí -Oliet N, Meseguer J, Talcott CL (eds) (2007) All about Maude—a high-performance logical framework, how to specify, program and verify systems in rewriting logic, volume 4350 of lecture notes in computer science. Springer · Zbl 1115.68046
[12] Cardelli, L.; Gordon, AD, Mobile ambients, Electr Notes Theor Comput Sci, 10, 198-201 (1997) · Zbl 1253.68238
[13] Ciobanu, G.; Koutny, M., Timed mobility in process algebra and petri nets, J Log Algebr Program, 80, 7, 377-391 (2011) · Zbl 1230.68154
[14] Cavalcanti, A.; Wellings, AJ; Woodcock, J., The safety-critical java memory model formalised, Formal Asp Comput, 25, 1, 37-57 (2013) · Zbl 1259.68029
[15] Duran, A.; Cavalcanti, A.; Sampaio, A., An algebraic approach to the design of compilers for object-oriented languages, Formal Asp Comput, 22, 5, 489-535 (2010) · Zbl 1214.68126
[16] Eker, S.; Meseguer, J.; Sridharanarayanan, A., The maude LTL model checker, Electr Notes Theor Comput Sci, 71, 162-187 (2002) · Zbl 1272.68243
[17] Gleirscher, M.; Foster, S.; Nemouchi, Y.; Ölveczky, PC; Salaün, G., Evolution of formal model-based assurance cases for autonomous robots, Software engineering and formal methods-17th international conference, SEFM 2019, Oslo, Norway, September 18-20, 2019, Proceedings (2019), Springer
[18] Hennessy, M.: Algebraic theory of processes. MIT Press series in the foundations of computing, MIT Press, Cambridge (1988)
[19] Hennessy, M., Semantics of programming languages-an elementary introduction using structural operational semantics (1990), Wiley · Zbl 0723.68067
[20] He, J.; Hoare, CAR, From algebra to operational semantics, Inf Process Lett, 45, 2, 75-80 (1993) · Zbl 0795.68124
[21] Hoare CAR, He J (1998) Unifying theories of programming. Prentice Hall international series in computer science
[22] Hoare, CAR; Hayes, IJ; He, J.; Morgan, C.; Roscoe, AW; Sanders, JW; Sørensen, IH; Michael, SJ; Sufrin, B., Laws of programming, Commun ACM, 30, 8, 672-686 (1987) · Zbl 0629.68006
[23] Hoare, CAR; He, J.; Sampaio, A., Normal form approach to compiler design, Acta Inf, 30, 8, 701-739 (1993) · Zbl 0790.68023
[24] Gérard H, Gilles K, Christine P-M (2004) The coq proof assistant a tutorial. Rapport Tech 178
[25] He, J.; Li, Q., A new roadmap for linking theories of programming and its applications on GCL and CSP, Sci Comput Program, 162, 3-34 (2018)
[26] Hoare, CAR, An axiomatic basis for computer programming (reprint), Commun ACM, 26, 1, 53-56 (1983)
[27] Hoare, CAR, Communicating sequential processes (1985), Upper Saddle River: Prentice-Hall, Upper Saddle River · Zbl 0637.68007
[28] Hoare CAR (2013) Unifying semantics for concurrent programming. In: Computation, logic, games, and quantum foundations. The many facets of Samson Abramsky—essays dedicated to Samson Abramsky on the occasion of his 60th birthday, volume 7860 of lecture notes in computer science, pp 139-149. Springer
[29] Hennessy, M.; Plotkin, GD, Full abstraction for a simple parallel programming language, Mathematical foundations of computer science 1979, proceedings, 8th symposium, 108-120 (1979), Czechoslovakia, Springer: Olomouc, Czechoslovakia, Springer
[30] He, J.; Seidel, K.; McIver, A., Probabilistic models for the guarded command language, Sci Comput Program, 28, 2-3, 171-192 (1997) · Zbl 0877.68014
[31] Hoare, T.; van Staden, S., In praise of algebra, Formal Asp Comput, 24, 4-6, 423-431 (2012) · Zbl 1259.68030
[32] Hoare, T.; van Staden, S.; Möller, B.; Struth, G.; Zhu, H., Developments in concurrent kleene algebra, J Log Algebr Methods Program, 85, 4, 617-636 (2016) · Zbl 1344.68149
[33] He, J.; Zhu, H.; Pu, G., A model for bpel-like languages, Front Comput Sci China, 1, 1, 9-19 (2007)
[34] Lakos C (2005) A petri net view of mobility. In: Formal techniques for networked and distributed systems—FORTE 2005, 25th IFIP WG 6.1 international conference, Taipei, Taiwan, October 2-5, 2005, Proceedings, pp 174-188 · Zbl 1169.68547
[35] Lakos, C., Modelling mobile IP with mobile petri nets, Trans Petri Nets Other Models Concurr, 3, 127-158 (2009) · Zbl 1266.68138
[36] Mäkelä M (2002) Maria: Modular reachability analyser for algebraic system nets. In: Applications and theory of Petri nets 2002, 23rd international conference, ICATPN 2002, Adelaide, Australia, June 24-30, 2002, Proceedings, pp 434-444 · Zbl 1047.68554
[37] Meseguer, J., Conditioned rewriting logic as a united model of concurrency, Theor Comput Sci, 96, 1, 73-155 (1992) · Zbl 0758.68043
[38] Milner, R.: A calculus of communicating systems. lecture notes in computer science, vol. 92. Springer, Berlin (1980) · Zbl 0452.68027
[39] Milner, R., Communicating and mobile systems-the pi-calculus (1999), Cambridge: Cambridge University Press, Cambridge · Zbl 0942.68002
[40] Milner, R., The space and motion of communicating agents (2009), Cambridge: Cambridge University Press, Cambridge · Zbl 1175.68461
[41] Milner, R.; Parrow, J.; Walker, D., A calculus of mobile processes, I. Inf Comput, 100, 1, 1-40 (1992) · Zbl 0752.68036
[42] Milner, R.; Parrow, J.; Walker, D., A calculus of mobile processes, II. Inf Comput, 100, 1, 41-77 (1992) · Zbl 0752.68037
[43] McCann, PJ; Roman, G-C, Modeling mobile IP in mobile UNITY, ACM Trans Softw Eng Methodol, 8, 2, 115-146 (1999)
[44] Nielson, HR; Nielson, F., Semantics with applications-a formal introduction (1992), Wiley, Hoboken: Wiley professional computing, Wiley, Hoboken · Zbl 0875.68626
[45] Nipkow, T., Paulson, L.C., Wenzel, M.: Isabelle/HOL-a proof assistant for higher-order logic. lecture notes in computer science, vol. 2283. Springer, Berlin (2002) · Zbl 0994.68131
[46] O’Hearn, P.W.: Resources, concurrency, and local reasoning. Theor Comput Sci 375(1-3), 271-307 (2007)
[47] Orava, F.; Parrow, J., An algebraic verification of a mobile network, Formal Asp Comput, 4, 6, 497-543 (1992) · Zbl 0782.68081
[48] Paulson LC (1994) Isabelle—a generic theorem prover (with a contribution by T. Nipkow), volume 828 of lecture notes in computer science. Springer, Berlin · Zbl 0825.68059
[49] Perkins, CE, IP mobility support for ipv4, revised, RFC, 5944, 1-100 (2010)
[50] Pereira E (2015) Mobile reactive systems over bigraphical machines—a programming model and its implementation. PhD thesis, University of California, Berkeley, USA
[51] Plotkin, GD, A structural approach to operational semantics, J Log Algebr Program, 60-61, 17-139 (2004) · Zbl 1082.68062
[52] Pita I, Riesco A (2015) Specifying and analyzing the kademlia protocol in maude. In: Theoretical aspects of computing—ICTAC 2015, volume 9399 of lecture notes in computer science, pp 524-541, Colombia, October 29-31. Springer · Zbl 06545745
[53] Potop-Butucaru, M.; Sznajder, N.; Tixeuil, S.; Urbain, X.; Flocchini, P.; Prencipe, G.; Santoro, N., Formal methods for mobile robots, Distributed computing by mobile entities, current research in moving and computing (2019), Springer
[54] Regensburger, F.; Barnard, A.; Steffen, B., Formal verification of SDL systems at the siemens mobile phone department, Tools and algorithms for construction and analysis of systems, 4th international conference, TACAS ’98, Held as Part of the European joint conferences on the theory and practice of software, ETAPS’98, Lisbon, Portugal, March 28-April 4, 1998, proceedings (1998), Springer
[55] Riesco, A.; Ogata, K.; Futatsugi, K., A maude environment for cafeobj, Formal Asp Comput, 29, 2, 309-334 (2017) · Zbl 1358.68195
[56] Reed, GM; Roscoe, AW, A timed model for communicating sequential processes, Theor Comput Sci, 58, 249-261 (1988) · Zbl 0655.68031
[57] Reisig, W., Rozenberg, G. (eds.): Lectures on Petri nets I: basic models. lecture notes in computer science, vol. 1491. Springer, Berlin (1998)
[58] Reisig, W., Rozenberg, G. (eds.): Lectures on Petri nets II: applications. lecture notes in computer science, vol. 1492. Springer, Berlin (1998)
[59] Sun, J.; Liu, Y.; Dong, JS; Chen, C., Integrating specification and programs for system modeling and verification, TASE 2009, third IEEE international symposium on theoretical aspects of software engineering, 29-31 July 2009, 127-135 (2009), China: Tianjin, China
[60] Sun J, Liu Y, Dong JS, Pang J (2009) Pat: Towards flexible verification under fairness volume 5643 of lecture notes in computer science, pp 709-714. Springer, Berlin
[61] Stoy JE (1979) Foundations of denotational semantics. In: Abstract software specifications, 1979 Copenhagen Winter School, volume 86 of lecture notes in computer science, pp 43-99. Springer
[62] Shi, L.; Zhao, Y.; Liu, Y.; Sun, J.; Dong, JS; Qin, S., A utp semantics for communicating processes with shared variables and its formal encoding in pvs, Formal Asp Comput, 30, 3-4, 351-380 (2018) · Zbl 1398.68373
[63] Tarski, A., A lattice-theoretical fixpoint theorem and its applications, Pac J Math, 5, 285-309 (1955) · Zbl 0064.26004
[64] Padberg, U., Schulz, A., (2016) Model checking reconfigurable petri nets with maude. In: Graph transformation-9th international conference, ICGT, : in memory of Hartmut Ehrig, held as part of STAF 2016. lecture notes in computer science, pp 54-70, Vienna, vol. 9761. Springer, Austria (2016) · Zbl 1344.68141
[65] Verdejo, A., Martí -Oliet N, : Executable structural operational semantics in maude. J Log Algebr Program 67(1-2), 226-293 (2006) · Zbl 1088.68095
[66] Watt, DA, Programming language syntax and semantics (1991), Prentice Hall, Upper Saddle River: Prentice Hall international series in computer science, Prentice Hall, Upper Saddle River · Zbl 0828.68094
[67] Xie, W.; Xiang, S.; Zhu, H., A utp approach for rtimo, Formal Asp Comput, 30, 6, 713-738 (2018) · Zbl 1425.68304
[68] Xie W, Zhu H, Qin S (2018) UTP semantics for bigrtimo. In: Formal methods and software engineering—20th international conference on formal engineering methods, ICFEM 2018, volume 11232 of lecture notes in computer science, pp 337-353, Gold Coast, QLD, Australia, November 12-16. Springer
[69] Xie W, Zhu H, Xu Q (2017) Bigrtimo-a process algebra for structure-aware mobile systems. In: 22nd International conference on engineering of complex computer systems, ICECCS 2017, pp 50-59, Fukuoka, Japan, November 5-8. IEEE Computer Society
[70] Xie W, Zhu H, Zhang M, Lu G, Fang Y (2018) Formalization and verification of mobile systems calculus using the rewriting engine maude. In: 2018 IEEE 42nd annual computer software and applications conference, COMPSAC 2018, pp 213-218, Tokyo, Japan, 23-27. IEEE Computer Society
[71] Zhu, H.; He, J.; Li, J.; Bowen, JP, Algebraic approach to linking the semantics of web services, ISSE, 7, 3, 209-224 (2011)
[72] Zhu, H.; Qin, S.; He, J.; Bowen, JP, PTSC: probability, time and shared-variable concurrency, ISSE, 5, 4, 271-284 (2009)
[73] Zhu H, Sanders JW, He J, Qin S (2012) Denotational semantics for a probabilistic timed shared-variable language. In: Unifying theories of programming, 4th international symposium, UTP 2012, volume 7681 of lecture notes in computer science, pp 224-247, Paris, France, August 27-28 · Zbl 1452.68062
[74] Zhu, H.; Yang, F.; He, J.; Bowen, JP; Sanders, JW; Qin, S., Linking operational semantics and algebraic semantics for a probabilistic timed shared-variable language, J Log Algebr Program, 81, 1, 2-25 (2012) · Zbl 1243.68208
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. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.