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.
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.
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.
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.
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.