Graphical animation of behavior models

ABSTRACT

Graphical animation is a way of visualizing the behavior of design models. This visualization is of use in validating a design model against informally specified requirements and in interpreting the meaning and significance of analysis results in relation to the problem domain. In this paper we describe how behavior models specified by Labeled Transition Systems (LTS) can drive graphical animations. The semantic framework for the approach is based on Timed Automata. Animations are described by an XML document that is used to generate a set of JavaBeans. The elaborated JavaBeans perform the animation actions as directed by the LTS model.

REFERENCES

• 1: Jeff Magee , Jeff Kramer , Dimitra Giannakopoulou, Behaviour Analysis of Software Architectures, Proceedings of the TC2 First Working IFIP Conference on Software Architecture (WICSA1), p.35-50, February 22-24, 1999
• 2: J. Magee , J. Kramer , D. Giannakopoulou, Analysing the behaviour of distributed software architectures: a case study, Proceedings of the 6th IEEE Workshop on Future Trends of Distributed Computing Systems (FTDCS '97), p.240, October 29-31, 1997
• 3: Shing C. Cheung , Jeff Kramer, Checking subsystem safety properties in compositional reachability analysis, Proceedings of the 18th international conference on Software engineering, p.144-154, March 25-29, 1996, Berlin, Germany
• 4: Dimitra Giannakopoulou , Jeff Magee , Jeff Kramer, Checking progress with action priority: is it fair?, Proceedings of the 7th European software engineering conference held jointly with the 7th ACM SIGSOFT international symposium on Foundations of software engineering, p.511-527, September 06-10, 1999, Toulouse, France
• 5: David Harel , Amir Pnueli , Hagi Lachover , Amnon Naamad , Michal Politi , Rivi Sherman , Aharon Shtull-Trauring , Mark Trakhtenbrot, STATEMATE: A Working Environment for the Development of Complex Reactive Systems, IEEE Transactions on Software Engineering, v.16 n.4, p.403-414, April 1990 [doi>10.1109/32.54292]
• 6: Jeff Magee , Jeff Kramer, Concurrency: state models & Java programs, John Wiley & Sons, Inc., New York, NY, 2000
• 7: Rajeev Alur , David L. Dill, A theory of timed automata, Theoretical Computer Science, v.126 n.2, p.183-235, April 25, 1994 [doi>10.1016/0304-3975(94)90010-8]
• 8: Dimitra Giannakopoulou , Jeff Kramer , Shing Chi Cheung, Behaviour Analysis of Distributed Systems Using the Tracta Approach, Automated Software Engineering, v.6 n.1, p.7-35, January 1999 [doi>10.1023/A:1008645800955]
• 9: A. Lotzberger and R. Muhfeld, "Task Description of a Flexible Cell with Real Time Properties," FZI, Karslruhe version 2.1, http://www.fzi.de/prost/projects/korsys/ 1996.
• 10: T. Bray, J. paoli, and C. M. Sperberg-McQueen, "Extensible Markup Language," World Wide Web Consortium http://www.w3.org/TR/1998/REC-xml-19980210 1998.
• 11: Gerard J. Holzmann, The Model Checker SPIN, IEEE Transactions on Software Engineering, v.23 n.5, p.279-295, May 1997 [doi>10.1109/32.588521]
• 12: Rance Cleaveland , Philip M. Lewis , Scott A. Smolka , Oleg Sokolsky, The Concurrency Factory: A Development Environment for Concurrent Systems, Proceedings of the 8th International Conference on Computer Aided Verification, p.398-401, August 03, 1996
• 13: R. Milner, A Calculus of Communicating Systems, Springer-Verlag New York, Inc., Secaucus, NJ, 1982
• 14: K. G. Larsen, P. Pettersson, and W. Yi, "UPPAAL in a Nutshell," Springer International Journal on Software Tools for Technology Transfer, vol. 1, pp. 134-152, 1997.
• 15: V. Roy and R. de Simone, "Auto/Autograph," in Computer-Aided Verification, R. Kurshan, Ed.: Kluwer Academic Publishers, 1993.
• 16: Constance Heitmeyer , James Kirby , Bruce Labaw, The SCR method for formally specifying, verifying, and validating requirements: tool support, Proceedings of the 19th international conference on Software engineering, p.610-611, May 17-23, 1997, Boston, Massachusetts, United States [doi>10.1145/253228.253498]
• 17: R. Bharadwaj and C. Heitmeyer, "Verifying SCR Requirements Specifications Using State Exploration," presented at 1st ACM Sigplan Workshop on Automated Analysis of Software (AAS'97), Paris, France, January 1997.
• 18: John T. Stasko , Marc H. Brown , Blaine A. Price, Software Visualization, MIT Press, Cambridge, MA, 1997
• 19: John T. Stasko, Tango: A Framework and System for Algorithm Animation, Computer, v.23 n.9, p.27-39, September 1990 [doi>10.1109/2.58216]
• 20: John Stasko, Animating algorithms with XTANGO, ACM SIGACT News, v.23 n.2, p.67-71, Spring 1992 [doi>10.1145/130956.130959]
• 21: Gruia-Catalin Roman , Kenneth C. Cox, A Taxonomy of Program Visualization Systems, Computer, v.26 n.12, p.11-24, December 1993 [doi>10.1109/2.247643]
• 22: G. C. Roman, K. Cox, C. Wilcox, and J. Plun, "Pavane: A System for Declarative Visualization of Concurrent Computations," Journal of Visual Languages and Computing, vol. 3, pp. 161-193, January 1992.
• 23: Gruia-Catalin Roman , H. Conrad Cunningham, Mixed Programming Metaphors in a Shared Dataspace Model of Concurrency, IEEE Transactions on Software Engineering, v.16 n.12, p.1361-1373, December 1990 [doi>10.1109/32.62445]
• 24: C. Karamanolis, D. Giannakopoulou, J. Magee, and S. Wheater, "Modelling and Analysis of Workflkow Processes," Imperial College, London TR 99/2, 1999.

INDEX TERMS

Primary Classification:
  K. Computing Milieux
  K.6 MANAGEMENT OF COMPUTING AND INFORMATION SYSTEMS
      K.6.3 Software Management
          Subjects: Software development

Additional Classification:
  H. Information Systems
  H.5 INFORMATION INTERFACES AND PRESENTATION (I.7)
      H.5.1 Multimedia Information Systems
          Subjects: Animations

  I. Computing Methodologies
  I.3 COMPUTER GRAPHICS
      I.3.7 Three-Dimensional Graphics and Realism
          Subjects: Animation

General Terms:
Algorithms, Design, Management, Performance, Theory, Verification

Keywords:
behvior analysis, graphic animation, labeled transition system