Verum develops Dezyne, a component-based language and toolchain for the development of stateful, concurrent and event-driven software. It makes interfaces, message interactions and component behaviour explicit before implementation.
Formal Software Engineering
Verum DezyneFormal Verification & Model-Based Engineering for Concurrent Software
Dezyne is a component-based language and toolchain for specifying, simulating, formally verifying and generating implementation code for concurrent, event-driven software in embedded and cyber-physical systems.
DezyneFormal VerificationConcurrent SoftwareSimulationCode GenerationBehavioural Models
Verum
TECHNOLOGY PARTNER · INDIA
Verum Dezyne technical evaluation and application support in India
Primionics supports engineering teams in India evaluating Dezyne for concurrent embedded software, component interaction modelling, formal verification and model-driven implementation workflows.
Technology Overview
Formal methods for concurrent, event-driven software
Dezyne uses formal semantics and automated model checking to analyse interface and component behaviour. Verification checks include deadlock, livelock, illegal actions, unreachable behaviour, determinism and adherence to defined behavioural contracts.
Verified components can be composed into larger systems, inspected through system, state and sequence views, simulated interactively and translated into implementation code. This brings formal analysis closer to software architecture and implementation rather than treating verification as a separate late-stage activity.
Dezyne Engineering Workflow
Model, verify, simulate and generate implementation code
Dezyne Modelling Language
A domain-specific language for interfaces, components, ports, events and behavioural contracts. The language expresses interfaces, allowed event sequences and component behaviour in a form suitable for formal analysis.
Explore DezyneFormal Verification Engine
Exhaustive analysis of reachable behaviour with diagnostic traces for detected defects. Model checking analyses reachable behaviour and returns diagnostic traces when an interaction violates the model.
Explore DezyneSimulation & Visualisation
Interactive execution helps engineers understand event flow, component coordination and design consequences.
Explore DezyneCode Generation
Generation of implementation code from verified component models for supported programming languages. Verified models can be transformed into implementation code, reducing the gap between analysed design and deployed software.
Explore DezyneDocumentation Tooling
Model-derived documentation for interfaces, components and verified behaviour. Generated views and model-derived documentation support reviews, communication and maintenance.
Explore DezyneFormal Verification Capabilities
Analyse component interactions before system integration
Dezyne applies formal semantics and model checking to component and interface behaviour, helping engineering teams reason about concurrency and event ordering at design time.
Behavioural contracts
Define provided and required interfaces, permitted event sequences and component behaviour explicitly so assumptions between software components are reviewable and verifiable.
Deadlock & livelock analysis
Verify reachable component behaviour for coordination failures that can leave a concurrent system blocked or permanently busy without serving required interactions.
Illegal, unreachable & deterministic behaviour
Check models for illegal actions, unreachable behaviour and determinism, with diagnostic traces that help engineers identify the sequence leading to a verification failure.
Simulation & code generation
Use system, state and sequence views to inspect behaviour, then generate implementation code for supported backends to reduce the gap between verified design and delivered software.
Applications
Engineering Value of Formal Verification
Concurrent component design
Define interfaces, components and interactions for event-driven and state-rich embedded software. Explicit interfaces and behavioural contracts make communication assumptions visible before implementation and system integration.
Deadlock and interaction analysis
Explore reachable behaviour exhaustively to detect concurrency and protocol defects before integration. Exhaustive exploration can reveal illegal event sequences and coordination errors that scenario-based testing may not expose.
Safety-related software architecture
Create precise behavioural models and verification evidence for high-integrity development workflows. Verified component behaviour provides stronger design evidence and a clearer basis for implementation, review and change control.
Controller and equipment software
Develop coordinated control logic for machines, medical systems, transport equipment and complex products. The approach is useful where multiple components coordinate actuators, sensors, operating modes and fault-handling logic.
Frequently Asked Questions
Technical questions about Verum Dezyne
What is Verum Dezyne?
Dezyne is a component-based language and engineering toolchain for modelling concurrent software behaviour, formally verifying component interactions, simulating event sequences and generating implementation code from verified models.
How is formal verification in Dezyne different from conventional testing?
Testing evaluates selected scenarios. Dezyne model checking analyses the reachable behaviour represented by the model and can identify interaction defects that are difficult to expose through scenario-based testing alone.
What properties can Dezyne verify?
Dezyne verification checks include properties such as deadlock, livelock, unreachable behaviour, illegal actions, determinism and adherence to defined interface contracts. The exact analysis applies to the behaviour represented in the Dezyne model.
Can Dezyne generate implementation code?
Yes. Dezyne includes code-generation capabilities that transform verified models into implementation code for supported language backends, helping maintain a closer connection between analysed behaviour and implementation.