The SIV Tool

SIV (Scenario Inter-dependency Visualization) is a tool aimed at visualizing inter-dependencies between scenarios in a scenario-based specification. More specifically, the tool accepts input graphs generated by the Play-Engine tool, based on Live Sequence Chart (LSC) specifications.

An inter-dependency graph is generated from a scenario-based specification, and captures many types of inter-dependencies between the scenarios. In this graph, each scenario is represented by a node. Special nodes are used to represent objects external to the system (clock, environment and user). Two nodes are connected by edges of different kinds, representing different kinds of inter-dependencies. This graph is visualized using the SIV tool. The tool allows many options, views and filters, in order to allow the user to better understand the specification, and to focus on the interesting parts thereof.

All examples given here were generated using the Play-Engine tool, developed in our group.

SIV is implemented in Java, using the excellent prefuse toolkit.

Additional information can be found in the paper (see "Publications" below). You can also contact me for any questions, comments, or suggestions.

This work was conducted in the lab of David Harel in the Weizmann Institute of Science, and supported by the John von Neumann Minerva Center for the Development of Reactive Systems at the Weizmann Institute of Science.

Publications

  1. D. Harel and I. Segall. "Visualizing Inter-Dependencies Between Scenarios". In
    R. Koschke, C. D. Hundhausen, and A. Telea, editors, Proceedings of the ACM 2008
    Symposium on Software Visualization (SoftVis’08), pp 145–153. ACM, 2008. [bibtex (DBLP)]

  2. D. Harel, I. Segall, H. Kugler and Y. Setty, "Crafting Game-Models using Reactive System Design", 
    Proc. Future Play 2008    , pp. 121-128, 2008 [pdf] [gym website].

Downloads

Screencasts

Examples

Following are some examples of inter-dependency graphs generated by the SIV tool.

Inter-dependency graph for the C-Elegans specification [1], as visualized in SIV. In this view, the user chose to visualize only causal and sync edges. This example shows some of the characteristics of the specification that are visually emphasized using this method. For example, note the DevelopmentalTime20c node,  that has many outgoing causal edges. This is a triggering LSC that drives the execution of many other LSCs. One can also note the set of LSCs named lin3* at the right end of the graph, all specifying the handling of the LIN-3 protein - an independent process, that is specified by a set of 7 LSCs, and is triggered by a single event appearing in the ACAdoptFate LSC (as can be seen by the fact that a single edge enters this set of LSCs, from the ACAdoptFate LSC). To the left of these LSCs, one can notice another quite-independent process, the AC/VU decision, invloving 7 other LSCs (in the middle of the graph).
In the bottom left corner of the graph there is a cloud of many LSCs with many edges connecting them. While the exact edges are not quite
prominent in this view, it is clear that this is a set of LSCs that are strongly inter-dependent. One can now further investigate these LSCs, and the way they
interact with each other.


A visualization of the C-Elegans specification, in which the user chose to view also the clock node. Edges adjacent to it were selected to be visible, yet not layoutable, therefore the layout from the previous image is maintained.


Aggregation of the C-Elegans specification according to Newman's community identification algorithm. In this aggregation, the graph is split into groups such that there are strong inter-dependencies within the group, and as few as possible between them. In SIV, one can also aggregate the nodes according to the use cases to which they belong.


Visualization of the the telecommunication application [2]. It is evident that in this specification, there are many "chain-reactions", i.e., a single LSC that causes a series of LSCs to open each other. 


Zoom in on a subset of the LSCs in the telecommunication application, showing both causal and sync edges.


Inter-dependency graph for an ATM specification. In this graph, causal and violating-cold-forbidden edges are shown. Note the clickCancel node, representing the LSC that reacts to the user clicking "cancel" - it may violate a cold forbidden element in several LSCs, thus cancelling their operation. The specification was written by Liat Nakar.


IDG for the "Gym Training System" specification [3]. Nodes labelled "WOx" represent charts waiting for external events, and trigerring different tasks, which in turn trigger different actions (each action represented by a single LSC node). Note that some actions, e.g. running, can be trigerred by several tasks, while others e,g, jumping, are task-specific. "Alert" LSCs, e.g. StormAlert, are in charge of output to external systems.


The "Gym Training System" IDG, aggregated according to Newman's community identification algorithm. The different tasks and their actions are clearly identified.


IDG for the "Gym Training System" specification, including both sync and causal edges. Now action LSCs are grouped closer, while input, task and output LSCs interact with this "cloud".

References

[1] N. Kam, D. Harel, H. Kugler, R. Marelly, A. Pnueli, E.J.A. Hubbard and M.J. Stern, "Formal Modeling of C. elegans Development: A Scenario-Based Approach", Proc. 1st Int. Workshop on Computational Methods in Systems Biology (ICMSB 2003), Lecture Notes in Computer Science, Vol. 2602, Springer-Verlag, pp. 4-20, Feb. 2003.  (Revised version in Modeling in Molecular Biology (G. Ciobanu and G. Rozenberg, eds.), Springer, Berlin, 2004, pp. 151-173.)

[2] P. Combes, D. Harel and H. Kugler, "Modeling and Verification of a Telecommunication Application using Live Sequence Charts and the Play-Engine Tool", Software and System Modeling (SoSyM), to appear. (Preliminary version in Proc. 3rd Int. Symp. on Automated Technology for Verification and Analysis (ATVA '05), Lecture Notes in Computer Science, Vol 3707, Springer-Verlag, 2005, 414-428.)

[3] D. Harel and Y. Setty, "Generic Reactive Animation: Realistic Modeling of Complex Natural Systems", Lecture Notes in Bioinformatics, to appear, 2008.  See also website.