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.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
References
Mauco, M.V., Leonardi, M.C., Riesco, D.: Deriving formal specifications from natural language requirements (2009)
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)
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)
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)
Lamsweerde, A.: Formal specification: a roadmap. In: Proceedings of the Conference on the Future of Software Engineering, pp. 147–159. Limerick, Ireland (2000)
Hasan, O., Tahar, S., Abbasi, N.: Formal reliability analysis using theorem proving. Comput. IEEE Trans. 59(5), 579–592 (2010)
Jackson, D.: Lightweight formal methods. In: FME 2001: Formal Methods for Increasing Software Productivity, pp. 1–1. Springer, Berlin, Germany (2001)
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)
Dromey, R.G.: Formalizing the transition from requirements to design. Math. Framew. Compon. Softw. Models Anal. Synth. 173–205 (2006)
Powell, D.: Requirements evaluation using behavior trees-findings from industry. In: Australian Software Engineering Conference (ASWEC’07), Melbourne, Australia (2007)
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)
Myers, T.: TextBE: a textual editor for behavior engineering. In: Proceedings of the 3rd Improving Systems and Software Engineering Conference (ISSEC), Sydney, Australia (2011)
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)
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)
Christie, A.M.: Simulation: an enabling technology in software engineering. CROSSTALK—J. Def. Softw. Eng. 12(4), 25–30 (1999)
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)
Sáenz-Pérez, F.: Outer joins in a deductive database system. Electron. Notes Theor. Comput. Sci. 282, 73–88 (2012)
Besson, F., Jensen, T.: Modular class analysis with datalog. In: Static Analysis, pp. 1075–1075. San Diego, California (2003)
Hoffmann, V., Lichter, H.: A model-based narrative use case simulation environment. In: ICSOFT, pp. 63–72. Athens, Greece (2010)
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)
Zafar, S., Dromey, R.G.: Managing Complexity in Modelling Embedded Systems. In: Systems Engineering/Test and Evaluation Conference SETE2005. Brisbane, Australia (2005)
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)
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)
Winter, K.: Formalising behaviour trees with CSP. In: Integrated Formal Methods, pp. 148–167 (2004)
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)
Yatapanage, N., Winter, K., Zafar, S.: Slicing behavior tree models for verification. In: Theoretical Computer Science, pp. 125–139. Springer (2010)
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)
Mens, T., Van Gorp, P.: A taxonomy of model transformation. Electron. Notes Theor. Comput. Sci. 152, 125–142 (2006)
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
Zafar, S., Farooq-Khan, N., Ahmed, M.: Requirements simulation for early validation using Behavior Trees and Datalog. Inf. Softw. Technol. 61, 52–70 (2015)
Steinberg, D., Budinsky, F., Merks, E., Paternostro, M.: EMF: Eclipse Modeling Framework. Pearson Education (2008)
Sáenz-Pérez, F.: DES: a deductive database system. Electron. Notes Theor. Comput. Sci. 271, 63–78 (2011)
Emerson, E.A.: Temporal and modal logic. Handb. Theor. Comput. Sci. 2, 995–1072 (1990)
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2020 Springer Nature Switzerland AG
About this paper
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
DOI: https://doi.org/10.1007/978-3-030-12385-7_27
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-030-12384-0
Online ISBN: 978-3-030-12385-7
eBook Packages: Intelligent Technologies and RoboticsIntelligent Technologies and Robotics (R0)