We are happy to announce Dezyne 2.19 which introduces data return, invariants, and directory support for verify and code. This release represents 258 commits over one year.

See the NEWS below for a brief summary.

Here is the Dezyne home page: dezyne.org

What's next?

In the next releases we would like to see:

• External functions and Global functions.
• New sequential simulator infrastructure with improved support for constraining interfaces, shared state, and debugging communcations labeled with external and defer.
• Support for early return and the deprecation of reply.
• Replace dzn traces with dzn test to enable end users to automate their functional or end to end tests.
• Performance improved parse infrastructure with respect to serialization, parse tree and abstract syntax tree related functionality: including language extensions and early editing feedback.
• Move blocking from the component to the interface.
• The unification of state and data at the language level.
• Composing specifications for verification from multiple interfaces separate from the component behavior.
• Verify these composed specifications both at the component as well as at the system level.

Enjoy!
The Dezyne developers.

Download

git clone git://git.savannah.nongnu.org/dezyne.git

Here are the compressed sources and a GPG detached signature[*]:
dezyne-2.19.0.tar.gz
dezyne-2.19.0.tar.gz.sig

Here are the SHA1 and SHA256 checksums:

3a3999d32543968c6715332bd71ca8831f6ac27e  dezyne-2.19.0.tar.gz  
aa43ab8014afb48c0912de96ce1b2c73cdc0d48a34f0a793760f0917de4773ca  dezyne-2.19.0.tar.gz

[*] Use a .sig file to verify that the corresponding file (without then .sig suffix) is intact. First, be sure to download both the .sig file and the corresponding tarball. Then, run a command like this:

gpg --verify .sig

If that command fails because you don't have the required public key, then run this command to import it:

gpg --keyserver keys.gnupg.net --recv-keys 1A858392E331EAFDB8C27FFBF3C1A0D9C1D65273

and rerun the gpg --verify command.

Alternatively, Dezyne can be installed using GNU Guix:

guix pull  
guix install dezyne

NEWS

Changes in 2.19.0 since 2.18.4

• Language

  • The concept of a predicate function, i.e., a boolean function consisting of a single expression without side effects, has been added.
  • A boolean implication operator => has been added.
  • Invariants have been added and can use both of these features.
  • An external type (data) can now be used as the return value of events and functions.

• Commands

  • A new command dzn exec has been added to run anything in a Docker container, such as, dzn exec ltsconvert ....
  • A new command, dzn hash has been added to produce a crpytographic hash of a dezyne file and its imports.
  • The dzn command has a new option: --version-number. This may simplify getting the version in environments where Dezyne is the only program in use that conforms to the GNU coding standards.
  • The dzn hello command has a new option: --runtime to display the (installed) location of the runtime.

• Parser

  • The dzn parse command has a new -D,--no-directives option, removing the need to use, know, or learn grep -v ^#.

• Code

  • Using --shell=model for a non-existent model, an imported model, or a non-system model now produces an error and exits unsuccessfully.
  • When generating C++ code, makefile dependencies are generated.
  • The dzn code command now supports generating code for multiple files, and for directories.
  • The dzn code command has a new -t,--touch-empty-files option to touch empty C++ execution units for consistency.

• Verification

  • The --threads option of mCRL2 202307.1 can now be used via dzn --threads=N.
  • When verifying multiple files or directories, imported models are skipped to prevent duplicate verification.

• Noteworthy bug fixes

  • Trivial deadlocks in a dzn graph procduced LTS or state-diagram in blocking external and collateral blocking defer contexts have been fixed.

  • The verify command now also respects the --model=MODEL selection when MODEL is an interface.

  • Using an expression as defer argument is flagged as an error by the parser.

Thanks to everyone who contributed to this release:

182 Janneke Nieuwenhuizen  
 38 Paul Hoogendijk  
 38 Rutger van Beusekom

For changes in the previous release see Dezyne release 2.18.4.

About Dezyne

Dezyne is a programming language and a set of tools to specify, validate, verify, simulate, document, and implement concurrent control software for embedded and cyber-physical systems.

The Dezyne language has formal semantics expressed in mCRL2 developed at the department of Mathematics and Computer Science of the Eindhoven University of Technology (TUE). Dezyne requires that every model is finite, deterministic and free of deadlocks, livelocks, and contract violations. This is achieved by means of the language itself as well as builtin verification through model checking. This allows the construction of complex systems by assembling independently verified components.

Dezyne is free software, it is distributed under the terms of the GNU Affero General Public Licence version 3 or later.

The Dezyne research and development on the language and command line tooling, also known as the Dezyne core, is the responsibility of Reasonable Sourcery commisioned by Verum.

About Verum

Verum, the organization behind the Dezyne language, is committed to continuing to invest in the language for the benefit of all its users. Verum assists its customers and partners in solving the software challenges of today and tomorrow, by offering expert consultancy on the application of the Dezyne language and the development and use of its tools, as well as on Verum's commercial tools like Verum-Dezyne's IDE support based on the LSP (Language Server Protocol), interactive integrated graphics, interactive simulation, (custom) code generation and (custom) runtime library support.

About Reasonable Sourcery

Reasonable Sourcery is the cooperative research and development spin-off organization of Verum.