Treffer: Requirements simulation for early validation using Behavior Trees and Datalog.

Context The role of formal specification in requirements validation and analysis is generally considered to be limited because considerable expertise is required in developing and understanding the mathematical proofs. However, formal semantics of a language can provide a basis for step-by-step execution of requirements specification by building an easy to use simulator to assist in requirements elicitation, validation and analysis. Objective The objective of this paper is to illustrate the usefulness of a simulator that executes requirements and captures system states as rules and facts in a database. The database can then be queried to carry out analysis after all the requirements have been executed a given number of times Method Behavior Trees (BTs) 1 BTs – Behavior Trees. 1 are automatically translated into Datalog facts and rules through a simulator called SimTree. The translation process involves model-to-model (M2M) transformation and model-to-text (M2T) transformation which automatically generates the code for a simulator called SimTree. SimTree on execution produces Datalog code. The effectiveness of the simulator is evaluated using the specifications of a published case study – Ambulatory Infusion Pump (AIP) 2 AIP – Ambulatory Infusion Pump. 2 . Results The BT specification of the AIP was transformed into SimTree code for execution. The simulator produced a complete state-space for a predetermined number of runs in the form of Datalog facts and rules, which were then analyzed for various properties of interest like safety and liveness. Conclusion Queries of the resultant Datalog code were found to be helpful in identifying defects in the specification. However, probability values had to be manually assigned to all the events to ensure reachability to all leaf nodes of the tree and timely completion of all the runs. We identify optimization of execution paths to reduce execution time as our future work. [ABSTRACT FROM AUTHOR]

Copyright of Information & Software Technology is the property of Elsevier B.V. and its content may not be copied or emailed to multiple sites without the copyright holder's express written permission. Additionally, content may not be used with any artificial intelligence tools or machine learning technologies. However, users may print, download, or email articles for individual use. This abstract may be abridged. No warranty is given about the accuracy of the copy. Users should refer to the original published version of the material for the full abstract. (Copyright applies to all Abstracts.)