INTENTION
This class provides all definitions to describe the behavior of an actuator if it has a malfunction.
The facility manager as well as the user are informed about a malfunction.
SIGNATURE
Time Constant | TinfDelay |
---|
Intention | : | This time constant represents the maximal delay between an important event concerning this actuator a user or the facility manager has to be informed about (e.g. a malfunction or the repair of a malfunction) and the time point the user or the facility manager is informed. |
Scope | : | ev |
Prereferences | : | pdref U11 |
pdref FM7 | ||
Postreferences | : | rsref MalfunctionActuator : R_MA3 |
rsref MalfunctionActuator : R_MA4 | ||
rsref MalfunctionActuator : R_MA5 | ||
rsref MalfunctionActuator : R_MA6 |
Time Constant | Tinfo |
---|
Intention | : | This time constant represents the maximal time span a user or the facility manager is informed about an important event concerning this actuator. |
Scope | : | ev |
Prereferences | : | pdref U11 |
pdref FM7 | ||
Postreferences | : | rsref MalfunctionActuator : R_MA1 |
rsref MalfunctionActuator : R_MA2 |
Timed Predicate | malDetEnv |
---|
Intention | : | This predicate is true iff the actuator existing in the real world has a malfunction. Note that this predicate represents the value as it exists in the real world. This value is not visible for the machine. |
Scope | : | eh |
Prereferences | : | pdref PD_13 |
Timed Predicate | malDetMach |
---|
Intention | : | This predicate is true iff the machine assumes that the actuator existing in the real world has a malfunction. Note that this predicate represents the value as it seen by the machine. |
Scope | : | mh |
Prereferences | : | pdref PD_13 |
Postreferences | : | msref Actuator : M_A1 |
rsref MalfunctionActuator : R_MA3 | ||
rsref MalfunctionActuator : R_MA4 | ||
rsref MalfunctionActuator : R_MA5 | ||
rsref MalfunctionActuator : R_MA6 |
Timed Predicate | FMInformed |
---|
Intention | : | This predicate is true iff the facility manager is informed about an important event concerning this actuator. An important event is either the detection of a malfunction of the actuator or that a malfunction of the actuator has been repaired.
The facility manager has to be informed by sending an email. |
Scope | : | eh |
Prereferences | : | pdref FM7 |
Postreferences | : | rsref MalfunctionActuator : I_MA2 |
rsref MalfunctionActuator : R_MA2 | ||
rsref MalfunctionActuator : R_MA4 | ||
rsref MalfunctionActuator : R_MA6 |
Timed Predicate | userInformed |
---|
Intention | : | This predicate is true iff the user is informed about an important event concerning this actuator. An important event is either the detection of a malfunction of the actuator or that a malfunction of the actuator has been repaired.
The user has to be informed by sending an email. |
Scope | : | eh |
Prereferences | : | pdref U11 |
Postreferences | : | rsref MalfunctionActuator : I_MA1 |
rsref MalfunctionActuator : R_MA1 | ||
rsref MalfunctionActuator : R_MA3 | ||
rsref MalfunctionActuator : R_MA5 |
Property | I_MA1 |
---|
Formal | : | userInformed |
NL | : | Initially the user is not informed about an important event concerning this actuator. |
Property | I_MA2 |
---|
Formal | : | FMInformed |
NL | : | Initially the facility manager is not informed about an important event concerning this actuator. |
Property | R_MA1 |
---|
Formal | : | ( [ userInformed ] Tinfo userInformed ) |
NL | : | Whenever a user becomes informed he is informed for at most milliseconds. By this requirement it is expressed, that the user is not informed permanently, but that the information is a kind of signal, e.g. an email. |
Prereferences | : | pdref U11 |
Property | R_MA2 |
---|
Formal | : | ( [ FMInformed ] Tinfo FMInformed ) |
NL | : | Whenever the facility manager becomes informed he is informed for at most milliseconds. By this requirement it is expressed, that the facility manager is not informed permanently, but that the information is a kind of signal, e.g. an email. |
Prereferences | : | pdref FM7 |
Property | R_MA3 |
---|
Formal | : | ( [ malDetMach ] TinfDelay userInformed ) |
NL | : | Whenever the machine assumes that a malfunction of the actuator has occurred, the user is informed about this within milliseconds. |
Prereferences | : | pdref U11 |
Property | R_MA4 |
---|
Formal | : | ( [ malDetMach ] TinfDelay FMInformed ) |
NL | : | Whenever the machine assumes that a malfunction of the actuator has occurred, the facility manager is informed about this within milliseconds. |
Prereferences | : | pdref FM7 |
Property | R_MA5 |
---|
Formal | : | ( [ malDetMach ] TinfDelay userInformed ) |
NL | : | Whenever the machine assumes that the actuator is working correctly again after it has had a malfunction, the user is informed about this within milliseconds. |
Prereferences | : | pdref U11 |
Property | R_MA6 |
---|
Formal | : | ( [ malDetMach ] TinfDelay FMInformed ) |
NL | : | Whenever the machine assumes that the actuator is working correctly again after it has had a malfunction, the facility manager is informed about this within milliseconds. |
Prereferences | : | pdref FM7 |