Abstract
This paper introduces automatic model driven animation, a novel approach to validate requirements specifications. This approach, here applied to SCR specifications, is based on graphical animation. Automatic model driven animation consists in automatically deriving scenarios from requirements specifications; these scenarios are used to animate critical system behaviors through a graphical interface. Animation is useful at the very early stages of systems development to better understand models and requirements, to gain confidence that specifications capture informal requirements, and to detect faults.We introduce a technique, exploiting model checkers, to automatically generate animation sequences starting from requirements specifications, and we present a prototype tool for the generation and animation of scenarios.
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
R. Bharadwaj and C. Heitmeyer. Model checking complete requirements specifications using abstraction. Automated Software Engineering Journal, 6(1), Jan. 1999.
J. Bicarregui, J. Dick, B. Matthews, and E. Woods. Making the most of formal specification through animation, testing and proof. Science of Computer Programming, 29(1–2):53–78, July 1997.
E. Börger, E. Riccobene, and J. Schmid. Capturing requirements by abstract state machines: The light control case study. Journal of Universal Computer Science, 6(7):597–620, July 2000.
A. Cavarra and E. Riccobene. Simulating UML statecharts. In R. Moreno-Diaz and A. Quesada-Arencibia, editors, Formal Methods and Tools for Computer Science-Eurocast 2001, pages 224–227, 2001.
P.-J. Courtois and D. L. Parnas. Documentation for safety critical software. In Proc. 15th Int’l Conf. on Softw. Eng. (ICSE’ 93), pages 315–323, Baltimore, MD, 1993.
A. Gargantini and C. Heitmeyer. Using model checking to generate tests from requirements specifications. In O. Nierstrasz and M. Lemoine, editors, Proceedings of the 7th European Engineering Conference and the 7th ACMSIGSOFT Symposium on the Foundations of Software Engineering, volume 1687 of LNCS, Sept. 6–10 1999.
A. Gargantini, L. Liberati, A. Morzenti, and C. Zacchetti. Specifying, validating and testing a traffic management system in the TRIO environment. In Compass’96: Eleventh Annual Conference on Computer Assurance, page 65, Gaithersburg, Maryland, 1996. National Institute of Standards and Technology.
A. Gargantini and A. Morzenti. Automated deductive requirements analysis of critical systems. ACM Transactions on Software Engineering and Methodology, 10(3):255–307, July 2001.
A. Gargantini and E. Riccobene. ASM-based testing: Coverage criteria and automatic test sequence generation. Journal of Universal Computer Science, 7(11):1050–1067, Nov. 2001.
D. Hazel, P. Strooper, and O. Traynor. Requirements engineering and verification using specification animation. In Thirteenth International Conference on Automated Software Engineering, pages 302–305. IEEE Computer Society Press, 1998.
C. Heitmeyer, J. Kirby, B. Labaw, and R. Bharadwaj. SCR: A toolset for specifying and analyzing software requirements. In Proc. 10th International Computer Aided Verification Conference, pages 526–531, 1998.
C. Heitmeyer, J. Kirby, Jr., B. Labaw, M. Archer, and R. Bharadwaj. Using abstraction and model checking to detect safety violations in requirements specifications. IEEE Transactions on Software Engineering, 24(11):927–948, Nov. 1998.
C. L. Heitmeyer. Software cost reduction. In J. J. Marciniak, editor, Encyclopedia of Software Engineering, Two Volumes. JohnWiley & Sons, January 2002.
C. L. Heitmeyer, R. D. Jeffords, and B. G. Labaw. Automated consistency checking of requirements specifications. ACM Transactions on Software Engineering and Methodology, 5(3):231–261, April–June 1996.
G. J. Holzmann. The model checker SPIN. IEEE Transactions on Software Engineering, 23(5):279–295, May 1997.
E. Kazmierczak, M. Winikoff, and P. Dart. Verifying model oriented specifications through animation. In Asia Pacific Software Engineering Conference, pages 254–261. IEEE Computer Society Press, 1998.
R. A. Kemmerer. Testing formal specifications to detect design errors. IEEE Transactions on Software Engineering, 11(1):32–43, Jan. 1985.
J. Magee, J. Kramer, B. Nuseibeh, D. Bush, and J. Sonander. Hybrid model visualization in requirements and design:Apreliminary investigation. In Proceedings of the 10th International Workshop on Software Specification and Design (IWSSD-10), Nov. 2000.
J. Magee, N. Pryce, D. Giannakopoulou, and J. Kramer. Graphical animation of behavior models. In Proceedings of the 22nd International Conference on Software Engineering, pages 499–508. ACM Press, June 2000.
K. L. McMillan. The SMV system. Technical report, Carnegie-Mellon University, Pittsburgh, PA, 1992. DRAFT.
T. Miller and P. Strooper. Animation can showonly the presence of errors, never their absence. In Proc. of the 2001 Australian Software Engineering Conference (ASWEC 2001), pages 76–85. IEEE Computer Society, 2001.
I. Parissis. A formal approach to testing lustre specifications. In 1st International IEEE Conference on Formal Engineering Methods, Hiroshima, pages 91–100, 1997.
J. Schimd. Executing ASM specifications with AsmGofer. http://www.tydo.de/AsmGofer.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2003 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Gargantini, A., Riccobene, E. (2003). Automatic Model Driven Animation of SCR Specifications. In: Pezzè, M. (eds) Fundamental Approaches to Software Engineering. FASE 2003. Lecture Notes in Computer Science, vol 2621. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-36578-8_21
Download citation
DOI: https://doi.org/10.1007/3-540-36578-8_21
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-00899-6
Online ISBN: 978-3-540-36578-5
eBook Packages: Springer Book Archive