(Timed) Function

 
 A function assigns values of one domain to values of another domain. In the following example the function tempVal represents the value delivered by a temperature sensor at a specific time point. This means that the function tempVal assigns to each time point a value of the domain TEMP.

Most of the functions used in a problem specification concerning reactive systems represent phenomena that evolve over time, as for example the delivered value of a temperature sensor. In order not to have to mention always explicitly the domain TIME, such functions are called timed functions. Thus, in the following example Timed Function tempVal $() \rightarrow$ TEMP is an abbreviation for Function tempVal $(\mathit{TIME}) \rightarrow$ TEMP.

Example: Timed Function

The entry in the field Intention explains the phenomenon represented by this designation.

To understand the entry in the field Scope some remarks are necessary. We suppose that a system can be split into the environment and the machine. The environment is the part of a system that already exists. Installed sensors or physical phenomena such a the temperature in a room belong to the environment. The machine is the part of a system that still has to be developed. An algorithm computing the settings of radiator valves for example belongs to the machine.

We suppose that each phenomenon is controlled by exactly one of these two parts. Control means that this part of the system controls the (not-) changing of a phenomenon. A phenomenon that is controlled by one of the two parts is also visible for this part. For the not controlling part a phenomenon can but do not have to be visible.

For example, the temperature in a room is controlled by the environment and is not visible for the machine. If a temperature sensor is already installed in the room, the value delivered by this sensor is also controlled by the environment but it is also visible for the machine. A radiator valve that is already installed in the room is normally controlled by the machine and visible for the machine. Values that the machine computes are phenomena controlled by the machine and which are not visible for the environment. Such phenomena are only allowed in a problem specification if they are explicitly introduced by the customer.

Due to this classification (control and visibility) one of the following four scopes is assigned to every phenomenon and by this to each function (and also to each predicate, cf. Section 2.1.2.4) representing a phenomenon:

• environment controlled, not visible (hidden) for the machine (eh)
• environment controlled, visible for the machine (ev)
• machine controlled, not visible (hidden) for the environment (mh)
• machine controlled, visible for the environment (mv)