Skip to main content
SpringerLink
Log in

SimTee: An Automated Environment for Simulation and Analysis of Requirements

  • Conference paper
  • First Online:
Book cover Advances in Information and Communication (FICC 2019)

Part of the book series: Lecture Notes in Networks and Systems ((LNNS,volume 70))

Included in the following conference series:

  • 1482 Accesses

Abstract

The mathematical nature of Formal Methods make them more amenable for machine assisted analysis. However, the exhaustive model-checking and theorem-proving of the complete specification remains an elusive target due to the state-explosion problem. Simulation or execution of formally specified requirements provides us a less expensive alternate to understand, analyze and validate requirements early in the development phase. In this paper, we present SimTree simulator that carries out requirements analysis. SimTree code is generated from automatically transforming Behavior Trees (BT)—a graphical formal notation—using ATLAS Transformation Language (ATL). During the step-by-step execution of BT, Datalog code is also generated. The Datalog queries are used to further analyze the stored state-space of the executed requirements. These features of the simulator are illustrated using a published case study. The simulator was useful for identifying and rectifying logical defects in the specification.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 169.00
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 219.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

References

  1. Mauco, M.V., Leonardi, M.C., Riesco, D.: Deriving formal specifications from natural language requirements (2009)

    Google Scholar 

  2. Jensen, K., Kristensen, L.M., Wells, L.: Coloured Petri nets and CPN tools for modelling and validation of concurrent systems. Int. J. Softw. Tools Technol. Transf. 9(3–4), 213–254 (2007)

    Article  Google Scholar 

  3. Wagner, F., Wolstenholme, P.: Modeling and building reliable, re-useable software. In: Engineering of Computer-Based Systems, 2003. Proceedings. 10th IEEE International Conference and Workshop on the, pp. 277–286. Alabama, USA (2003)

    Google Scholar 

  4. Dromey, R.G.: From requirements to design: Formalizing the key steps. In: Software Engineering and Formal Methods, 2003. Proceedings. First International Conference, pp. 2–11. Brisbane, Australia (2003)

    Google Scholar 

  5. Lamsweerde, A.: Formal specification: a roadmap. In: Proceedings of the Conference on the Future of Software Engineering, pp. 147–159. Limerick, Ireland (2000)

    Google Scholar 

  6. Hasan, O., Tahar, S., Abbasi, N.: Formal reliability analysis using theorem proving. Comput. IEEE Trans. 59(5), 579–592 (2010)

    Article  MathSciNet  Google Scholar 

  7. Jackson, D.: Lightweight formal methods. In: FME 2001: Formal Methods for Increasing Software Productivity, pp. 1–1. Springer, Berlin, Germany (2001)

    Google Scholar 

  8. Schmid, R., Ryser, J., Berner, S., Glinz, M., Reutemann, R., Fahr, E.: A survey of simulation tools for requirement engineering. Universität Zürich, Institut für Informatik (2000)

    Google Scholar 

  9. Dromey, R.G.: Formalizing the transition from requirements to design. Math. Framew. Compon. Softw. Models Anal. Synth. 173–205 (2006)

    Google Scholar 

  10. Powell, D.: Requirements evaluation using behavior trees-findings from industry. In: Australian Software Engineering Conference (ASWEC’07), Melbourne, Australia (2007)

    Google Scholar 

  11. Wen, L., Colvin, R., Lin, K., Seagrott, J., Yatapanage, N., Dromey, G.: ‘Integrare’, a collaborative environment for behavior-oriented design. In: Cooperative Design, Visualization, and Engineering, pp. 122–131. Springer (2007)

    Google Scholar 

  12. Myers, T.: TextBE: a textual editor for behavior engineering. In: Proceedings of the 3rd Improving Systems and Software Engineering Conference (ISSEC), Sydney, Australia (2011)

    Google Scholar 

  13. Grunske, L., Winter, K., Yatapanage, N.: Defining the abstract syntax of visual languages with advanced graph grammars—a case study based on behavior trees. J. Vis. Lang. Comput. 19(3), 343–379 (2008)

    Article  Google Scholar 

  14. Kim, S.-K., Myers, T., Wendland, M.-F., Lindsay, P.A.: Execution of natural language requirements using state machines synthesised from Behavior Trees. J. Syst. Softw. 85(11), 2652–2664 (2012)

    Article  Google Scholar 

  15. Christie, A.M.: Simulation: an enabling technology in software engineering. CROSSTALK—J. Def. Softw. Eng. 12(4), 25–30 (1999)

    Google Scholar 

  16. Rushby, J.M.: Model Checking and Other Ways of Automating Formal Methods Position Paper Panel Model Checking Concurrent Programs. Software Quality Week, San Francisco (1995)

    Google Scholar 

  17. Sáenz-Pérez, F.: Outer joins in a deductive database system. Electron. Notes Theor. Comput. Sci. 282, 73–88 (2012)

    Article  Google Scholar 

  18. Besson, F., Jensen, T.: Modular class analysis with datalog. In: Static Analysis, pp. 1075–1075. San Diego, California (2003)

    Google Scholar 

  19. Hoffmann, V., Lichter, H.: A model-based narrative use case simulation environment. In: ICSOFT, pp. 63–72. Athens, Greece (2010)

    Google Scholar 

  20. Dromey, R.G.: Architecture as an emergent property of requirements integration. In: STRAW’03 Second International Software Requirements to Architectures Workshop, p. 77. Oregon, USA (2003)

    Google Scholar 

  21. Zafar, S., Dromey, R.G.: Managing Complexity in Modelling Embedded Systems. In: Systems Engineering/Test and Evaluation Conference SETE2005. Brisbane, Australia (2005)

    Google Scholar 

  22. Grunske, L., Lindsay, P., Yatapanage, N., Winter, K.: An automated failure mode and effect analysis based on high-level design specification with behavior trees. In: Integrated Formal Methods, pp. 129–149. The Netherlands, Eindhoven (2005)

    Chapter  Google Scholar 

  23. Colvin, R., Grunske, L., Winter, K.: Timed behavior trees for failure mode and effects analysis of time-critical systems. J. Syst. Softw. 81(12), 2163–2182 (2008)

    Article  Google Scholar 

  24. Winter, K.: Formalising behaviour trees with CSP. In: Integrated Formal Methods, pp. 148–167 (2004)

    Google Scholar 

  25. Grunske, L., Colvin, R., Winter, K.: Probabilistic model-checking support for FMEA. In: Quantitative Evaluation of Systems, 2007. QEST 2007. Fourth International Conference, pp. 119–128. Edinburgh, Scotland (2007)

    Google Scholar 

  26. Yatapanage, N., Winter, K., Zafar, S.: Slicing behavior tree models for verification. In: Theoretical Computer Science, pp. 125–139. Springer (2010)

    Google Scholar 

  27. Allilaire, F., Bézivin, J., Jouault, F., Kurtev, I.: ATL-eclipse support for model transformation. In: Proceedings of the Eclipse Technology eXchange workshop (eTX) at the ECOOP 2006 Conference, vol. 66. Nantes, France (2006)

    Google Scholar 

  28. Mens, T., Van Gorp, P.: A taxonomy of model transformation. Electron. Notes Theor. Comput. Sci. 152, 125–142 (2006)

    Article  Google Scholar 

  29. Templates, J.E.: Part of the Eclipse Modeling Framework, see JET Tutorial by Remko Pompa at http://eclipse.org/articles, Article-JET2/jet_tutorial2. html, vol. 69

  30. Zafar, S., Farooq-Khan, N., Ahmed, M.: Requirements simulation for early validation using Behavior Trees and Datalog. Inf. Softw. Technol. 61, 52–70 (2015)

    Article  Google Scholar 

  31. Steinberg, D., Budinsky, F., Merks, E., Paternostro, M.: EMF: Eclipse Modeling Framework. Pearson Education (2008)

    Google Scholar 

  32. Sáenz-Pérez, F.: DES: a deductive database system. Electron. Notes Theor. Comput. Sci. 271, 63–78 (2011)

    Article  Google Scholar 

  33. Emerson, E.A.: Temporal and modal logic. Handb. Theor. Comput. Sci. 2, 995–1072 (1990)

    MathSciNet  MATH  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Faculty of Computing, Riphah International University, Islamabad, Pakistan

    Saad Zafar, Musharif Ahmed, Taskeen Fatima & Zohra Aslam

Authors
  1. Saad Zafar
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Musharif Ahmed
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Taskeen Fatima
    View author publications

    You can also search for this author in PubMed Google Scholar

  4. Zohra Aslam
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Saad Zafar .

Editor information

Editors and Affiliations

  1. Faculty of Science and Engineering, Saga University, Saga, Japan

    Kohei Arai

  2. The Science and Information (SAI) Organization, Bradford, UK

    Rahul Bhatia

Rights and permissions

Reprints and permissions

Copyright information

© 2020 Springer Nature Switzerland AG

About this paper

Check for updates. Verify currency and authenticity via CrossMark

Cite this paper

Zafar, S., Ahmed, M., Fatima, T., Aslam, Z. (2020). SimTee: An Automated Environment for Simulation and Analysis of Requirements. In: Arai, K., Bhatia, R. (eds) Advances in Information and Communication. FICC 2019. Lecture Notes in Networks and Systems, vol 70. Springer, Cham. https://doi.org/10.1007/978-3-030-12385-7_27

Download citation

Publish with us

Policies and ethics

Search

Navigation