Abstract
Process algebra can be considered to be one of the best methods to model IoT systems since it can represent the main properties of things in the systems: communication, movements, deadlines, etc. The best known algebras are π-calculus and mobile ambient. However, there are some limitations to model the different types of movements of the things with secure requirements. π-calculus passes the name of ports for indirect movements unrealistically, and mobile ambient uses ambient to synchronize asynchronous movements forcefully and unnaturally. This paper presents new process algebra, called δ-calculus, to model the different types of such synchronous movements for the things in IoT over some target geographical space. A process can be nested in another process, and their configuration will be changed by these movements. Any violation of the secure movements can be detected and prevented by the properties of the movements: synchrony, priority and deadline. To demonstrate the feasibility, a tool, called SAVE, was developed on the ADOxx metamodeling platform with an emergency medical system, which is one of the best suitable application domains for IoT.
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
Whitmore, A., Agarwal, A., Xu, L.D.: The internet of things—a survey of topics and trends. Inf. Syst. Front. 17(2), 261–274 (2015)
Larcom, B.: Secure Requirement. https://www.frisc.no/arrangementer/finse-winter-school-2014/ (2014)
Heitmeyer, C., Mandrioli, D.: Formal Methods for Real-Time Computing: An Overview, Formal Methods for Real-Time Computing, pp. 1–32. Wiley (1996)
Milner, R., Parrow, J., Walker, D.: A calculus of mobile processes (i-ii). Inf. Comput. 100, 1–77 (1992)
Cardelli, L., Gordon, A.: Mobile ambients. In: Nivat, M. (ed.) ETAPS 1998 and FOSSACS 1998, LNCS, vol. 1378, pp. 140–155. Springer, Heidelberg (1998)
Lin, H.: Predicate μ-calculus for mobile ambients. J. Comput. Sci. Technol. 20(1), 95–104 (2005)
Milner, R.: A Calculus of Communicating Systems. Springer, New York (1982)
Choe, Y., Lee, M.: δ-calculus: process algebra to model secure movements of distributed mobile processes in real-time business application. In: 23rd European Conference on Information Systems (2015)
Clarke, E.M., Emerson, E.A.: Design and synthesis of synchronization skeletons using branching-time temporal logic. In: Kozen, D. (ed.) Proceedings of the Workshop on Logic of Programs, Yorktown Heights, vol. 131 of Lecture Notes in Computer Science, pp. 52–71. Springer (1981)
Choe, Y., Choi, W., Jeon, G., Lee, M.: A Tool for Visual Specification and Verification for Secure Process Movements, eChallenges e-2015, Nov 2015
Fill, H., Karagiannis, D.: On the conceptualisation of modelling methods using the ADOxx meta modelling platform. Enterp. Modell. Inf. Syst. Arch. 8(1), 4–25 (2013)
Choi, W., Choe, Y., Lee, M.: A reduction method for process and system complexity with conjunctive and complement choices in a process algebra. In: IEEE 39th Annual International Computer, Software and Applications Conference (2015)
Acknowledgments
This work was supported by Basic Science Research Programs through the National Research Foundation of Korea (NRF) funded by the Ministry of Education (2010-0023787), and the MISP (Ministry of Science, ICT and Future Planning), Korea, under the ITRC (Information Technology Research Centre) support program (IITP-2015-H8501-15-1012) supervised by the IITP (Institute for Information & Communications Technology Promotion), and Space Core Technology Development Program through the NRF (National Research Foundation of Korea) funded by the Ministry of Science, ICT and Future Planning (NRF-2014M1A3A3A02034792), and Basic Science Research Program through the National Research Foundation of Korea (NRF) funded by the Ministry of Education (NRF-2015R1D1A3A01019282).
Tool Download http://www.omilab.org/save.
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2016 Springer International Publishing Switzerland
About this chapter
Cite this chapter
Choe, Y., Lee, M. (2016). Algebraic Method to Model Secure IoT. In: Karagiannis, D., Mayr, H., Mylopoulos, J. (eds) Domain-Specific Conceptual Modeling. Springer, Cham. https://doi.org/10.1007/978-3-319-39417-6_15
Download citation
DOI: https://doi.org/10.1007/978-3-319-39417-6_15
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-39416-9
Online ISBN: 978-3-319-39417-6
eBook Packages: Computer ScienceComputer Science (R0)