Description Class EnteredValue

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

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

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

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

REQUIREMENT SPECIFICATIONS

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.