INTENTION
This class provides all definitions to describe the entering of a value using an appropriate device (in our case this device is a control panel). For a value e that is entered (expressed by the function entered) a value c (expressed by the function checked) is determined using the function nearestValue. This function is intended to check the entered value e whether it is an allowed value and returns the value which is nearest to e.
It is assumed that the entered value can not be seen by the machine, i.e. there exists up to now no possibility to enter the value. Hence, the development of such a device is part of the overall development of the system. In our case this is the control panel, which still has to be developed. Therefore the timed function entered has the scope eh.
FORMAL PARAMETERS
| Sort | CHECKED_DOM |
|---|
| Intention | : | This domain contains the values that can be produced out of an entered value using the function nearestValue. |
SIGNATURE
| Timed Function | entered  STRING |
|---|
| Intention | : | This function represents the value entered by a person. The value is represented as a string. |
| Scope | : | eh |
| Postreferences | : | rsref EnteredValue : R_EV1 |
| Timed Function | checked CHECKED_DOM |
|---|
| Intention | : | This function represents the value decided by the machine to use. checked is determined out of entered using the function nearestValue. |
| Scope | : | mh |
| Postreferences | : | msref MalfunctionSensor : M_MS1 |
| msref Sensor : M_S1 | ||
| msref Actuator : M_A1 | ||
| msref AreaLightCtrlPanelFM : I_LCPFM1 | ||
| msref AreaLightCtrlPanelFM : I_LCPFM2 | ||
| msref RoomLightCtrlPanelFM : I_LCPR1 | ||
| msref RoomLightCtrlPanelFM : M_LCPR1 | ||
| msref MalfunctionOccupancy : M_MO1 | ||
| msref Occupancy : M_OCC1 | ||
| msref AreaLight : M_AL5 | ||
| msref RoomLight : M_RL2 | ||
| msref RoomLight : M_RL3 | ||
| msref RoomLight : M_RL4 | ||
| msref RoomLight : M_RL5 | ||
| msref RoomLight : M_RL6 | ||
| msref RoomLight : M_RL7 | ||
| msref RoomLight : M_RL8 | ||
| msref RoomLight : M_RL9 | ||
| msref RoomLight : M_RL10 | ||
| msref RoomLight : M_RL12 | ||
| msref RoomLight : M_RL13 | ||
| msref RoomLight : M_RL14 | ||
| rsref EnteredValue : R_EV1 | ||
| rsref AreaLight : R_AL1 |
| Timed Function | nearestValue : STRING CHECKED_DOM |
|---|
| Intention | : | This function returns the value which is the nearest one in the domain CHECKED_DOM w.r.t. the first argument. |
| Scope | : | mh |
| Postreferences | : | rsref EnteredValue : R_EV1 |
| Timed Function | checkTime TIME |
|---|
| Intention | : | This function represents the time needed to check a value, entered by a person, using the function nearestValue. |
| Scope | : | mh |
| Postreferences | : | rsref EnteredValue : R_EV1 |
| Property | R_EV1 |
|---|
| Formal | : |  ( entered  checkTime nearestValue checked) |
| NL | : | The checked value is always derived from the entered value using the function nearestValue. A change of the entered value is always propagated within the time checkTime. |