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 |
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 |
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 |
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 |
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 |
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 |
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. |
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. |
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. |
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. |
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. |
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. |