Philips Healthcare has been Verum’s lead customer since 2008 and in that time have used our products for a range of applications, using both Dezyne’s predecessor, the ASD:Suite, and Dezyne itself. Philips have also contributed to a range of case studies and papers related to the use of our tools.
Case Studies and Papers
Modelling in an Industrial Setting
In this presentation, Professor Jan Friso Groote of the Eindhoven University of Technology describes the use of Verum’s ASD:Suite toolset (Dezyne’s predecessor) in an industrial setting. For healthcare applications he states that “At Philips Healthcare software is developed by staff using formal methods [Verum’s tools]. Is this better? Yes, up to 10 times less bugs, up to 3 times faster. Industry standard 5-50 bugs/Kloc. Formal techniques 0.7 bugs/Kloc”. He concludes his presentation with “Model based design and verification of behaviour leads to a 10-fold increase in quality and a 3-fold increase in development speed.”
Industrial Experience with the Migration of LegacyModels using a DSL
In this paper, we present an approach to use a RhapsodyDSL to transform Rhapsody models into Dezyne models. Model instances of the Rhapsody tool are instances of this DSL. The generator of the DSL transforms the models into model in-stances of the Dezyne modelling tool. We used ComMA as an intermediate language. To gain conﬁdence in the transformation, model learning and equivalence checking have been applied.
Evaluating the effect of a lightweight formal technique in industry
We evaluate the effect of applying the commercial formal technique Analytical Software Design (ASD) toan industrial project. In ASD, interfaces and software designs are modelled using a formal tabular notation. The ASD toolset supports formal checks of these models, such as deadlock freedom and interface compliance. In addition, full code can be generated from design models. ASD has been applied atPhilips Healthcare to develop parts of the software of interventional X-ray systems. We report about the experiences with the embedding of ASD into the development processes.The quality of the resulting code and the productivity has been analysed and compared to code developed with other techniques. We observe that the use of ASD leads to a strong reduction of the number of defects and an increase in productivity. The results are also compared to the literature about standards and related projects at other companies