Yet another real-time specification for the steam boiler: Local clocks to statically measure systems performance

In this paper we apply a new real-time modeling to the well-known Steam Boiler case study. The novelty of our approach is in explicitly representing the various system components, i. e. hardware sensors, software controllers and so on, with separate local clocks. The aim of our approach is to be able to statically analyze the global system specification taking into account the relative speed of each system components. For example, we can statically verify if, and how changing the local speed of a component can affect the global performance of the system. Component behaviors are specified by means of a simple process algebra. Local clocks are modeled as higher order terms in a given signature, and unification is used to define the common clock. Then an operational semantics defines which transitions a process can perform and which transitions let time to elapse.