https://www.gravatar.com/avatar/460e16e9610c376ebf7bb398669d81ac?s=240&d=mp

Joran Jessurun

Dezyne: Implementing and Testing Components

Introduction In this article, I will present an implementation for a motor in Dezyne. The implementation will build upon the MotorGlue introduced in a previous article, incorporating error handling and an asynchronous protocol. Firstly, I will introduce the necessary interfaces for composing the desired behavior and present the Motor interface. Subsequently, I will provide an implementation for the Motor interface, referred to as MotorImpl. Following that, I will discuss the aspects that require testing and those that are already handled by the Dezyne verification.

Dezyne: Creating Glue Code and Testing

Introduction Handwritten code is the most error prone part of a Dezyne project. Some often-seen mistakes are: Throwing an exception on the Dezyne thread. Mistakes with the difference between asynchronous and synchronous events. Wrong reply value. Multi-threading mistakes. Many of these mistakes are related to not strictly following the Dezyne interface. Besides that, the functional behavior of the handwritten code could also contain bugs. In this article I will introduce the handwritten code for connecting the Dezyne models to the underlying code to control a Motor and show how to rigorously test it.

Dezyne: From dzn.async via Defer to Async

Introduction Sometimes a synchronous interface needs to be converted into an asynchronous interface. The way to do this in Dezyne from Verum has changed over time. I will first introduce two interfaces, one asynchronous and one synchronous. Then I will show different ways to make a component that provides the synchronous and requires the asynchronous interfaces. Unless stated otherwise, all examples are made using Dezyne 2.18. From Synchronous to Asynchronous Calls One of the often needed behavioral transformations is converting a synchronous interface to an asynchronous one.

Dezyne 2.18: Implicit Interface Constraints and Shared Interface State

Introduction Dezyne is a domain specific language with code generation and verification tools developed by Verum. It is used to describe and verify event based systems using state machines. In this article I will introduce some basic concepts of Dezyne. I will start by giving examples of two interfaces and show a basic implementation of a component. Then I will introduce implicit interface constraints which is introduced in Dezyne 2.17 and shared interface state which is introduced in Dezyne 2.