MODEL DRIVEN ENGINEERING
MODEL DRIVEN ENGINEERING
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.
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.
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.
Domain Specific Language & Formal Verification
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.
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.
Continuous Testing
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.
CODE GENERATION
Dezyne delivers verified, validated, easy to read source code that can be easily integrated with existing native or legacy code.
