The Airco example consists of a cooling device and a fan. A temperature sensor measures the current temperature. It can also be instructed to inform the controller when the temperature raises above a certain value or drops below a certain value. The user can change the target temperature causing the cooler to start or stop immediately. The fan can be controlled independently to operate at either a low level or a high level. The user settings are stored in non-volatile memory (nvm) when the airco is switched off, and they are restored when it is switched on.
The controller has an orthogonal statemachine with 2 regions for the cooler and for the fan. Due to the asynchronous triggers of the temperature sensor, the controller must have its own thread.
A special remark is made about the nvm component. It exports some simple set and get functions, so that a stateless protocol suffices. However, for the purpose of verification the server role has a protocol state machine causing a (harmless) consistency error, that is reported as remark 2330. The PSM can return 2 different target temperatures serving as input to the controller. In this way, all possible execution scenarios can be generated during a verification process.
Several UML diagrams of this example are shown at Modeling / Screenshots. The state machine of the cooling mechanism, the heart of the airco, is shown below:
Valid combinations for generating source code are in the table below.
|
Target |
Generate |
|
Protocols |
|
|
AircoProtocol |
Simulation code, Verification code |
|
CoolerProtocol |
none |
|
FanProtocol |
Simulation code, Verification code |
|
NvmProtocol |
Simulation code, Verification code |
|
SensorProtocol |
Simulation code, Verification code |
|
Architecture |
|
|
ExecEnv |
Simulation code, Verification code |
The file TismSds.html contains an overview of the verification scenarios.
The files in the tables below are free to download.
| Airco.xml | The XMI file of the Airconditioning UML model. |
| Airco.tsm | The project file for the TismTool. |
| AircoTranslations.tsl |
The translation table. |
| Airco.pdf | The UML diagrams. |
| Airco.zip | The zipped archive containing the (generated) source code, the verification executable, and the logfiles TismLog_0001.txt and TismSeq_0001.txt. |
| AircoScript.pdf | The script for modeling 'Airco.xml' using MagicDraw. |
| AllAirco.zip | All the above files zipped together. |
| Airco.xml |
The XMI file of the Airconditioning UML model. |
| Airco_Java.tsm |
The project file for the TismTool. |
| AircoTranslations_Java.tsl |
The translation table. |
| Airco.pdf |
The UML diagrams. |
| Airco_Java.zip |
The zipped archive containing the (generated) source code, the verification executable jar file, and the logfiles TismLog_0001.txt and TismSeq_0001.txt. |
| AircoScript.pdf |
The script for modeling 'Airco.xml' using MagicDraw. |
| AllAirco_Java.zip |
All the above files zipped together. |
| Airco.xml |
The XMI file of the Airconditioning UML model. |
| Airco_Cpp.tsm |
The project file for the TismTool. |
| AircoTranslations_Cpp.tsl |
The translation table. |
| Airco.pdf |
The UML diagrams. |
| Airco_Cpp.zip |
The zipped archive containing the (generated) source code, the verification executable, and the logfiles TismLog_0001.txt and TismSeq_0001.txt. The used C++ Boost library has version 1.48 . |
| AircoScript.pdf |
The script for modeling 'Airco.xml' using MagicDraw. |
| AllAirco_Cpp.zip |
All the above files zipped together. |
| L_AIRCO_CPP.tar.gz |
The tar-zipped archive containing the (generated) source code, the makefiles, the verification executable, and the logfiles TismLog_0001.txt and TismSeq_0001.txt. The used C++ Boost library has version 1.47 . |
| L_AllAIRCO_CPP.tar.gz | The tar-zipped archive containing the XMI file of the Airconditioning UML model, TismTool project file, the translation table, pdf of UML diagrams, and the above L_AIRCO_CPP.tar.gz file. |
| Airco.xml |
The XMI file of the Airconditioning UML model. |
| Airco_C.tsm |
The project file for the TismTool. |
| AircoTranslations_C.tsl |
The translation table. |
| Airco.pdf |
The UML diagrams. |
| Airco_C.zip |
The zipped archive containing the (generated) source code, the verification executable, and the logfiles TismLog_0001.txt and TismSeq_0001.txt. The used OSAL library is based on Windows. |
| AircoScript.pdf |
The script for modeling 'Airco.xml' using MagicDraw. |
| AllAirco_C.zip |
All the above files zipped together. |
| L_AIRCO_C.tar.gz |
The tar-zipped archive containing the (generated) source code, the makefiles, the verification executable, and the logfiles TismLog_0001.txt and TismSeq_0001.txt. The used OSAL library is based on Linux. |
| L_AllAIRCO_C.tar.gz |
The tar-zipped archive containing the XMI file of the Airconditioning UML model, TismTool project file, the translation table, pdf of UML diagrams, and the above L_AIRCO_C.tar.gz file. |
TismTool reports the following remarks about the UML model:
W 5090: Trigger 'Operation' preferred over 'Name' @ ( Xmi > Data > Protocols > CoolerProtocol > Stop() )
W 2330: No FSM @ ( Xmi > Data > Protocols > NvmProtocol > NvmClient )
I 4360: Informal guard "low level" becomes 'true' @ ( Xmi > Data > Protocols > AircoProtocol > AircoServer > AircoServerPsm >> Active > Fan > ChoiceState )
I 4360: Informal guard "cold" becomes 'true' @ ( Xmi > Data > Protocols > SensorProtocol > SensorServer > SensorServerPsm >> Outer >> ChoiceState )
I 4360: Informal guard "low level" becomes 'true' @ ( Xmi > Data > Protocols > NvmProtocol > NvmServer > NvmServerFsm >> ChoiceState )
I 4360: Informal guard "low target" becomes 'true' @ ( Xmi > Data > Protocols > NvmProtocol > NvmServer > NvmServerFsm >> ChoiceState )
W 4535: Self-transition is errorprone for NativeTrigger @ ( Xmi > Data > Protocols > AircoProtocol > AircoClient > AircoClientPsm >> Active > Cooler > Outer )
W 4535: Self-transition is errorprone for NativeTrigger @ ( Xmi > Data > Protocols > AircoProtocol > AircoClient > AircoClientPsm >> Active > Cooler > Outer >> Idle )
W 4535: Self-transition is errorprone for NativeTrigger @ ( Xmi > Data > Protocols > SensorProtocol > SensorClient > SensorClientPsm >> Outer )
ad W 5090:
In the CoolerServerPsm the trigger of the transition from Busy to
Idle is defined in 2 ways: via the Name field, and also via the
Operation field. In such a case TismTool prefers the Operation field.
ad W 2330:
A Protocol State Machine for the NvmClient is not needed because of
absence of state behaviour. The severe (but harmless) message is given
since the peer, NvmServer, has a Protocol State Machine. The NvmServer
is used as Mock in the verification of the Airco system. The different
return values of the transitions guarantee that all possible scenarios
will be generated.
ad I 4360:
Informal guards are translated to source code depending on the purpose.
For verification/simulation the guard becomes a condition that is
dynamically true of false to generate all possible scenarios.
Generating application code for a protocol is not very meaningful, and
the guard becomes always 'true'.
ad I 4535:
Self-transitions may cause an unlimited number of messages to a
receiver causing queue overflow.
By downloading and/or using the above items you accept the terms of the Disclaimer. So make sure you have read it before downloading or using anything from this section of the site. In general terms that means you use them at your own risk, and we accept NO RESPONSIBILITY WHATSOEVER for anything that may occur as a result of your use of, or inability to use, any item provided via these pages.