@inbook{4aa986cf0f4943e3a5f548a644f58439,
title = "Denotational and Algebraic Semantics for the SMrCaIT Calculus Based on UTP",
abstract = "The rapid development of the Internet of Things (IoT) has generated a global demand for related technologies, especially in improving system quality and security. In response, our recent work proposes SMrCaIT, a secure mobile real-time process calculus explicitly designed for IoT systems. Using SMrCaIT, we can model and verify IoT systems before implementation, enhancing system reliability and security. To provide a rigorous mathematical explanation of the meaning of the SMrCaIT program and explore its properties, this paper gives the denotational and algebraic semantics of this calculus based on the Unifying Theories of Programming (UTP). To facilitate the algebraic exploration of parallel expansion laws, we extend the SMrCaIT calculus with three types of guarded choices, allowing us to convert any SMrCaIT program into a unified form (i.e., a guarded choice form).",
keywords = "Algebraic Semantics, Denotational semantics, IoT, SMrCaIT calculus, UTP",
author = "Ningning Chen and Huibiao Zhu and Jifeng He",
note = "Publisher Copyright: {\textcopyright} The Author(s), under exclusive license to Springer Nature Switzerland AG 2024.",
year = "2024",
doi = "10.1007/978-3-031-67114-2\_1",
language = "英语",
series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",
publisher = "Springer Science and Business Media Deutschland GmbH",
pages = "1--21",
booktitle = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",
address = "德国",
}