Examples

To test and gain experience with our simulator, besides modeling simple examples like the node-network example (described while discussing the input grammar), we have modeled four non-trivial examples. We briefly discuss these examples here which can be downloaded by following the links on the left.

  1. Telephone-switch: Our model is based on the state-based models of the switch and phone given in [1]. It consists of a network of phones and switches, connected to each other. We model three groups of phones in different geographical localities, each being served by its own group of switches. These three groups of switches are in-turn connected with each other to facilitate a connection from a phone in one group to a phone in another group. We have also added the call-waiting feature to the basic call-setup protocol.
     
  2. Rail-car network: We have also modeled the popular rail-car example, whose behavioral requirements have been described in [2] using statecharts and in [3], using LSCs. It consists of railcar network, with several cars operating on two parallel cyclic paths with a fixed number of terminals (in our models it is, though it can be changed easily with minor modifications in the input specifications). The cars run clockwise on one of the cyclic paths and anti-clockwise on another. There are several reactive components in the system, such as: car, cruiser, platform-handler, proximity-sensor, etc. , which make its modeling and simulation even more interesting. A brief description of the example and its model can be found in [7].

    The next two examples we have modeled, are based on real-life reactive systems and have been proposed in the software engineering community as case studies for trying out reactive system modeling techniques [4].
     
  3. Automated rail-shuttle system: This system [5] consists of various shuttles which bid for orders to transport passengers between various stations on a railway-interconnection network. The successful bidder needs to complete the order in a given time, for which it gets payment as specified in the bid. In case it gets late in picking up its order or in reaching the destination on time, it has to pay penalty which is predetermined. A shuttle also needs to pay toll for the part of network it travels. A part of network may be disabled at some time due to repair work, causing shuttles to take alternative routes. Also, after traveling a specified distance the shuttles need to undergo maintenance-check. In case a shuttle becomes bankrupt (due to payment of fines exceeding its earning), it is retired from the system.
     
  4. Weather-update controller: The weather update controller [6] is a crucial part of the Center TRACON Automation System (CTAS),  a set of automation tools developed at NASA to manage high volume of arrival air-traffic at large airports. In this example, we model three components: weather-aware clients, weather-control panel(WCP), and the controller or communications manager(CM). When there is new weather information at the WCP, and user presses the update button then this latest weather information is sent to all weather-aware clients, currently connected to the controller, via the controller. These clients then need to update themselves using this new information and start using it together. This update may succeed or fail in different ways, and clients may even get disconnected as a result of this.

    Following example is based on the requirements specification of a real-life media infotainment networking system.
     
  5. Media Oriented Systems Transport (MOST). The MOST is a networking standard [8] that has been designed for interconnecting various classes of multimedia components in automobiles. The MOST network can contain up to 64 nodes, connected together in ring topology. The nodes mainly comprise of multimedia devices such as CD player etc. One of the main network activity is of `Network Management' and deals with managing and distributing the node information amongst the node themselves; so that they can use services provided by each-other. For this purpose, one node designated as `Network Master', or NM, maintains the central registry containing information about all other nodes which are called `Network Slaves' or NS. Whenever network is switched `On' or there is a `Network Change Event' due to some node leaving or entering the network, NM rescans the network to update its central registry. During a network-scan NM requests information from all the slave nodes, and expects a reply within a given time period. Various scenarios arise when-- a slave node fails to reply within the given time, sends an erroneous reply etc.

The zip file containing these examples, together with state diagrams and explanations of the main components in the system can be downloaded by following the links on the left.

References

  1. G.J. Holzmann. Modeling a Simple Telephone Switch, chapter 14. The SPIN Model Checker. Addison-Wesley, 2004.
  2. D. Harel and E. Gery. Executable object modeling with statecharts. IEEE Computer, 30(7), 1997.
  3. W. Damm and D. Harel. LSCs: Breathing life into message sequence charts. Formal Methods in System Design, 19(1), 2001.
  4. http://scesm04.upb.de/case-studies.html
  5. Shuttle Control System. New rail-technology Paderborn. See http://wwwcs.uni-paderborn.de/cs/ag-schaefer/CaseStudies/ShuttleSystem
  6. CTAS. Center TRACON automation system. http://ctas.arc.nasa.gov
  7. Modeling of Harel's Rail-Car Example as Interacting Process Classes. http://www.comp.nus.edu.sg/~ankit/Railcar.ps
  8. MOST cooperation. Media Oriented System Transport. http://www.mostcooperation.com