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.

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.

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

Java source code generation

C++ source code generation (Windows)

C++ source code generation (Linux)

C source code generation (Windows)

C source code generation (Linux)

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.