PROTEUM/FSM (Program Testing Using Mutants)
Jose Maldonado and Dr. Marcio Delamaro of the University of Sao Paulo at Sao Carlos in Brazil.
website not identified
Verification, Validation, and Testing
FSM-based Test Sequence Generator (TSG 3.0).
University of Ottawa, Hasan Ural et al
http://www.site.uottawa.ca/~ural/tsg/intro_fr.html
CS,DS generation.
Not available
also se http://www-cad.eecs.berkeley.edu/~tah/mocha/ Mocha model checker
The Assertion Based Testing Tool: ADL2
Open Group
ADL, or the Assertion Definition Language, is a formal grammar for describing the behavior of interfaces. Assertions are written as a description of how the function behavior is affected by the input state, and the resulting changes on the output state.
Unix. Free (Open Source tm).
Autolink - Automatic Test Generation from SDL Specification
Institute for Telematics (aslo SAMSTAG tool etc)
http://www.itm.mu-luebeck.de/english/research/specification/autolink/index.html
SDL is a CEFSM language.(for TAU)
TestComposer
(an SDL test generator from Object Geode SDL tool of Telelogic)
Automatic Test Generation from Formal Specifications
Dr. Paul E. Black
http://hissa.nist.gov/~black/FTG/autotest.html
An mutant based test generation by modelchecker project.
Free download.
GOTCHA/TCBeacns
IBM (Haifa)
http://www.haifa.il.ibm.com/projects/verification/gtcb
Developing, executing and organizing function tests directed
against Application Program Interfaces (APIs) and software protocols written
in Java, C or C++. GOTCHA is the tool kit's engine for generating an abstract
test suite for a finite state machine (FSM) driven by a coverage model.
The finite state machine is described in a high level language for modeling
concrete systems.
Côte de Resyste
University of Twente (UT) and Eindhoven University of Technology (also a stochastic modelcheker)
http://fmt.cs.utwente.nl/projects/CdR-html
A project related to test generation. Free download of a ConfCase case
study.
FSM Library
AT&T
http://www.research.att.com/sw/tools/fsm
General-purpose finite-state machine software tools.
Minimization, determinization, projections, products etc on weighted
automata and traducers
C library and utilities
Unix, C API
Free for non-commercial use
http://www.research.att.com/sw/tools/fsm/description.html
The FSM library is a set of general-purpose software tools available for Unix, for building, combining, optimizing, and searching weighted finite-state acceptors and transducers. Finite-state transducers are automata for which each transition has an output label in addition to the more familiar input label. Weighted acceptors or transducers are acceptors or transducers in which each transition has a weight as well as the input or input and output labels. Generality: to support the representation and use of the various information sources in speech recognition
Modularity: to allow rapid experimentation with different representations
Efficiency: to support competitive large-vocabulary recognition using automata of
more than 10 million states and transitions.
The mathematical foundation of the library is the theory of rational power series, which
supplies the semantics for the objects and operations and creates opportunity for
optimizations such as determinization and minimization.
Intergrated with the free visualization tool
Graphviz - open source graph drawing software
FSA Utilities toolbox:
Gertjan van Noord
Vakgroep Alfa-informatica & BCN
Rijksuniversiteit Groningen
http://grid.let.rug.nl/~vannoord/papers/fsa/fsa.html
a collection of utilities to manipulate finite-state automata and finite-state transducers.
SICStus Prolog
free (GNU General Public License)
ftp://ftp.let.rug.nl/pub/prolog-app/FSA/
http://www.let.rug.nl/~vannoord/Fsa/
Manipulations include determinization (both for finite-state acceptors and finite-state
transducers), minimization, composition, complementation, intersection,
Kleene closure, etc. Furthermore, various visualization tools are available
to browse finite-state automata. The toolbox is implemented in SICStus
Prolog.
Xerox Finite-State Compiler
Xerox MLTT team
http://www.xrce.xerox.com/research/mltt/fst/
transforms a regular expression into the minimal epsilon-free deterministic automate
(3 min limit) web application. Web pages of other Xerox FSM tools are
not identified.
The Edinburgh Speech Tools Library
Centre for Speech Technology Research at the University of Edinburgh.
http://www.cstr.ed.ac.uk/projects/festival/
C++
Distributed within Festival Speech Synthesis Tool 1.4.0 (free)
ftp://ftp.cstr.ed.ac.uk/pub/festival/1.4.0/
Ptolemey II
Department of EECS, UC Berkeley
http://ptolemy.eecs.berkeley.edu
Ptolemy II is a set of Java packages supporting heterogeneous, concurrent modeling and design. Allows visualization/modeling hierarchical extended finite state machine, hybrid machines, CSP, dataflow etc. Graph-theoretic manipulations.
free download
Flap/JFlap (Formal Languages and Automata Package),
Susan H. Rodger, Dan Caugherty, Mark LoSacco, David Harrison, and Greg Badros.
http://www.cs.duke.edu/~rodger/tools/tools.html
an educational tool for designing and simulating several variations
of finite automata, pushdown automata, and Turing machines. FLAP and other
tools are available via anonymous ftp. he
Java version of FLAP, is now available (Aug. 1999). New features in 3.1
include regular expressions, including conversions of regular expressions
to NFA, and DFA to regular expressions. New features from 3.0 include several
conversions from onerepresentation to another. The conversions are nondeterministic
finite automaton (NFA) to deterministic finite automaton (DFA), DFA to
minimum state DFA, NFA to regular grammar, regular grammar to NFA, nondeterministic
pushdown automaton (NPDA) to context-free grammar (CFG), and three algorithms
for CFG to NPDA. Two of the CFG to NPDA conversions are useful in studying
LL and LR parsing. In addition, you can now slide the labels along the
arcs and stretch the loops (grab the dot on top) for more room. To get
on the JFLAP mailing list for notices, send email to [email protected].
DAG-O-Bert: A Tool for Designing and Profiling Finite-State Automata,
Olivier Baby
http://www.cs.brandeis.edu/~obaby/publications.html
Specification of NFA with an elegant high level language (augmented
FSM), which supports hierarchical constructs and type definition.
Innovative visualization and analysis of executions of an input sequence.
Grapher
A graphical tool for designing CSM automata
http://www.ii.pw.edu.pl/~ratajcza/csm/grapher/grapher.html
The Institute of Computer Science Faculty of Electronics and Information Technology,
Warsaw University of Technology.
Composing flat and hierarchical automata,
drawing states, assigning state's name, product and description,
drawing transitions between states, assigning transition's name, condition
and description,
drawing nested automaton-states, specifying plug-in and plug-out states,
connecting transitions to nested automaton's plug states,
printing automaton, copy&paste states and transitions,
copying subset of states to clipboard as CXL text,
drag&drop states and transitions,
view and change automaton formulas,
support for CXL language.
free download
The Finite State Machine Explorer
a third year undergraduate project (1995-6)
http://www.belgarath.demon.co.uk/java/fsme.html
visualization/simulation
a third year undergraduate project (1995-6)
java
Interactive Graph Drawing
Úlfar Erlingsson, in collaboration with Mukkai Krishnamoorthy.
http://www.cs.rpi.edu/projects/pb/graphdraw
a Java-based system for doing interactive graph drawing on the WWW, inspired by Arthur van Hoff's early GraphLayout Java
demonstration applet
The Formal Languages Environment AUTOMATA
Dipartimento di Scienze dell'Informazione
Università degli Studi di Milano
Maria Alberta Alberti
http://homes.dsi.unimi.it/~alberti/colos/automata.html
AUTOMATA is a tool for modelling automata and experimenting with
grammars. The environment deals with:
finite state automata - FSA, both deterministic and non deterministic
push-down automata - PDA, both deterministic and non deterministic
finite state transducers, Moore and Mealy machines
grammars regular expressions pattern matching, a module to generate
automata given a pattern
matching problem. It provides the visualisation of some important algorithms,
such as the
transformation of non deterministic automata into deterministic ones
or the
minimisation. The automata are defined by entering their state diagram
in a
graphic editor or by giving a grammar. An example of a finite state
automaton, accepting strings of even number of a's and b's, and its
equivalent regular grammar.
Interactive Animation Of FSA
Tom Dunn
http://www.ccs.neu.edu/home/tdunn/COM1350/honors/
Deus ex Machina
Nick Savoiu
http://www.ics.uci.edu/~savoiu/
Animation/simulation FSA, Linear-Bounded Automata, Pushdown-Stack, Register,
Turing and Vector Machines
Automata Research Tool
Parshev
Saratov State University
http://www.ssu.runnet.ru/english/personal/papshev.htm (MS DOS)
http://prcnit.ssu.runnet.ru/English/ScienceLab/
CGI (www)
free
Strong connection for automata
Automaton graph and its connected components visualization
Automorphism group
Congruence lattice
Tolerance lattice
Subautomata lattice
Save information about automata into Database and restore from it
Compatible linear orderes
ASSIST: A Simple Simulator for State Transitions
EILEEN F. S. HEAD
Master thesis
Autograph
http://pauillac.inria.fr/~cheno/autograph/
Laurent Chéno
La bibliothèque autograph vous permet de manipuler des automates
finis.
Remarque : elle utilise init_vect, de la version 0.74 de Caml Light.
Que vous pouvez diffuser et utiliser librement à condition de
joindre le fichier lisezmoi à votre distribution.
AutomataX
Michel Quercia
http://caml.inria.fr/polycopies/quercia/index-fra.html
Utilitaires pour manipuler des arbres, graphes et automates en Caml-Light
parallele
A Tree Automata Library
http://www.irisa.fr/lande/genet/timbuk/
an OCaml library
RXan interpreter for Rational Tree Languages
http://www.informatik.uni-leipzig.de/~joe/rx/
RX is a system that knows about regular tree grammars, finite tree automata,
and rational tree expressions. You may feed some regular tree grammars
to my RX interpreter and do some computations. See the online examples,
and edit.
The Java Computability Toolkit (JCT)
http://humboldt.sunyit.edu/JCT
contains a pair of graphical environments for creating and simulating NFAs, DFAs, and high level Turing Machines. JCT is written in 100% Java and makes heavy use of the new JFC Swing components. It is designed to run as an
application or applet on any platform supporting either:
...1. ...JDK 1.2
...2. ...JDK 1.1.7 and Swing 1.1.
3. JDK 1.1.7 (or lower) and Swing 1.0.3 (or lower)
..4.... Java Plugin w/ either 1.1.x or 1.2 JRE (if run in Applet mode)
When JDK1.2 compliant browsers are released plugin instalation will not be required to run JCT as an applet.
Finite Automata Environment: The Finite Automata Environment allows
a user to create and simulate multiple NFAs and DFAs in cascading
internal windows.
The following unary operations are allowed on FAs:
Convert To DFA, Minimize, Complement, Kleene Star.
The following binary operations are allowed on FAs:
Intersection, Concatenation, Union.
The Finite Automata Environment also features:
Compute on a given input: Types in a string and send it to the NFA/DFA
for computation. If the string is accepted a list is generated
Displaying the transitions used in the (or one of the) optimum [shortest]
acceptance path.
Trace acceptance path. If a string is accepted as the result of a Compute
the user can choose to graphically walk through each configuration
of the optimum acceptance path taken.
A Graph Representation.can be generated of any DFA or NFA.
Transition Grouping. Transitions which have the same "from" and "to"
states are grouped together to reduce screen clutter. Each transition
is separated into its own boxe and can be removed or modified without
affecting other members of the group.
Moveable Transitions. Each transition group can be automatically positioned
by JCT or manually positioned by the user.
Printing. Grabs an image of the current Finite Automata and prints
it along with Author info.
Undo. One level of undo.
Save and Load. Finite Automata can be saved and loaded locally.
The Glace System
The goal of the Glace is the simulation/visualization of automata networks. The automata (nodes) can be whatever: particles, atoms, molecules, neurons, electronic components, widgets, computers, X clients/server, people, ...
Glace can be also used as an universal easy to use 2D/3D drawing and presentation tool.
Features
The visalisation is done in 3d using Mesa (OpenGL API).
User programmed function/visualization is done in C++, the resulting
shared object can be dynamically loaded into glace.
Offscreen buffer selection mechanism is used for handling of the mouse
events (based on OSMesa). Every object of arbitrary complex shape under
arbitrary transformation can receive mouse and keyboard events (is
widget in window terminology). This mechanism gives 3d interactivity a
new
meaning. Multiple camera support, each with different lighting and
OpenGL model.
C++, Linux (i386).
Grail+
Department of Computer Science, University of Western Ontario, Canada
http://www.csd.uwo.ca/research/grail
http://www.cs.ust.hk/~dwood/grail/index.html
Grail is a symbolic computation environment for finite-state machines, regular expressions, and other formal language theory objects. Using Grail, one can input machines or expressions, convert them from one form to the other, minimize, make deterministic, complement, and perform many other operations. Grail is intended for use in teaching, for research into the properties of machines, and for efficient computation with machines. Grail is written in C++. It can be accessed either through a process library or through a C++ class library. Version 2.4 of Grail enables you to manipulate parameterizable finite-state machines and regular expressions. By `parameterizable', we mean that the alphabet is not restricted to the usual twenty-six letters and ten digits. Instead, all algorithms are written in a type-independent manner, so that any valid C++ base type and any user-defined type or class can define the alphabet of a finite-state machine or regular expression. Version 2.4 of Grail supports Mealy machines.
http://www.cs.ust.hk/~dwood/grail/index.html
msdos/unix/mac and others
free for non-commercial use
There is an ongoing project on test generation with Grail.
Another Finite State Machine Simulator (EH9-1)
http://watson2.cs.binghamton.edu/~tools/fsm/fsmdoc.html
Another Finite State Machine Simulator java application is a tool designed to aid students in learning how FSM and NFA work. The students create a description of a FSM in a textfile which is read by the program. The main program runs in graphics mode. There is text mode option which allows for easy grading. Examples of FSM and DFA machines based on Hopcroft and Ullman's text are included.
Finite State Machine Simulator by Kyril Faenov
http://www.iamexwi.unibe.ch/studenten/mguenter/demos/Antenna/Description
State Machine Simulator allows user to edit in a drag-and-drop fashion
a finite state machine and simulate, step-by-step its execution with specified
input string of tokens. It allows 10
states and 26 different tokens.
SIMFSM - Finite State Machine Simulator
http://esng.dibe.unige.it/netpro/PagineLocali/SimFsm.htm
SIMFSM is a Finite State machine Simulator developed by ESNG-DIBE University of Genoa for learning purposes.
SIMFSM runs under Windows 3.1, Windows 98, Windows NT 4 and Windows 95.
free
TM simulator
http://www.igs.net/~tril/tm/tm.html
Bandera
www.cis.ksu.edu/santos/bandera
Software Model Construction for Finite-state machines.. Bridging the
semantic gap between FSM and non-finite-state software systems (Java).
InVeSt (Invariants Verification System)
VERIMAG (see also TGV, IF), Univ. of Kiel, SRI
http://www-verimag.imag.fr/~async/INVEST
Name: InVeSt
Main Functionalities: Verification of invariance properties of infinite
state systems
Derived Functionalities:
Automatic generation of invariants
Compositional computation of abstractions
Reachability analysis of lossy communicating systems
PAX
Parameterized systems Abstracted and eXplored
http://www.informatik.uni-kiel.de/~kba/pax/
PAX is a tool that allows to verify parameterized networks of finite
state processes.
TReX
A Tool for Reachability Analysis of CompleX Systems
http://www.liafa.jussieu.fr/~sighirea/trex/
Université
Paris 7
Denis-Diderot
Laboratoire d'Informatique Algorithmique : Fondements et Applications
TReX is a tool for the analysis of systems having infinitely many configurations by using generic reachability semi-algorithms on symbolic representation of configurations. The kind of infinite systems which can be actually analyzed using TReX are extended automata with variables of heterogeneous types: clocks, counters, booleans, and enumerations. The variables may be assigned or compared with parameters, i.e., uninstantiated variables. The automata may communicate by unbounded lossy FIFO-channels and shared variables. For this kind of systems, TReX may either verify on-the-fly a safety property or generate the symbolic finite graph of the reachable configurations.
The current version of TReX is developed in C++ by Aurore Annichini
at VERIMAG and Mihaela Sighireanu at LIAFA.
TREAT: Timed REachability Analysis Tool
http://www.cis.upenn.edu/~lee/inhye/treat.html
GFA
Karel Culik
http://www.cs.sc.edu/~culik/
an applet that allows to draw a diagram of an automaton and immediately shows the images corresponding to each state (image compressing)
also GWFA
Generalized Weighted Finite Automata Based Image Compression,
TETRA
University of Montreal.
see ECVALIPTUS toolset
http://www-run.montefiore.ulg.ac.be/projects/EUCALYPTUS.html
Trace analysis: It is possible to verify whether a given trace (ecesution
sequence) can be obtained from a LOTOS description. This allows the validation
of test suites and their verdicts with respect to a LOTOS description
representing the system under test.
The generated or minimized LTS models can be displayed graphically
(i.e. in postscript) and edited. These BCG_Draw and BCG_Edit tools are
part of the CADP toolset developed in Verimag. Another tool, called VISCOPE
and developed at IRISA (Rennes), is also integrated and allows
3D visualization of graphs.
Java FSM editor of WELD web based electronic desigh
Berkeley
http://www-cad.eecs.berkeley.edu/Respep/Research/weld/index.html
CADP:Caesar/Aldebaran Development Package
inria (see inria site for other FM projects)
Conformance relation checking/minimisation v.r.t multiple relations.
FSM, CFSM, Lotos.
Model checking etc,
Unix/Windows
free for non commercial use
SMV .
Carnegie-Melon Univercity - School of Computer Science
http://www.cs.cmu.edu/~modelcheck
model checking
free for research
SyMP .
Carnegie-Melon Univercity - School of Computer Science
http://www.cs.cmu.edu/~modelcheck
is our new tool that combines model checking and theorem
proving in a single framework
Verus (real time)
Carnegie-Melon Univercity - School of Computer Science
http://www.cs.cmu.edu/~modelcheck/verus.html
Verus allows the formal specification and verification of real-time and other time critical systems. Free (for research)
Bounded Model Checker: BMC
Carnegie-Melon Univercity - School of Computer Science
http://www.cs.cmu.edu/~modelcheck/bmc.html
free for research
a ModelChecker for Stochastic Automata
David Akehurst, Howard Bowman, Jeremy Bryans, and John Derrick
Computing Laboratory, University of Kent, December 2000.
http://www.cs.ukc.ac.uk/pubs/2000/1187
(the manual)
COSPAN (COordinated SPecification ANalysis)
R. Kurshan and others, AT T Bell Laboratories
ftp://ftp.research.att.com/dist/COSPAN
Prototyping. CFSM (language containment) verification based on BDD
free for educational use. selection/resolution language.
DCVALID
A tool for model checking Duration Calculus Formulae
Paritosh Pandya
http://www.tcs.tifr.res.in/~pandya/dcvalid.html
Quantified Discrete-time Duration Calculus (QDDC). For every formula D, we
construct a finite state automaton A(D) precisely accepting the finite
state sequences satisfying D. The automaton can be used to find models
and counter models, or as a synchronous observer (or monitor) for model
checking.
EST - efficient symbolic tools
Robert Meolic
Tatjana Kapus
Ale¡ s ¡ Casar
Mirjam Sepesy Mau¡ cec
Zmago Brezo¡ cnik
University of Maribor
Faculty of Electrical Engineering and Computer Science
Smetanova 17, SI-2000 Maribor, Slovenia
http://www.el.feri.uni-mb.si/est
free (Gnu licence)
TVS
Delft University of Technology an
http://tvs.twi.tudelft.nl/toolset.html
model checking, simulation, and visualization of timed automata
FC2Tools
MEIJE – a joint researche grope of INRIA and Ecole des Mines/CMA (see also XEVE)
http://www-sop.inria.fr/meije/verification/index.html
The FC2Tools package, together with its graphical editor Autograph,
is a forerunner amongst softwares dealing with model-based, automatic verificationof
distributed communicating systems.
HyTech: The HYbrid TECHnology Tool
Thomas A. Henzinger
Electrical Engineering and Computer Sciences
University of California at Berkeley
http://www-cad.eecs.berkeley.edu/~tah/HyTech
Hybrid automata on fly model checker
Graphics from Uppal
VERSA: Verification Execution and Rewrite System for ACSR
Department of Computer and Information Science at the University of Pennsylvania
http://www.cis.upenn.edu/~lee/duncan/versa.html
To facilitate the use of the Algebra of Communicating Shared Resources
(ACSR) in the design and analysis of real-time systems we have developed
an
integrated set of tools called VERSA (Verification, Execution and Rewrite
System for ACSR). VERSA supports three types of analysis techniques:
1.Application of rewriting rules to ACSR specifications to deduce system
properties.
2.Construction of a state machine and automatic exploration and analysis
of the state space to verify safety properties and test equivalence of
3.Interactive execution of the process specification to explore specific
system behaviors and sample the execution traces of the system.
PROD 3.3.09
An Advanced Tool for Efficient Reachability Analysis
Kimmo Varpaaniemi, Keijo Heljanko and Johan Lilius
Helsinki University of Technology, Digital Systems Laboratory
http://www.tcs.hut.fi/prod/proddescription.html
T/Petri net reachablity analysis. Supports verification of CTL properties from the reachability graph, and on-the-fly verification of LTL-properties. Textual.
Free, registration is requied
also Emma (TNSDL) analysis
The PEP Tool (Programming Environment based on Petri Nets)
http://theoretica.informatik.uni-oldenburg.de/~pep/
simulation
SDL, CFSM -> petri nets
free for non commercial use
PEP2 will be open source soon
is a comprehensive set of modelling, compilation, simulation and verification
components, linked together within an Tcl/Tk-based graphical user interface.
PEP's modelling components facilitate the design of parallel systems
by parallel programs (B(PN)^2 and SDL), interacting
finite automata, process algebra, or high-level/low-level Petri nets.
PEP's compilers generate Petri nets from such models.
PEP's simulators allow automatic or user-driven simulation of high-level
/ low-level nets and may trigger simulation of the
corresponding programs and/or a 3D model.
PEP's verification component contains various Petri net indigenous
algorithms to check, e.g., reachability properties and
deadlock-freeness, as well as verification algorithms. We mention Esparza's
partial order based model checker, and
interfaces to
the INA package (offering structural analysis - invariants, etc. -
as well as stubborn set and symmetrically reduced
state space analysis),
the FC2Tools (offering verification based on networks of automata),
SMV (offering BDD based CTL model checking) and
SPIN (offering LTL model checking with optional partial order reductions).
The PEP tool can be considered as an open platform. Further algorithms
can be integrated in the user interface easily.
The COQ Proof Assistant
Inria
Caml
Java Pathfinder
NASA
Java model checker. SVC automatic theorem-prover is used for abstraction.
Available for beta testers and project collaborators.
The ToolBus Application Architecture
http://www.cwi.nl/projects/MetaEnv/toolbus/
The ToolBus is a software application architecture developed at the
University of Amsterdam and the CWI. The ToolBus utilizes a scripting language
based on process algebra to describe the communication between software
tools. A ToolBus script describes a number of processes that can communicate
with each other and with tools living outside the ToolBus. A language-dependent
adapter that translates between the internal ToolBus data format and the
data format used by the individual tools makes it possible to write every
tool in the language best suited for the task(s) it has to perform.
Statemate MAGNUM
I-Logic
http://www.sei.cmu.edu/domain-engineering/STATEMATE.html
Statecharts.
Windows, Solaris, HP/UX
Stateflow
Mathworks
http://www.mathworks.com/products
Statecharts visualization, animation, C code generation.
Stateflow is an interactive design tool for modeling and simulating complex event-driven systems. Tightly integrated with Simulink® and MATLAB®, Stateflow lets you design embedded systems that contain supervisory logic. A combination of graphical modelingand animated simulation brings system specification and design closer together.
Commercial, 30-day free trial. Price varies on the usage.
LIBERO
Imatix
http://www.imatix.com/html/libero/index.htm
a FSM CASE tool
commercial/GNU general public license (in the same time)
To do list
To find webpages :
AGL, AMORE, Automate, FADELA, FinITE, FireLite, INR, MONA, Turing's World, FANCY, and the Fire Engine.
model checkers
CWB [CPS93], MURPHI [DDHY92],
SPIN [Hol91], and VFSMvalid [FHS95]
Kronos , and UppAal , Winston, EMC, Auto
Disco, CMC, UPPAAL, Xeve(Inris)
Also to
check inria, verymag and other groups we know.
-------------------------------------------------------------------------
AUTOMATA TOOL LISTS
Tools from VERIMAG
http://www-verimag.imag.fr/tools.en.shtml
(content of the page:)
Synchronous Languages and Reactive systems
http://www.inria.fr/valorisation/logiciels
Numerous free (and free for non research use) tool including
This tutorial page should help you get started with the 3 different finite-state packages we have installed:
FSA Utilities
XFST: Xerox Finite-State Tool
FSM: AT&T finite-state library
Finite-state machine software, products, and projects
A FSM product list from Grail+ creators
http://www.csd.uwo.ca/research/grail/links.html
Verification tool list
(Indian Institute of Technology, Bombay)
http://www.cfdvs.iitb.ac.in/Docs/verification/tools/tool.html
Model checking links
http://www.abo.fi/~jolilius/mc/mclinks.html
provides links to the following
Academic Tools: HyTech, Kronos, MONA, Murphi, PEP, PROD, RAVEN, TREAT, TVS, SPIN, STEP, SMV, SMC, UPPAAL, Verus , Vis
Commercial Tools: CheckOff-M, FormalCheck, NP-Tools, PropertyProver,
Temporal-Rover.
FORMAL METHODs (VIRTUAL LIBRARY)
SDL Forum
A site devoted to SDL - Specification and Description Language standardized
as ITU (International Telecommunication Union) Recommendation Z.100. Language
is based on the CEFSM concept. Link to tool for SDL verification, testing,
etc are presented.
ABSTRACT STATE MACHINES
http://www.eecs.umich.edu/gasm
Tools for Abstract State Machines (former evolving algebra of Gurevich)
development, validation, visualization etc.
Selected Conferences:
Conference on Implementation and Application of Automata
(former WORKSHOP ON IMPLEMENTING AUTOMATA)
International Workshop on Graph Transformation and Visual Modeling Techniques and Workshop on Verification of Parameterized Systems
(Sattelites of ICALP International Colloquium on Automata, Languages and Programming)
Other FM, model-checking, Discrete Mathematics, and Theoretical CS conferences may be relevant