Denotational and Algebraic Semantics for the CaIT Calculus

The Internet of Things (IoT) has been wildly used in various fields of our lives, such as health care, smart environment, transportation, etc. However, the existing research on IoT mainly concentrates on its practical applications, and there is still a lack of work on modelling and reasoning about IoT systems from the perspective of formal methods. Therefore, the Calculus of the Internet of Things (CaIT) has been proposed to model the interactions among components and verify the network deployment to ensure the quality and reliability of IoT systems. Unfortunately, the CaIT calculus can only support point-to-point communication, while broadcast communication is more common in IoT systems. Therefore, this paper updates the CaIT calculus by replacing its communication primitive with the broadcast. Based on the Unifying Theories of Programming (UTP), we further explore its denotational semantics and algebraic semantics, with a special focus on broadcast communication, actions with the timeout (e.g. input actions and migration actions), and channel restriction. To facilitate the algebraic exploration of parallel expansion laws, we further extend the CaIT calculus with a new concept called guarded choice, which allows us to transform each program into the guarded choice form.