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
© 2007 This document authored, composed and
maintained by: Valeriy V. Vyatkin
All rights reserved.