April 9-11th 2014
Churchill College, Cambridge UK


Session Title

Testing ASD Interface Compliance with Spec Explorer

Session Type Case Study
Duration 45 minutes
Session Description

As with any kind of construction, reliability is of utmost importance in software engineering. To achieve this, Verum® has created the Analytical Software Design (ASD), a component based design method. By using this method, software can be constructed that is guaranteed to implement specified interfaces and protocols and is deadlock-free. It is based on the decomposition of a system into different components, used to generate verified code for the designed components that can then be integrated to construct complete and correct industrial scale systems from these components. However, in practice, many software systems require the use of third party and/or legacy components that have not been verified. The ASD method gives no guarantees for these external components nor for the integrated system. To remedy this, we propose to use Model-Based Testing (MBT) to verify if the external components implement the behaviour of the interface defined by the ASD models.

We implemented a prototype of this approach that transforms ASD models to Microsoft® Spec Explorer models. Spec Explorer allows us to generate automated test cases that explore the expected interface behaviour of any component, and enables us to find violations of the requirements with a minimum of manual effort. Furthermore, in addition to the verification ASD provides, Spec Explorer can use data testing to validate that the system implements desired behaviour by linking inputs to observable events. By reusing ASD models, this novel method gives us the full usage of all benefits of this powerful MBT tool (e.g. data abstraction to reduce state space and overcome state explosion and models decomposition) without facing issues related to creation of complex test models.


Arjan van der Meer (Nspyre)

Arjan van der Meer is a Software Engineer at Nspyre where he works in the domain of model-driven engineering and model-based testing. Before joining Nspyre, Arjan was a PhD student at the Eindhoven University of Technology, where he also obtained his Masters in Computer Science and Engineering. He hopes to defend his thesis in early 2014. During his time as a PhD student, Arjan worked on specification and implementation of type systems for domain specific languages.