Model – Checkers for Net Condition/Event Systems

Net Condition/Event Systems is a formal graphical language that fits well for modelling and verification of distributed embedded and control systems. The models can be formally analysed using special software tools called model-checkers.

SESA

SESA is a command line software tool for the analysis of Signal-Net Systems. SESA was developed in 1999-2002 at Humboldt University of Berlin (Germany) by Professor Peter Starke and his group. SESA was developed in a collaborative R&D project “Function Blocks” conducted together with the group of Professor Hans-Michael Hanisch at Martin Luther University of Halle (Germany). The project was funded by DFG  –  German  Research Foundation.
After the retirement of Professor Starke, SESA support by Humboldt University has been discontinued.  A limited support  is intended to be provided by Valeriy Vyatkin of  The University of Auckland (New Zealand).

Download original SESA version 1.6  (ZIP, 367 KB)
Download SESA built 1.7 Auckland 2008 (ZIP, 184 KB)
Download short documentation of SESA (PDF, 210 KB)
Download ‘Analyzing Signal-Event Nets’ – a longer document on NCES (PDF, 1MB)

Visual Verifier (ViVe)

ViVe is an interactive graphical model-building and analysis tool. The main goal of ViVe is to assist in building models of large and complex distributed systems. Development of an earlier prototype of ViVe called iMATCh was started by Valeriy Vyatkin in 2003.  ViVe can be used with SESA and/or standalone.

For more details on ViVe please visit the following link.

Download guide on modelling and verification of automation and control systems using NCES and ViVe
Download documentation on Visual Editor of NCES
Download guide to examples supplied with ViVe