EST 1st Edition
Overview
Project: Efficient Symbolic Tools - 1st Edition
Synopsis: EST 1st Edition is a toolbox for the formal verification of concurrent systems
Administrator: Robert Meolic (robert.meolic@um.si)
Authors: Robert Meolic, Tatjana Kapus, Aleš Časar, Mirjam Sepesy Maučec, Zmago Brezočnik
History: started in 1992, first release in 1999
COBISS-ID: 5626902 (this number is used by Slovenian libraries)
Features:
[all] based on BDD package Biddy, 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 ACTLW model checking
. . .
EST 1st Edition - release 1.5.x
The most important changes from release 1.4
[all] Biddy is isolated and does not belong to EST project anymore
[all] Biddy is now dynamically linked (v1.3 is required for release 1.5.4)
[all] modul gui added which covers functions removed in My Interface
[all] modul bdd added which covers functions removed in Biddy
[all] on MS Windows, bison and flex from MINGW distribution are used
[all] on MS Windows, EST is now compiled with MINGW 5.1.4 (gcc 3.4.5)
[all] improved packaging on MS Windows (using 7zsd.sfx)
[all] added Makefiles for Mac OS X (Darwin)
[all] makefiles improved and simplified
[all] adapted for 64-bit architectures
[all] added debian and rpm packaging
[all] Tcl/Tk related files are now compiled with Tcl Stubs
[all] all modules are using TCL stubs (to support changes in Tcl 8.5.10)
[all] added main program (it can be used instead of wish)
[all] added cmdsh mode (tcl api without mish gui)
[bdd] added experimental drawing of BDDs using bddview
Download sources
est-1ed-1-5-4-source.zip, Apr 25, 2015, SVN revision 103
est-1ed-1-5-3-source.zip, Oct 28, 2014, SVN revision 96
est-1ed-1-5-2-source.zip, Oct 15, 2010, SVN revision 23
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 1st Edition - release 1.4 (Jun 13, 2007)
The most important changes from release 1.3
[all] sources cleaned, makefiles fixed
[versis] implemented renaming, hiding and forbiding actions
[versis] implemented searching for deadlocks and divergences
Download sources
est-1ed-1-4-source.zip, Jun 13, 2007, SVN revision 9
. . .
EST 1st Edition - release 1.3 (Jan 15, 2007)
The most important changes from release 1.2
[all] mingw and sunos specific files removed from the project
[all] makefiles improved
Download sources
est-1ed-1-3-source.zip, Jan 15, 2007, SVN revision 7
. . .
EST 1st Edition - release 1.2 (Oct 20, 2006)
The most important changes from release 1.1
[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
Download sources
est-1ed-1-2-source.zip, Oct 20, 2006, SVN revision 4
. . .
EST 1st Edition - release 1.1 (Sep 16, 2003)
The most important changes from release 1.0
[pa] parser for process algebra is now more roboust
[pa] added simple recovery on syntax errors
[mc] added standard ACTL model checking
[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
Sources not available
EST 1st Edition - release 1.0 (1999 - 2003)
All version from 1999-2003 have been numbered as version 1.0. The last one 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.
Sources not available
History notes
The project EST 1st Edition is now marked as matured, because we are not planning to add new features (others than GUI improvements). However, there is still a lot of work to do, including writing documentation, cleaning up the code, adding new examples etc. Hence, the project is not closed, yet.
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 local SVN repository for EST 1st Edition project (last version in this repository was labeled as revision 23). In October 2014, we created SVN repository at Savannah. First version in new repository is labeled as revison 95. Notes from local repository have not been passed to new repository.
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.
