Demo MediaPlayer

The MediaPlayer is a typical controller component in consumer equipment for playback of multimedia data. It coordinates reading of the data from a storage medium and presentation on a display device. The user selects a title from the available material and starts playback. The controller retrieves file information from a title database and starts the reading device. When sufficient data have been read and buffered, then the display device is started. Buffering is needed to prevent data underflow. The user is able to pause and continue the presentation. For the sake of convenience, no other trick modes are implemented. The controlled devices can report errors, for example because of unreadable DVD discs due to fingerprints or scratches or because of improperly authored data streams with e.g. too high bitrates. The controller is able to recover from such anomalies: it stops playback, reports the error to the title database, and then restarts playback at a suitable position. In case of too many errors, title playback stops and the user is informed. The error recovery feature introduces a lot of complexity in the controller's behaviour. Therefore, the transaction mechanism is applied for the realisation of the controller.

The MediaPlayer is decomposed in 3 parts: the BackEnd and 2 proxy components called ProxyReader and ProxyDisplay. The top level finite state machines of BackEnd and ProxyDisplay are shown below.

MediaPlayer Backend FSM

MediaPlayer ProxyDisplayFSM

The UML design model is fairly elaborate consisting of 7 concurrent state machines, 277 (super)states, 376 transitions, and more than 10000 scenario steps.

Valid combinations for generating source code are in the table below.

Target

Generate

Protocols


DisplayProtocol

Simulation code, Verification code

PlayerProtocol

Simulation code, Verification code

ReaderProtocol

Simulation code, Verification code

TitlebaseProtocol

Simulation code, Verification code

Repository


Player


ProxyProtocols


ProxyDisplayProtocol

Simulation code, Verification code

ProxyReaderProtocol

Simulation code, Verification code

Architecture


ExecEnv

Simulation code, Verification code

The verification detects no errors. Because of the many scenario steps, no sequence diagrams have been generated.

The files in the tables below are free to download.

C# source code generation

MediaPlayer.xml The XMI file of the MediaPlayer UML model.
MediaPlayer.tsm The project file for the TismTool.
MpTranslations.tsl
The translation table.
MediaPlayer.pdf The UML diagrams.
MediaPlayer.zip The zipped archive containing the (generated) source code, the verification executable, and the logfiles TismLog_0001.txt and TismSeq_0001.txt.
AllMediaPlayer.zip All the above files zipped together.

Java source code generation

MediaPlayer.xml
The XMI file of the MediaPlayer UML model.
MediaPlayer_Java.tsm
The project file for the TismTool.
MpTranslations_Java.tsl
The translation table.
MediaPlayer.pdf
The UML diagrams.
MediaPlayer_Java.zip
The zipped archive containing the (generated) source code, the verification executable jar, and the logfiles TismLog_0001.txt and TismSeq_0001.txt.
AllMediaPlayer_Java.zip
All the above files zipped together.

C++ source code generation (Windows)

MediaPlayer_Cpp.xml
The XMI file of the MediaPlayer UML model.
MediaPlayer_Cpp.tsm
The project file for the TismTool.
MpTranslations_Cpp.tsl
The translation table.
MediaPlayer_Cpp.pdf
The UML diagrams.
MediaPlayer_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 .

AllMediaPlayer_Cpp.zip
All the above files zipped together.

C++ source code generation (Linux)

L_MEDIAPLAYER_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_AllMEDIAPLAYER_CPP.tar.gz The tar-zipped archive containing the XMI file of the MediaPlayer UML model, TismTool project file, the translation table, pdf of UML diagrams, and the above L_MEDIAPLAYER_CPP.tar.gz file.

C source code generation (Windows)

MediaPlayer_C.xml
The XMI file of the MediaPlayer UML model.
MediaPlayer_C.tsm
The project file for the TismTool.
MpTranslations_C.tsl
The translation table.
MediaPlayer_C.pdf
The UML diagrams.
MediaPlayer_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.

AllMediaPlayer_C.zip
All the above files zipped together.

C source code generation (Linux)

L_MEDIAPLAYER_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_AllMEDIAPLAYER_C.tar.gz
The tar-zipped archive containing the XMI file of the MediaPlayer UML model, TismTool project file, the translation table, pdf of UML diagrams, and the above L_MEDIAPLAYER_C.tar.gz file.

Discussion

TismTool reports the following remarks about the UML model:

W 5030: Effect 'Name' preferred over 'Operation' @ ( ProxyReaderClientPsm >> CompoundState >> Open ) => ( ProxyReaderClientPsm >> CompoundState >> Open )
W 5030: Effect 'Name' preferred over 'Operation' @ ( ReaderClientPsm >> CompoundState >> Open ) => ( ReaderClientPsm >> CompoundState >> Open )
W 5030: Effect 'Name' preferred over 'Operation' @ ( DisplayServerPsm >> Active >> Busy ) => ( DisplayServerPsm >> Active >> Synclost )
W 4570: Missing argument 'Sector' in trigger rp_reader->CbError() @ transition ( Xmi > Data > Repository > Player > Decomposition > ProxyReader > ProxyReader > ProxyReaderFsm >> Transition )
W 2800: Unused trigger rpp_reader___Px_CbOpened() @ ( Xmi > Data > Repository > Player > Decomposition > Backend > BackendClass > rpp_reader )
W 2800: Unused trigger rpp_reader___Px_CbStopped() @ ( Xmi > Data > Repository > Player > Decomposition > Backend > BackendClass > rpp_reader )
W 2800: Unused trigger rpp_reader___Px_CbClosed() @ ( Xmi > Data > Repository > Player > Decomposition > Backend > BackendClass > rpp_reader )
W 2800: Unused trigger rpp_reader___Px_CbReading() @ ( Xmi > Data > Repository > Player > Decomposition > Backend > BackendClass > rpp_reader )
W 2800: Unused trigger rpp_reader___Px_CbFilled() @ ( Xmi > Data > Repository > Player > Decomposition > Backend > BackendClass > rpp_reader )
W 2800: Unused trigger rpp_display___Px_CbContinued() @ ( Xmi > Data > Repository > Player > Decomposition > Backend > BackendClass > rpp_display )
W 2800: Unused trigger rpp_display___Px_CbPaused() @ ( Xmi > Data > Repository > Player > Decomposition > Backend > BackendClass > rpp_display )
W 2800: Unused trigger rpp_display___Px_CbPrepared() @ ( Xmi > Data > Repository > Player > Decomposition > Backend > BackendClass > rpp_display )
W 2800: Unused trigger rpp_display___Px_CbStarted() @ ( Xmi > Data > Repository > Player > Decomposition > Backend > BackendClass > rpp_display )
W 2800: Unused trigger rpp_display___Px_CbStopped() @ ( Xmi > Data > Repository > Player > Decomposition > Backend > BackendClass > rpp_display )
I 4360: Informal guard "ok" becomes 'true' @ ( Xmi > Data > Repository > Player > ProxyProtocols > ProxyDisplayProtocol > ProxyDisplayServer > ProxyDisplayServerPsm >> CompoundState >> CompoundState >> ChoiceState )
I 4360: Informal guard "ok" becomes 'true' @ ( Xmi > Data > Repository > Player > ProxyProtocols > ProxyReaderProtocol > ProxyReaderServer > ProxyReaderServerPsm >> Idle >> ChoiceState )
I 4360: Informal guard "ok" becomes 'true' @ ( Xmi > Data > Repository > Player > ProxyProtocols > ProxyReaderProtocol > ProxyReaderServer > ProxyReaderServerPsm >> CompoundState >> ChoiceState )
I 4360: Informal guard "ok" becomes 'true' @ ( Xmi > Data > Protocols > PlayerProtocol > PlayerServer > PlayerServerPsm >> ChoiceState )
I 4360: Informal guard "ok" becomes 'true' @ ( Xmi > Data > Protocols > ReaderProtocol > ReaderServer > ReaderServerPsm >> ChoiceState )
I 4360: Informal guard "ok" becomes 'true' @ ( Xmi > Data > Protocols > ReaderProtocol > ReaderServer > ReaderServerPsm >> CompoundState >> ChoiceState )
I 4360: Informal guard "valid TitleId" becomes 'true' @ ( Xmi > Data > Protocols > TitlebaseProtocol > TitlebaseServer > TbServerPsm >> ChoiceState )
I 4360: Informal guard "valid AtTime" becomes 'true' @ ( Xmi > Data > Protocols > TitlebaseProtocol > TitlebaseServer > TbServerPsm >> CompoundState >> ChoiceState )
I 4360: Informal guard "valid Chunk" becomes 'true' @ ( Xmi > Data > Protocols > TitlebaseProtocol > TitlebaseServer > TbServerPsm >> CompoundState >> ChoiceState )
I 4360: Informal guard "finished" becomes 'true' @ ( Xmi > Data > Protocols > TitlebaseProtocol > TitlebaseServer > TbServerPsm >> CompoundState >> ChoiceState )
W 4535: Self-transition is errorprone for NativeTrigger @ ( Xmi > Data > Repository > Player > ProxyProtocols > ProxyReaderProtocol > ProxyReaderClient > ProxyReaderClientPsm >> CompoundState >> Open )
W 4535: Self-transition is errorprone for NativeTrigger @ ( Xmi > Data > Protocols > ReaderProtocol > ReaderClient > ReaderClientPsm >> CompoundState >> Open )
W 4535: Self-transition is errorprone for NativeTrigger @ ( Xmi > Data > Protocols > TitlebaseProtocol > TitlebaseClient > TbClientPsm >> CompoundState >> Play )
W 4535: Self-transition is errorprone for NativeTrigger @ ( Xmi > Data > Protocols > TitlebaseProtocol > TitlebaseClient > TbClientPsm >> CompoundState >> Play )

ad W 5030:
If both the Name field and the Specification field of a trigger's Effect are specified, then the contents of the Name field is used.

ad W 4570:
The missing argument 'Sector' of trigger rp_reader->CbError() in state Stopping does not harm, since the trigger is ignored.

ad W 2800:
These triggers are not explicitly mentioned, because the AnyReceiveEvent takes care of the execution of the triggers.

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 W 4535:
Self-transitions may cause an unlimited number of messages to a receiver causing queue overflow.

Verification ProxyReaderProtocol:

============================================================
@ state: ( ProxyReaderProtocol > InsProxyReaderServer > ProxyReaderServerPsm >> Opening )
Unvisited transition: ( ProxyReaderServerPsm >> Opening ) => ( ProxyReaderServerPsm >> Opening ) : 'ProxyNok' Px_Stop


The proxy server accepts the trigger Px_Stop() in the Opening state to satisfy a possible caller.
However, the modeled proxy client has no need to call this trigger.

Verification ExEnv:

============================================================
@ state: ( ExEnv > Player > PlayerProxyDisplay > implementation > ProxyDisplayFsm >> Active >> Busy >> Pausing )
Unvisited transition: ( ProxyDisplayFsm >> Active >> Busy >> Pausing ) => ( ProxyDisplayFsm >> Active >> Busy >> Pausing ) : 'ProxyNok' ppp_display->Px_Pause


The Display proxy component accepts the possible triggers from the Backend in those states, where a request is still being processed by the lower level DisplayMock component. However, the Backend has no need to call Px_Pause() in the Pausing state. A similar remark holds for the 4 unvisited transitions below.

============================================================
@ state: ( ExEnv > Player > PlayerProxyDisplay > implementation > ProxyDisplayFsm >> Active >> Busy >> Continuing )
Unvisited transition: ( ProxyDisplayFsm >> Active >> Busy >> Continuing ) => ( ProxyDisplayFsm >> Active >> Busy >> Continuing ) : 'ProxyNok' ppp_display->Px_Continue

============================================================
@ state: ( ExEnv > Player > PlayerProxyDisplay > implementation > ProxyDisplayFsm >> Active >> Preparing )
Unvisited transition: ( ProxyDisplayFsm >> Active >> Preparing ) => ( ProxyDisplayFsm >> Active >> Preparing ) : 'ProxyNok' ppp_display->Px_Prepare

============================================================
@ state: ( ExEnv > Player > PlayerProxyDisplay > implementation > ProxyDisplayFsm >> Active >> Starting )
Unvisited transition: ( ProxyDisplayFsm >> Active >> Starting ) => ( ProxyDisplayFsm >> Active >> Starting ) : 'ProxyNok' ppp_display->Px_Start

============================================================
@ state: ( ExEnv > Player > PlayerProxyDisplay > implementation > ProxyDisplayFsm >> Active >> StartPausing )
Unvisited transition: ( ProxyDisplayFsm >> Active >> StartPausing ) => ( ProxyDisplayFsm >> Active >> StartPausing ) : 'ProxyNok' ppp_display->Px_Pause


============================================================
@ state: ( ExEnv > Player > PlayerProxyReader > implementation > ProxyReaderFsm >> Opening )
Unvisited transition: ( ProxyReaderFsm >> Opening ) => ( ProxyReaderFsm >> Opening ) : 'ProxyNok' ppp_reader->Px_Open


The Reader proxy component accepts the possible triggers from the Backend in those states, where a request is still being processed by the lower level ReaderMock component. However, the Backend has no need to call Px_Open() in the Opening state.
A similar remark holds for the 3 unvisited transitions below.

============================================================
@ state: ( ExEnv > Player > PlayerProxyReader > implementation > ProxyReaderFsm >> Opening )
Unvisited transition: ( ProxyReaderFsm >> Opening ) => ( ProxyReaderFsm >> Opening ) : 'ProxyNok' ppp_reader->Px_Close

============================================================
@ state: ( ExEnv > Player > PlayerProxyReader > implementation > ProxyReaderFsm >> Closing )
Unvisited transition: ( ProxyReaderFsm >> Closing ) => ( ProxyReaderFsm >> Closing ) : 'ProxyNok' ppp_reader->Px_Close

============================================================
@ state: ( ExEnv > Player > PlayerProxyReader > implementation > ProxyReaderFsm >> Seeking )
Unvisited transition: ( ProxyReaderFsm >> Seeking ) => ( ProxyReaderFsm >> Seeking ) : 'ProxyNok' ppp_reader->Px_Read

============================================================
@ state: ( ExEnv > UserMock > InsPlayerClient > PlayerClientPsm >> Active >> Running >> Busy >> ChoiceState )
Unvisited transition: ( PlayerClientPsm >> Active >> Running >> Busy >> ChoiceState ) => ( PlayerClientPsm >> Active >> Running >> Paused )


In the PlayerProtocol an event race can occur when the client calls Continue() in state Paused whereas the server has in the mean time made a transition from state Paused to state Error. If this happens then the client will make the above transition from ChoiceState to Paused.
The implementation of the Backend has a slightly different behaviour. In state Paused it would be strange to refresh the screen with a new image when a read error happens. Therefore, the occurrence of a read error is remembered in state Paused/ReadError. The error will be handled after receiving a Continue() request in state Continuing. The return value of Continue() is OK, because successful outcome of the request is still possible. So, the Backend satisfies a correct server role in the PlayerProtocol although it differs from the specified protocol server role.

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.

W 5030: Effect 'Name' preferred over 'Operation' @ ( ProxyReaderClientPsm >> CompoundState >> Open ) => ( ProxyReaderClientPsm >> CompoundState >> Open )
W 5090: Trigger 'Operation' preferred over 'Name' @ ( Xmi > Data > Protocols > ReaderProtocol > CbFilled )
W 5030: Effect 'Name' preferred over 'Operation' @ ( ReaderClientPsm >> CompoundState >> Open ) => ( ReaderClientPsm >> CompoundState >> Open )
W 5030: Effect 'Name' preferred over 'Operation' @ ( DisplayServerPsm >> Active >> Busy ) => ( DisplayServerPsm >> Active >> Synclost )
W 4570: Missing argument 'Sector' in trigger rp_reader->CbError() @ transition ( Xmi > Data > Repository > Player > Decomposition > ProxyReader > ProxyReader > ProxyReaderFsm >> Transition )
W 2800: Unused trigger rpp_reader___Px_CbOpened() @ ( Xmi > Data > Repository > Player > Decomposition > Backend > BackendClass > rpp_reader )
W 2800: Unused trigger rpp_reader___Px_CbStopped() @ ( Xmi > Data > Repository > Player > Decomposition > Backend > BackendClass > rpp_reader )
W 2800: Unused trigger rpp_reader___Px_CbClosed() @ ( Xmi > Data > Repository > Player > Decomposition > Backend > BackendClass > rpp_reader )
W 2800: Unused trigger rpp_reader___Px_CbReading() @ ( Xmi > Data > Repository > Player > Decomposition > Backend > BackendClass > rpp_reader )
W 2800: Unused trigger rpp_reader___Px_CbFilled() @ ( Xmi > Data > Repository > Player > Decomposition > Backend > BackendClass > rpp_reader )
W 2800: Unused trigger rpp_display___Px_CbContinued() @ ( Xmi > Data > Repository > Player > Decomposition > Backend > BackendClass > rpp_display )
W 2800: Unused trigger rpp_display___Px_CbPaused() @ ( Xmi > Data > Repository > Player > Decomposition > Backend > BackendClass > rpp_display )
W 2800: Unused trigger rpp_display___Px_CbPrepared() @ ( Xmi > Data > Repository > Player > Decomposition > Backend > BackendClass > rpp_display )
W 2800: Unused trigger rpp_display___Px_CbStarted() @ ( Xmi > Data > Repository > Player > Decomposition > Backend > BackendClass > rpp_display )
W 2800: Unused trigger rpp_display___Px_CbStopped() @ ( Xmi > Data > Repository > Player > Decomposition > Backend > BackendClass > rpp_display )
I 4360: Informal guard "ok" becomes 'true' @ ( Xmi > Data > Repository > Player > ProxyProtocols > ProxyDisplayProtocol > ProxyDisplayServer > ProxyDisplayServerPsm >> CompoundState >> CompoundState >> ChoiceState )
I 4360: Informal guard "ok" becomes 'true' @ ( Xmi > Data > Repository > Player > ProxyProtocols > ProxyReaderProtocol > ProxyReaderServer > ProxyReaderServerPsm >> Idle >> ChoiceState )
I 4360: Informal guard "ok" becomes 'true' @ ( Xmi > Data > Repository > Player > ProxyProtocols > ProxyReaderProtocol > ProxyReaderServer > ProxyReaderServerPsm >> CompoundState >> ChoiceState )
I 4360: Informal guard "ok" becomes 'true' @ ( Xmi > Data > Protocols > PlayerProtocol > PlayerServer > PlayerServerPsm >> ChoiceState )
I 4360: Informal guard "ok" becomes 'true' @ ( Xmi > Data > Protocols > ReaderProtocol > ReaderServer > ReaderServerPsm >> ChoiceState )
I 4360: Informal guard "ok" becomes 'true' @ ( Xmi > Data > Protocols > ReaderProtocol > ReaderServer > ReaderServerPsm >> CompoundState >> ChoiceState )
I 4360: Informal guard "valid TitleId" becomes 'true' @ ( Xmi > Data > Protocols > TitlebaseProtocol > TitlebaseServer > TbServerPsm >> ChoiceState )
I 4360: Informal guard "valid AtTime" becomes 'true' @ ( Xmi > Data > Protocols > TitlebaseProtocol > TitlebaseServer > TbServerPsm >> CompoundState >> ChoiceState )
I 4360: Informal guard "valid Chunk" becomes 'true' @ ( Xmi > Data > Protocols > TitlebaseProtocol > TitlebaseServer > TbServerPsm >> CompoundState >> ChoiceState )
I 4360: Informal guard "finished" becomes 'true' @ ( Xmi > Data > Protocols > TitlebaseProtocol > TitlebaseServer > TbServerPsm >> CompoundState >> ChoiceState )
W 4535: Self-transition is errorprone for NativeTrigger @ ( Xmi > Data > Repository > Player > ProxyProtocols > ProxyReaderProtocol > ProxyReaderClient > ProxyReaderClientPsm >> CompoundState >> Open )
W 4535: Self-transition is errorprone for NativeTrigger @ ( Xmi > Data > Protocols > ReaderProtocol > ReaderClient > ReaderClientPsm >> CompoundState >> Open )
W 4535: Self-transition is errorprone for NativeTrigger @ ( Xmi > Data > Protocols > TitlebaseProtocol > TitlebaseClient > TbClientPsm >> CompoundState >> Play )
W 4535: Self-transition is errorprone for NativeTrigger @ ( Xmi > Data > Protocols > TitlebaseProtocol > TitlebaseClient > TbClientPsm >> CompoundState >> Play )