A UTP Refinement Model of the STeC Language

The Internet of Things (IoT) and Cyber-Physical Systems (CPS) are new trends of real-time systems in the area of information technology. The consistency between time and location is a basic feature of IoT and CPS. Such spatial-temporal consistency means that an agent arrives at the required location at the required time and finishes the required tasks within the required time. In order to describe the requirement of spatial and temporal consistency of cyber-physical systems, a specification language called STeC was proposed by Chen in 2012 [1]. This paper will focus on formalising the refinement of STeC programs using the UTP methods. For the STeC language, algebraic refinement, denotational refinement and operational refinement are introduced based on He's presentation on a new roadmap of linking theories of programming. The equivalence among these three kinds of refinement is given.