{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,21]],"date-time":"2026-02-21T19:09:52Z","timestamp":1771700992204,"version":"3.50.1"},"reference-count":43,"publisher":"MDPI AG","issue":"2","license":[{"start":{"date-parts":[[2022,2,9]],"date-time":"2022-02-09T00:00:00Z","timestamp":1644364800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Future Internet"],"abstract":"<jats:p>Fog systems are a new emergent technology having a wide range of architectures and pronounced needs making their design complex. Consequently, the design of fog systems is crucial, including service portability and interoperability between the various elements of a system being the most essential aspects of fog computing. This article presents a fog system cross-layer architecture as a first step of such a design to provide a graphical and conceptual description. Then, a BiAgents* (Bigraphical Agents) formal model is defined to provide a rigorous description of physical, virtual, and behavioural aspects of Fog systems. Besides, this formalisation is implemented and executed under a Maude strategy system. The proposed approach is illustrated through a case study: an airport terminal Luggage Inspection System (LIS) while checking the correctness of its relevant properties: the portability of data and their interoperability. The integration of the Maude strategies in the rewriting of Fog system states made it possible to guide the execution of the model and its analysis.<\/jats:p>","DOI":"10.3390\/fi14020052","type":"journal-article","created":{"date-parts":[[2022,2,9]],"date-time":"2022-02-09T21:19:06Z","timestamp":1644441546000},"page":"52","update-policy":"https:\/\/doi.org\/10.3390\/mdpi_crossmark_policy","source":"Crossref","is-referenced-by-count":3,"title":["A Strategy-Based Formal Approach for Fog Systems Analysis"],"prefix":"10.3390","volume":"14","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-8378-1855","authenticated-orcid":false,"given":"Souad","family":"Marir","sequence":"first","affiliation":[{"name":"LIRE Laboratory, TLSI Department, Constantine 2 University, Constantine 25000, Algeria"},{"name":"LIUPPA Laboratory, Universite de Pau et des Pays de l\u2019Adour, E2S UPPA, LIUPPA, 64000 Pau, France"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-4563-4061","authenticated-orcid":false,"given":"Faiza","family":"Belala","sequence":"additional","affiliation":[{"name":"LIRE Laboratory, TLSI Department, Constantine 2 University, Constantine 25000, Algeria"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-3311-4146","authenticated-orcid":false,"given":"Nabil","family":"Hameurlain","sequence":"additional","affiliation":[{"name":"LIUPPA Laboratory, Universite de Pau et des Pays de l\u2019Adour, E2S UPPA, LIUPPA, 64000 Pau, France"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"1968","published-online":{"date-parts":[[2022,2,9]]},"reference":[{"key":"ref_1","unstructured":"(2018). IEEE Standard for Adoption of OpenFog Reference Architecture for Fog Computing. Standard No. IEEE Standard 1934\u20132018."},{"key":"ref_2","doi-asserted-by":"crossref","first-page":"77","DOI":"10.1016\/j.dcan.2017.07.001","article-title":"Edge computing technologies for Internet of Things: A primer","volume":"4","author":"Ai","year":"2018","journal-title":"Digit. Commun. Netw."},{"key":"ref_3","doi-asserted-by":"crossref","unstructured":"Yi, S., Hao, Z., Qin, Z., and Li, Q. (2015, January 12\u201313). Fog computing: Platform and applications. Proceedings of the 2015 Third IEEE Workshop on Hot Topics in Web Systems and Technologies (HotWeb), Washington, DC, USA.","DOI":"10.1109\/HotWeb.2015.22"},{"key":"ref_4","doi-asserted-by":"crossref","first-page":"416","DOI":"10.1109\/COMST.2017.2771153","article-title":"A comprehensive survey on fog computing: State-of-the-art and research challenges","volume":"20","author":"Mouradian","year":"2017","journal-title":"IEEE Commun. Surv. Tutor."},{"key":"ref_5","unstructured":"Asadi, M., Fathy, M., Mahini, H., and Rahmani, A.M. (2021). An Evolutionary Game Approach to Safety-Aware Speed Recommendation in Fog\/Cloud-Based Intelligent Transportation Systems. IEEE Trans. Intell. Transp. Syst., 1\u201310."},{"key":"ref_6","doi-asserted-by":"crossref","unstructured":"Xiao, Y., and Krunz, M. (2021). AdaptiveFog: A Modelling and Optimization Framework for Fog Computing in Intelligent Transportation Systems. IEEE Trans. Mob. Comput.","DOI":"10.1109\/TMC.2021.3080397"},{"key":"ref_7","doi-asserted-by":"crossref","unstructured":"Thampi, S.M., Gelenbe, E., Atiquzzaman, M., Chaudhary, V., and Li, K.C. (2021). Modelling a Plain N-Hypercube Topology for Migration in Fog Computing. Advances in Computing and Network Communications, Springer.","DOI":"10.1007\/978-981-33-6987-0"},{"key":"ref_8","doi-asserted-by":"crossref","first-page":"9114113","DOI":"10.1155\/2021\/9114113","article-title":"IoT Workflow Scheduling Using Intelligent Arithmetic Optimization Algorithm in Fog Computing","volume":"2021","author":"Abualigah","year":"2021","journal-title":"Comput. Intell. Neurosci."},{"key":"ref_9","doi-asserted-by":"crossref","unstructured":"Souad, M., Faiza, B., and Nabil, H. (2020, January 28\u201330). Formal Modeling IoT Systems on the Basis of BiAgents* and Maude. Proceedings of the 2020 International Conference on Advanced Aspects of Software Engineering (ICAASE), Constantine, Algeria.","DOI":"10.1109\/ICAASE51408.2020.9380126"},{"key":"ref_10","doi-asserted-by":"crossref","unstructured":"Milner, R. (2009). The Space and Motion of Communicating Agents, Cambridge University Press.","DOI":"10.1017\/CBO9780511626661"},{"key":"ref_11","unstructured":"Pereira, E., Kirsch, C., and Sengupta, R. (2012). Biagentsa bigraphical agent model for structure-aware computation. Cyber-Phys. Cloud Comput. Work. Pap. CPCC Berkeley, 1\u201313. Available online: http:\/\/cpcc.berkeley.edu\/papers\/paperBiagents12.pdf."},{"key":"ref_12","doi-asserted-by":"crossref","first-page":"3","DOI":"10.1016\/j.entcs.2006.03.017","article-title":"Deduction, strategies, and rewriting","volume":"174","author":"Eker","year":"2007","journal-title":"Electron. Notes Theor. Comput. Sci."},{"key":"ref_13","unstructured":"McKendrick, J. (2022, January 12). Fog Computing: A New IoT Architecture?. Available online: https:\/\/www.rtinsights.com\/what-is-fog-computing-open-consortium."},{"key":"ref_14","doi-asserted-by":"crossref","unstructured":"Iorga, M., Feldman, L., Barton, R., Martin, M.J., Goren, N.S., and Mahmoudi, C. (2018). Fog Computing Conceptual Model, NIST SP, National Institute of Standards and Technology.","DOI":"10.6028\/NIST.SP.500-325"},{"key":"ref_15","doi-asserted-by":"crossref","first-page":"36","DOI":"10.1109\/MCC.2017.25","article-title":"A cooperative fog approach for effective workload balancing","volume":"4","author":"Kapsalis","year":"2017","journal-title":"IEEE Cloud Comput."},{"key":"ref_16","doi-asserted-by":"crossref","first-page":"46","DOI":"10.1109\/MCC.2017.28","article-title":"Cross-site virtual network in cloud and fog computing","volume":"4","author":"Montero","year":"2017","journal-title":"IEEE Cloud Comput."},{"key":"ref_17","doi-asserted-by":"crossref","unstructured":"Bouheroum, A., Benzadri, Z., and Belala, F. (2019, January 26\u201328). Towards a formal approach based on bigraphs for fog security: Case of oil and gas refinery plant. Proceedings of the 2019 7th International Conference on Future Internet of Things and Cloud (FiCloud), Istanbul, Turkey.","DOI":"10.1109\/FiCloud.2019.00017"},{"key":"ref_18","doi-asserted-by":"crossref","unstructured":"Marir, S., Belala, F., and Hameurlain, N. (2018, January 24\u201326). A formal model for interaction specification and analysis in IoT applications. Proceedings of the International Conference on Model and Data Engineering, Marrakesh, Morocco.","DOI":"10.1007\/978-3-030-00856-7_25"},{"key":"ref_19","doi-asserted-by":"crossref","unstructured":"Sales, M. (2013). The Air Logistics Handbook: Air Freight and the Global Supply Chain, Routledge.","DOI":"10.4324\/9780203080078"},{"key":"ref_20","doi-asserted-by":"crossref","unstructured":"da Rocha, H., Espirito-Santo, A., and Abrishambaf, R. (2020, January 18). Semantic interoperability in the industry 4.0 using the IEEE 1451 standard. Proceedings of the IECON 2020 the 46th Annual Conference of the IEEE Industrial Electronics Society, Singapore.","DOI":"10.1109\/IECON43393.2020.9254274"},{"key":"ref_21","first-page":"251","article-title":"Portability in clouds: Approaches and research opportunities","volume":"15","author":"Petcu","year":"2014","journal-title":"Scalable Comput. Pract. Exp."},{"key":"ref_22","first-page":"58","article-title":"Axiomatizing binding bigraphs","volume":"13","author":"Damgaard","year":"2006","journal-title":"Nord. J. Comput."},{"key":"ref_23","doi-asserted-by":"crossref","first-page":"73","DOI":"10.1016\/j.entcs.2008.10.006","article-title":"Stochastic bigraphs","volume":"218","author":"Krivine","year":"2008","journal-title":"Electron. Notes Theor. Comput. Sci."},{"key":"ref_24","doi-asserted-by":"crossref","unstructured":"Sevegnani, M., and Calder, M. (2016, January 17\u201323). BigraphER: Rewriting and analysis engine for bigraphs. Proceedings of the International Conference on Computer Aided Verification, Toronto, ON, Canada.","DOI":"10.1007\/978-3-319-41540-6_27"},{"key":"ref_25","doi-asserted-by":"crossref","first-page":"121","DOI":"10.1016\/j.entcs.2007.02.031","article-title":"Directed bigraphs","volume":"173","author":"Grohmann","year":"2007","journal-title":"Electron. Notes Theor. Comput. Sci."},{"key":"ref_26","doi-asserted-by":"crossref","unstructured":"Perrone, G., Debois, S., and Hildebrandt, T. (2011). Bigraphical refinement. arXiv.","DOI":"10.4204\/EPTCS.55.2"},{"key":"ref_27","unstructured":"Clavel, M., Dur\u00e1n, F., Eker, S., Lincoln, P., Mart\u0131-Oliet, N., Meseguer, J., and Talcott, C. (2005). Maude Manual (Version 2.1), SRI International."},{"key":"ref_28","doi-asserted-by":"crossref","first-page":"227","DOI":"10.1016\/j.entcs.2009.05.022","article-title":"A rewriting semantics for Maude strategies","volume":"238","author":"Meseguer","year":"2009","journal-title":"Electron. Notes Theor. Comput. Sci."},{"key":"ref_29","doi-asserted-by":"crossref","first-page":"1","DOI":"10.4018\/ijaras.2014100101","article-title":"Bigraphical reactive systems based approaches for modeling context-aware systems","volume":"5","author":"Cherfia","year":"2014","journal-title":"Int. J. Adapt. Resilient Auton. Syst. (IJARAS)"},{"key":"ref_30","doi-asserted-by":"crossref","first-page":"1603","DOI":"10.1007\/s10586-020-03080-8","article-title":"Formalizing and simulating cross-layer elasticity strategies in Cloud systems","volume":"23","author":"Khebbeb","year":"2020","journal-title":"Clust. Comput."},{"key":"ref_31","doi-asserted-by":"crossref","first-page":"395","DOI":"10.3233\/MGS-170277","article-title":"A formal framework for organization-centered multi-agent system specification: A rewriting logic based approach","volume":"13","author":"Laouadi","year":"2017","journal-title":"Multiagent Grid Syst."},{"key":"ref_32","doi-asserted-by":"crossref","unstructured":"Metelo, A., Braga, C., and Brand\u00e3o, D. (2018, January 2\u20135). Towards the modular specification and validation of cyber-physical systems. Proceedings of the International Conference on Computational Science and Its Applications, Melbourne, Australia.","DOI":"10.1007\/978-3-319-95162-1_6"},{"key":"ref_33","doi-asserted-by":"crossref","unstructured":"Fadlisyah, M., and \u00d6lveczky, P.C. (2013, January 3\u20136). The HI-Maude tool. Proceedings of the International Conference on Algebra and Coalgebra in Computer Science, Warsaw, Polan.","DOI":"10.1007\/978-3-642-40206-7_25"},{"key":"ref_34","unstructured":"\u00d6lveczky, P.C. (2022, January 12). Real-Time Maude 2.3 Manual. Available online: http:\/\/urn.nb.no\/URN:NBN:no-35645."},{"key":"ref_35","doi-asserted-by":"crossref","first-page":"3324","DOI":"10.1002\/sec.1537","article-title":"Modelling of Internet of Things units for estimating security-energy-performance relationships for quality of service and environment awareness","volume":"9","author":"Venckauskas","year":"2016","journal-title":"Secur. Commun. Netw."},{"key":"ref_36","doi-asserted-by":"crossref","unstructured":"Mutlag, A.A., Ghani, M.K.A., Mohammed, M.A., Lakhan, A., Mohd, O., Abdulkareem, K.H., and Garcia-Zapirain, B. (2021). Multi-Agent Systems in Fog\u2013Cloud Computing for Critical Healthcare Task Management Model (CHTM) Used for ECG Monitoring. Sensors, 21.","DOI":"10.3390\/s21206923"},{"key":"ref_37","doi-asserted-by":"crossref","first-page":"102674","DOI":"10.1016\/j.jnca.2020.102674","article-title":"QoS-aware service provisioning in fog computing","volume":"165","author":"Murtaza","year":"2020","journal-title":"J. Netw. Comput. Appl."},{"key":"ref_38","doi-asserted-by":"crossref","first-page":"447","DOI":"10.1109\/TNSE.2020.3040215","article-title":"An Efficient Formal Modeling Framework for Hybrid Cloud-Fog Systems","volume":"8","author":"Chen","year":"2020","journal-title":"IEEE Trans. Netw. Sci. Eng."},{"key":"ref_39","doi-asserted-by":"crossref","first-page":"5057","DOI":"10.1109\/JSYST.2020.3022244","article-title":"Fog-centric authenticated key agreement scheme without trusted parties","volume":"15","author":"Guo","year":"2020","journal-title":"IEEE Syst. J."},{"key":"ref_40","doi-asserted-by":"crossref","unstructured":"Sahli, H., Ledoux, T., and Rutten, \u00c9. (2019, January 16\u201320). Modeling self-adaptive fog systems using bigraphs. Proceedings of the International Conference on Software Engineering and Formal Methods, Oslo, Norway.","DOI":"10.1007\/978-3-030-57506-9_19"},{"key":"ref_41","doi-asserted-by":"crossref","first-page":"51","DOI":"10.4018\/IJOCI.2021040103","article-title":"A Formal Framework for Secure Fog Architectures: Application to Guarantee Reliability and Availability","volume":"11","author":"Benzadri","year":"2021","journal-title":"Int. J. Organ. Collect. Intell. (IJOCI)"},{"key":"ref_42","doi-asserted-by":"crossref","first-page":"101821","DOI":"10.1016\/j.sysarc.2020.101821","article-title":"A maude-based rewriting approach to model and verify cloud\/fog self-adaptation and orchestration","volume":"110","author":"Khebbeb","year":"2020","journal-title":"J. Syst. Archit."},{"key":"ref_43","doi-asserted-by":"crossref","first-page":"27132","DOI":"10.1109\/ACCESS.2017.2766180","article-title":"Fog computing over IoT: A secure deployment and formal verification","volume":"5","author":"Zahra","year":"2017","journal-title":"IEEE Access"}],"container-title":["Future Internet"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.mdpi.com\/1999-5903\/14\/2\/52\/pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,10,10]],"date-time":"2025-10-10T22:16:44Z","timestamp":1760134604000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.mdpi.com\/1999-5903\/14\/2\/52"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022,2,9]]},"references-count":43,"journal-issue":{"issue":"2","published-online":{"date-parts":[[2022,2]]}},"alternative-id":["fi14020052"],"URL":"https:\/\/doi.org\/10.3390\/fi14020052","relation":{},"ISSN":["1999-5903"],"issn-type":[{"value":"1999-5903","type":"electronic"}],"subject":[],"published":{"date-parts":[[2022,2,9]]}}}