Skip to Main content Skip to Navigation
Journal articles

jSynoPSys - A Scenario-Based Testing Tool based on the Symbolic Animation of B Machines

Frédéric Dadeau 1 Régis Tissot 2
1 CASSIS - Combination of approaches to the security of infinite states systems
FEMTO-ST - Franche-Comté Électronique Mécanique, Thermique et Optique - Sciences et Technologies (UMR 6174), Inria Nancy - Grand Est, LORIA - FM - Department of Formal Methods
Abstract : This paper presents the jSynoPSys tool that implements the concept of Scenario-Based Testing from B machines. This consists in describing execution scenarios, expressed as regular expressions over the operations of the system, coupled with intermediate system states that have to be reached when the scenario is unfolded. The tool relies on the BZ-Testing-Tools engine, originally designed to perform symbolic animation and boundary test generation from B machines. The main advantage of our Scenario-Based Testing technique is that it performs a full abstraction of the operation parameter values, that are instantiated at the end, when the scenario has been completely unfolded, using constraint solving techniques.
Document type :
Journal articles
Complete list of metadata
Contributor : Frédéric Dadeau Connect in order to contact the contributor
Submitted on : Monday, November 2, 2009 - 10:29:12 AM
Last modification on : Saturday, October 16, 2021 - 11:26:06 AM

Links full text



Frédéric Dadeau, Régis Tissot. jSynoPSys - A Scenario-Based Testing Tool based on the Symbolic Animation of B Machines. Electronic Notes in Theoretical Computer Science, Elsevier, 2009, Proceedings of Fifth Workshop on Model Based Testing (MBT 2009), 253 (2), pp.117-132. ⟨10.1016/j.entcs.2009.09.055⟩. ⟨inria-00429234⟩



Record views