Discover Dezyne
Why Dezyne?
Designing and creating software that controls embedded and cyber-physical systems is challenging. The complexity of these systems keeps growing and consequently the demand on the software increases. The software must control and monitor many processes in parallel, and deal with a large number of exceptional conditions that disrupt the regular control flow, which must be handled appropriately.
For this reason software engineers have to take care of many requirements:
- How to manage increasing complexity while keeping the quality and reliability in check?
- How to increase connectivity while ensuring cybersecurity?
- How to keep the costs down?
- How to guarantee the safety of the system?
- How to deal with software updates and maintenance?
With Dezyne – create, simulate, mathematically verify and automatically generate code for cyber-physical systems – these challenges become manageable.
Dezyne Language & IDE
Dezyne is a programming language with formal semantics aimed at control software (specifying the behavior of a system), such as found in embedded systems. Dezyne is devised with the regular software engineer in mind, a professional without a background in applying formal methods (mathematically rigorous techniques for the specification, development and verification of software and hardware systems).
Dezyne is an open plain text, domain specific language, used to design the structure and behavior of a software system with a syntax similar to that of common programming languages such as Java or C.
To stick to familiar and commonly used development environments, Verum has chosen to implement LSP for interfacing with commonly used IDE's such as VS Code and Emacs. On the basis of LSP other IDE's can be added.
Verification
Testing event driven control software is difficult. Testing time on hardware is expensive, so often software simulators on various levels of (hardware) details are created to mitigate these cost. However, the ultimate test is still the execution on the real hardware, and errors found during the final testing are very costly and time consuming to fix. Writing test cases for the software is tedious or even undoable, since a very large amount of execution scenarios (potentially several hundred thousand or even much more) have to be considered. As a result, due to economic reasons, only a small percentage of the possible execution scenarios are effectively tested in practice.
Even worse, a lot of scenarios cannot be checked with conventional testing because it is not possible to identify or reach them. Only while performing the verification with Dezyne, one can be sure that the whole space is being covered.
In addition, Dezyne helps you to identify the area where the issue occurs. Issues identified by Dezyne are, for example, livelocks, deadlocks and interface violations.
Validation and Exploration
The Dezyne simulator enables engineers to validate whether their specifications and designs behave as expected and whether the intended use cases have been implemented properly.
Engineers explore the behavior of a specification or design with the help of the simulator, which constructs a sequence trace that guides the user to step through the traces, examining the program flow, variables, events and responses.
Code Generation
Dezyne provides code generators for C++, C# and more. The generated code is verified, validated, and directly deployable.
Verum warrants that the generated code is equivalent to the verified models and therefore 100% defect-free.
Toolchain
Dezyne is one of the many tools that is being used in the software engineering lifecycle. To support the interoperability in the toolchain, Dezyne and the supported file format for storing model information are open. This means that another program can write to a Dezyne file, read a Dezyne file or interact with Dezyne directly.
An example is a process in which tools such as UML/ SysML are used, and the work saved in those tools is transformed into information stored in a Dezyne file. Subsequently Dezyne is able to verify and validate the results.
Prevent and eliminate defects
Dezyne will save you time and effort building your software. It is achieved by providing engineers with the ability to continuously "test" software specifications and designs, preventing entire classNamees of defects from occurring and ensuring that many of those that do, are quickly found and repaired.
Source code for the components specified, is generated directly from Dezyne. The result is a remarkable decrease in development effort and time, and a corresponding increase in process predictability and product quality.
Applying Dezyne
The reasons for applying Dezyne in your software process can vary. Some examples:
- New projects: An easy way to apply Dezyne is in case of a new/ greenfield module, project, or system.
- Refactoring: Dezyne is a great tool and method to help transform legacy code.
- Maintenance: A model describing a component is easier to update than many thousands of lines of code. Also, Dezyne manages the relations between models, which helps your understanding of the software, now and in the future.
- Safety: Capture the safety aspects of your system in models, and verify & validate them.
- Security: Make sure that you are in control of the behavior of your code by means of the rigorous verification which Dezyne supports.
