Verum Dezyne

Code first without downsides

Download

Join the community of software engineers and scientists who use Dezyne to develop flawless software for embedded and cyber-physical systems.

Trials are free and we don’t ask things like credit card details.

Follow this link to download and install Verum Dezyne on your desktop.

Verum Dezyne: a power language

Verum Dezyne uses Dezyne, an open-source, plain text, domain specific language, 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. It allows to generate directly deployable code such as C, C++ and C#.

It makes hard things as formal methods very simple, in the basis it works the same way as a grammar checker in a word processor. Verum Dezyne creates confidence in the result of your work.

Verum Dezyne Quick Start

Verum Dezyne comes as a convenient ready-to-use package, equipped with LSP and plenty of powerful GUI tools. Verum provides rich documentation, tutorials and working examples. Dezyne is available in two editions:

  • Visual Studio Code Extension: Simply download the extension from the Marketplace, link the Dezyne package directory, create a .dzn file and access all Dezyne tools through the right-click context menu.
  • Command-line tool: It offers extensive configuration options, designed for complex project build and CI/CD tool-chains

Features

Dezyne Language

Dezyne is an open, C-like language for developing complex embedded software. It uses a "Design by Contract" approach, serving as an intermediary between formal models and target source code. Dezyne's building blocks are interfaces and components, enabling the creation of complex systems through composition. Its interactions are visualized as state diagrams, allowing for easier control flow analysis.

Dezyne IDE

Verum Dezyne supports modern development environments such as VS Code through the Language Server Protocol. The VS Code extension for Dezyne also provides access to Dezyne commands such as “Code”, “Simulate” and “Verify” as well as interactive system, sequence, and state diagrams.

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 model and entirely free of defects.

Verification

Verum Dezyne uses model checking to identify bugs and design flaws such as race conditions, logic jams, unhandled exceptions/interrupts. Verification is treated as a standard tool like compilation. Dezyne can verify interfaces and components separately for fast issue resolution. Small changes can be checked in seconds, which streamlines software development and improves code quality.

Rapid Prototyping: Code First

Dezyne encourages a code first approach, by supporting the start of development even when the requirements and specifications are not detailed in full yet. Single functionalities can be rapidly implemented, simulated and verified for potential pitfalls. A working prototype, as a separate, atomic component, can be easily incorporated into a larger system. Allowing short iterations, Dezyne supports a highly agile software development process.

Bug Traceability

Verum Dezyne provides precise feedback when the verification detects bugs, including the issue location and steps to reproduce it. The sequence diagram offers a visual representation of the system's state and factors leading up to the error. Dezyne can reveal intricate fault-scenarios that are often hard to detect in complex systems.

Validation and Exploration

Verum Dezyne offers graphical tools to validate and test the structure of the system and its specification and behavior. The Sequence Diagram lets users simulate the system, inspect variables, events and responses. The State Diagram explores every possible system state and its contributing factors. Dezyne's batch mode is compatible with modern CI/CD toolchains, enabling seamless testing and validation.

Applicability in the Toolchain

Verum Dezyne provides formal verification for all aspects of a system, applicable in any project stage, ensuring compliance with standards, reliability and performance. It offers a reliable retrofit/ maintenance solution by translating legacy code, enhancing maintainability and transparency in component relations. Dezyne's safety and security features validate system models, making it ideal for meeting safety standards and tackling security breaches.

Join our Community

Discuss, learn, find advice, give advice, and ask your questions: about Dezyne and the concepts supporting Dezyne. Our forum is a platform, freely accessible for everybody that is interested in the Verum products.

Join Community

Keep me informed

What our users say

Dezyne reduces the extremely complex matter of formal verification to the role of a colleague who sits next to you and shows you all the bugs in an understandable form.

Dezyne really builds trust and gives me this nice feeling of self-confidence while coding.

Even if the requirements/ specifications are not finally defined, I can still start with coding and when Dezyne stops complaining I'm getting code that is reliable and actually works.