Specification languages and tools
Process algebra
We think process algebra is suitable for describing various aspects of VEs:
modalities, GUI components, and possibly task and dialogue models. In terms of
computer-aided tools, process algebra has two possibilities: automatic model
checking and execution.
Model checkers/process algebra compilers
- SPIN - A powerful model checking tool. Models are
specified in Promela. Quick example: towers of Hanoi
problem. The problem can be solved by verifying the property that the
discs can never be at peg 2 at the same time. The counterexample found is a
solution to the problem. A `shortest trace' (optimal solution) can also be
generated.
- SMV
- LOTOS
- Occam
- FSP - Looks
much like CSP, but with some useful shorthands. There is an LTS analyser for
FSP that is able to do model checking and simulation.
- VHDL - A language for modelling hardware. The standard VHDL toolkit
does not contain a model checker, only a simulator with visualisation of
signals as waveforms.
Process algebra in programming languages
We are interested in execution of process algebraic descriptions or automatic
code generation. In our case, we wish to develop a VE system that is
web-based, which probably implies Java.
- CTJ - CTJ
is a realtime multithreading extension to Java, which is based on Occam
language constructs.
- JCSP - JCSP similar to CTJ. It is not real-time but the
extensions include process algebra versions of GUI objects as well.
- FSP/Java - The FSP tutorial also includes some examples, and
some extensions for writing CSP-based Java programs more easily.
- synchjava
Merging CSP with OO
- Erlang - Functional and
parallel programming language.
Architectural description languages
The basic idea of architectural description languages (ADL) is to enable the
structuring of a software system into modules with explicit interfaces.
Plan-based executable languages
AI and `agent' applications often use plan-based engines. Such engines are
also used for simulation of human cognition.
- ETAG (Geert de Haan's
publications on ETAG) - ETAG is used for specifying and
sometimes simulating user tasks.
-
DESIRE - Language + toolkit for modelling multi-agent systems
- SOAR - A well-known AI programming language, also supporting multiple
agents. Quick example (taken from the standard SOAR examples): towers of Hanoi. Though it will be much faster
than the model checking version above, it is also more verbose, and a solving
strategy (basically, just the standard Hanoi solution algorithm) must be given
explicitly.
- Act-R A
`cognitive simulator'.
Agent platforms
Agent platforms typically implement a protocol through which (mobile,
Web-based) agents may communicate. Sometimes, though usually not, a plan
specification language with reasoning engine is also supplied. Since these
platforms are generally internet-based, they are typically written in Java.