In this award winning paper, we describe the Dezyne language and a model transformation to the mCRL2 language, providing users access to advanced model checking capabilities and refinement checks of the mCRL2 tool set.
In this paper, we show how Dezyne can be used to recover lost or poorly understood behaviour from a legacy codebase. The models of the rediscovered behavior will be both formally complete and correct. These models then offer a solid foundation for the further development of a software system.
This paper takes both the notion of McBabe’s Cyclomatic Complexity metric (CC) and Halstead metrics, and adopts them for a model based approach. The Cyclomatic Complexity is an indication of the number of independent path in the code, whereas Halstead metrics measure the cognitive load of a program which is the mental effort to understand the program.
In this paper the effects of applying Verum tools of formal verification to the development of various control software units developed for the X-ray machines are analyzed. The quality of these units are compared with other units developed in traditional development methods. The results indicate that Verum’s formal design verification eliminates design errors earlier and results in reduced development time.
In this paper we use the Agile manifesto as a reference framework to describe how a Component Based Development (CBD) methodology in combination with Model Driven Development (MDD) and Dezyne supports an Agile development process.