Dezyne is a model-driven software engineering tool that enables software engineers to specify, design, validate and formally verify software components for embedded, industrial & technical software systems.
Model Driven Development
Based on the Eclipse IDE, Dezyne provides a complete environment for specifying, designing, exploring, testing, generating and building model based software components. Engineers can easily understand, navigate through and communicate about their component models using a range of graphical representations, including state charts, event tables, system models and sequence charts. Dezyne integrates directly with conventional build environments and tools, enabling model verification, validation and code generation to be completely integrated with existing build processes.
Component Based Design
Dezyne is based upon well-established component engineering principles common place in the hardware world. A Dezyne component is stated in terms of two types of model, an interface specification model and a component implementation model. Interface specifications define the externally visible behaviour of a component. Implementation models contain the operational logic of a component. Implementation models are verified against any interface specifications that they provide or require and can therefore be easily composed into entire, hierarchical systems. Dezyne models are compositional, meaning that large, reliable and robust systems can be constructed from verified component models. As with hardware engineering, software components built with Dezyne are easy to maintain, simple to reuse and straight forward to extend.
Domain Specific Language
The heart of Dezyne is an open, plain text, domain specific language used to design the structure and behaviour of a software system. While the syntax of the Dezyne Modelling Language (DML) is intentionally similar to that of most common programming languages, DML distinguishes itself from other modelling languages such as UML, by having formally specified semantics. This enables the direct translation of DML into a mathematical representation that is then subjected to automated analysis using formal methods. DML is an open language and can be easily translated to and from other formalisms.
Dezyne ensures that many defects are detected and removed from specifications and component designs early in the lifecycle by subjecting both types of model to formal mathematical analysis. At the user’s behest, DML models are automatically converted into mathematical form and a range of completeness and correctness theorems are applied. Should a design error be found, the sequence of events that led to the error is displayed in the Dezyne simulator. The close coupling of modelling, verification and simulation enables the most complex behavioural design errors to be rapidly identified and fixed, saving huge amounts of testing and rework later in the lifecycle.
Simulation and Validation
The Dezyne simulator enables engineers to validate that their specifications and designs behave as expected and that they implement required use cases. Engineers can explore the behaviour of a specification or design using the simulator by constructing a sequence trace and then stepping through the trace at model statement level, examining program flow, variables, events and responses. Traces can be stored and replayed at will, providing the means to automatically regression test Dezyne models against use cases. Establishing that a design meets its requirements early in the lifecycle is yet another way in which Dezyne saves time, effort and money.
Dezyne provides mechanisms to support the continuous testing – verification and validation – of specification and design models throughout the lifecycle. Whenever a Dezyne model is changed, the model can be automatically verified for errors and validated against invariant use cases. Changes to specification models can be configured to trigger verification and validation test cycles for all other dependent models, immediately identifying where a specification change has a ripple effect. By ensuring that all models remain complete, correct and consistent throughout the lifecycle, Dezyne prevents the long term degradation of a codebase and reduces the accumulation of technical debt, enabling businesses to spend more time developing new features and less time maintaining old code.
Ultimately, Dezyne delivers verified, validated, easy to read source code that can be easily integrated with existing native or legacy code. Dezyne provides code generators for various flavours of C, C++, C#, Java and Python. Dezyne does not require the use of a proprietary run-time environment. For most languages, such a C++ 11, C# or Java, Dezyne makes use of run-time facilities built into the language itself. For C or C++ 03, a minimal, small footprint runtime is required, which is provided to the user in source code form. Dezyne is the result of years of co-creation with Verum’s core customers and has been designed from the ground up for direct and easy integration with existing codebases.