LOTOS Utilities
AD/IT (Abstract Decision/Interactive Trees)
The list that follows gives a few Lotos utilities I wrote for my own purposes. They are available in source form.
Summary:These files are used to define, translate and formally analyse decision trees. See the AD/IT web page for more details.
Needs: GNU M4, Perl, Lola/Topo
Usage: See README file
Source: Obtain adit-1.2.zip by http
Summary:These files generate and analyse IN (Intelligent Network) service specifications using Lotos as the underlying language. The Plain Old Telephone Service and a variety of IN-like features are supported. See the Anise web page for more details.
Needs: GNU M4, Perl, Lola/Topo
Usage: See README file
Source: Obtain anise-1.0.zip by http
Summary:These files generate OSI (Open Systems Interconnection) service specifications in Lotos. Both connection-less and connection-oriented services are handled. See Template-based specification in Lotos and Relating Architecture and Specification for more details.
Needs: M4, Lotos tools
Usage: See README file
Source: Obtain basil.zip by http
Summary:Clove (Cress Langage-Oriented Verification Environment) is a notation and a tool for specifying and verifying specification properties. The principal designer was Larry Tan (University of Stirling). Clove has been used for DS (Device Services), GS (Grid Services), IN (Intelligent Network), IVR (Interactive Voice Response), SIP (Session Initiation Protocol) and WS (Web Services). See the Clove web page for an overview of Clove.
Needs:
- M4, Perl and REGLDG (Regular Expression Grammar Language Dictionary Generator)
- CADP for use with Lotos
Usage: See README file (on SourceForge)
Source: Obtain cresstools-1.0.zip (from SourceForge)
Summary:Dill (Digital Logic in Lotos) is an approach for specifying digital logic circuits and translating them to Lotos. Circuits are described using the Dill language that builds designs from their constituent components. See the Dill web page for more details.
Needs: M4, Lotos tools
Usage: See README file
Source: Obtain dill-2.4.zip by http
Summary:These tools support the analysis, testing and translation of Lotos specifications. The software belongs to the Polytechnic University of Madrid, and is distributed here only because of its port by the author to CygWin/Microsoft Windows and Debian Linux.
Needs: CygWin and Microsoft Windows, or Debian Linux
Usage: See README file
Source: Obtain topo-3.7.5.zip by http
Summary:Mint (Mustard Interpreter) is a language and a tool for defining and validating grid or web service test scenarios. It has been used for GS (Grid Services) and WS (Web Services). See the Mustard web page for Mustard as the context of Mint.
Needs:
- Sun JDK (e.g. version 1.6) and Perl (e.g. version 5.X)
- ActiveBPEL (e.g. version 5.0.2) for use with grid or web services
- Globus WS Core (e.g. version 4.2) for use with web services
Usage: See README file (on SourceForge)
Source: Obtain cresstools-1.0.zip (from SourceForge)
Summary:Mustard (Multiple-Use Scenario Test And Refusal Description) is a notation and a tool for specifying and validating test scenarios. It has been used for DS (Device Services), GS (Grid Services), IN (Intelligent Network), IVR (Interactive Voice Response), SIP (Session Initiation Protocol) and WS (Web Services). See the Mustard web page for an overview of Mustard.
Needs:
- M4 and Perl
- Lola/Topo for use with Lotos
- Telelogic Tau SDL Suite for use with SDL/MSC
Usage: See README file (on SourceForge)
Source: Obtain cresstools-1.0.zip (from SourceForge)
Summary:These files generate OSI (Open Systems Interconnection) service specifications in Lotos. Services are described using the Sage language that builds services from their constituent facilities. See An engineering approach to formal methods and Exploiting the m4 macro language for more details.
Needs: M4, Lotos tools
Usage: See README file
Source: Obtain sage.zip by http
Several Lotos sites offer information and tools for specification checking, simulation, compilation and analysis.
Up one level to Ken Turner - Software