Denotational and Algebraic Semantics for the SMrCaIT Calculus Based on UTP

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