EST 1st Edition

Overview

Features:

• [all] based on Biddy BDD package, includes API functions for Tcl/Tk GUI called My Interface
• [pa] parser for simple textual representation of processes, encoding and decoding of processes, decoding of compositons
• [versis] parallel composition, checking strong equivalence, observational equivalence, and testing equivalence, renaming, hiding and forbiding actions, searching for deadlocks and divergences
• [mc] ACTL and ACTL-W model checking

Previews: license, menu, dialog, colors, an example of verification.

Acknowledgement: Project EST 1st Edition has been entirely realized during the research process on Faculty of Electrical Engineering and Computer Science in Maribor, Slovenia. The project has been partly supported by the Slovenian Ministry of Science and Technology in years 1993-1995 and 1996-1998 under grants J2-5122-0796-95 and J2-7495-0796-96, respectively. From 1995-1997 the project has been partly supported by COST 247 project Verification and Validation Methods for Formal Descriptions.

Download

Modules from EST 1st Edition and EST 2nd Edition are not interchangeable, i.e. EST 2nd Edition release-2-0 is not an upgrade of EST 1st Edition release-1-x.

In October 2006, we created a SVN repository for EST 1st Edition project.

EST 1st Edition - release 1.5.1 (Jul 30, 2007)

• [all] modul gui added which covers functions removed in My Interface v0.99
• [all] modul bdd added which covers functions removed in Biddy v0.99
• [all] bison (for Win32) updated to release 2.1
• [all] flex (for Win32) updated (still 2.5.4a)
• [all] makefiles improved and simplified

• est-1ed-1-5-1-source.zip, Jul 30, 2007, SVN revision 15
• est-1ed-1-5-source.zip, Jul 19, 2007, SVN revision 14

• est-1ed-1-5-1-Linux-mish.zip (i686, GNU/Linux, Tcl/Tk),
• est-1ed-1-5-1-Linux64-mish.zip (i686-64, GNU/Linux, Tcl/Tk),
• est-1ed-1-5-1-SunOS-mish.zip (sun4u, Solaris, Tcl/Tk),
• est-1ed-1-5-1-Win-mish.exe (i686, Win32, Tcl/Tk).

• est-1ed-1-5-1-Linux.zip (i686, GNU/Linux),
• est-1ed-1-5-1-Linux64.zip (i686-64, GNU/Linux),
• est-1ed-1-5-1-SunOS.zip (sun4u, Solaris),
• est-1ed-1-5-1-Win.zip (i686, Win32).

EST 1st Edition - release 1.4 (Jun 13, 2007)

• [all] sources cleaned, makefiles fixed
• [versis] implemented renaming, hiding and forbiding actions
• [versis] implemented searching for deadlocks and divergences

• est-1ed-1-4-source.zip, Jun 13, 2007, SVN revision 9

EST 1st Edition - release 1.3 (Jan 15, 2007)

• [all] mingw and sunos specific files removed from the project
• [all] makefiles improved

• est-1ed-1-3-source.zip, Jan 15, 2007, SVN revision 7

EST 1st Edition - release 1.2 (Oct 20, 2006)

• [all] improved dialogs
• [all] supported tcl/tk 8.4
• [all] makefiles improved, OS is now automaticaly recognized
• [all] bdd package becomes a separated project called Biddy
• [all] FSF rules to make program free are more strictly considered

• est-1ed-1-2-source.zip, Oct 20, 2006, SVN revision 4

EST 1st Edition - release 1.1 (Sep 16, 2003)

• [mc] standard ACTL model checking

• [pa] parser for process algebra is now more roboust
• [pa] added simple recovery on syntax errors
• [mc] semantics of ACTLW fixed
• [mc] W is used instead of UU for unless
• [mc] parser for ACTL/ACTLW is now more roboust
• [mc] added simple recovery on syntax errors

EST 1st Edition - release 1.0

• In 1992, Ales Casar and Robert Meolic implemented the first version of BDD package. It was written in Pascal and ran on VAX 4000-600. In 1994, Ales Casar rewrote the package in C.
• In 1995, Ales Casar implemented CTL model checker on finite state machines. His package is not a part of EST, but it served as a basis for ACTL model checker.
• In 1996, Mirjam Sepesy Maucec implemented a package for description and formal verification of concurrent systems with a simple CCS-like process algebra. Her package was called Versis (VERifikacija SIStemov) and was capable of performing basic operations on processes, parallel composition of processes, and checking strong and observational equivalence between processes. It was written in C and ran on HP Workstation.
• In 1999, Robert Meolic formed the first version of EST package. It was based on BDD package and Versis package. The code from BDD package had been purified and transformed into module called bdd. The code from Versis package had been completelly rewrited and splited into two modules called pa and versis. Many improvements had been done and a lot of features had been added in comparison with the original packages. The most important is checking of testing equivalence between processes. The first version of EST, which is now called EST 1st Edition, also contained simple ACTL model checker and Tcl/Tk GUI called My Interface.
• Afterwards, many releases has been formed and all of them was stated to be version 1.0. In August 2003, a CVS repository for EST package was created. Moreover, all packages have been reorganized and partially rewrited. All history notes (which were not very useful) have been deleted. The last release, which was numbered as version 1.0, was capable of representation of concurrent systems with LTSs, parallel composition of LTSs, strong, observational and testing equivalence checking between LTSs and ACTLW model checking on LTSs.