Requirements simulation for early validation using Behavior Trees and Datalog

ContextThe 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.ObjectiveThe 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 timesMethodBehavior Trees (BTs)¹ 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)².ResultsThe 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.ConclusionQueries 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.