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