LOTOS, the Language Of Temporal Ordering Specifications, is a specification language for distributed systems which has been developed within the International Organization for Standardization (ISO) as International Standard 8807.
Initially, the prime purpose of LOTOS was to specify Open Systems Interconnection (OSI) protocols and services. However, the language has proven useful for specifying other distributed systems. Among possible users are designers and developers of, and researchers on distributed systems, especially protocols and telephone systems.
ELUDO stands for Environnement LOTOS de l'Université d'Ottawa (University of Ottawa LOTOS Environment). Developed at the University of Ottawa, ELUDO takes a LOTOS specification as input, checks its static semantics, and executes the specification to produce the next possible actions as output. Full standard LOTOS is supported (the only exception being simultaneous actualization and renaming of formal types), and specifications of thousands of lines have been executed.
The purpose of the tool is thus to provide an integrated environment to the LOTOS specifier, with the tools necessary to verify LOTOS specifications. It can be used in different modes:
the user is prompted, at each step, with the next possible actions. The user chooses the next action to be executed and, if the action involves a choice of data, the user is required to provide it. Used in this way, the specification may be considered as a running prototype of the entity specified.
the user may generate a tree of all possible actions from any point. However, values are represented by a combinaison of value expressions and symbolic identifiers that may involve nested references to other values.
the user asks the tool to find an execution path based on the user specified (partial) trace.
The X in XEludo indicates that the interface of the tool is an X window system based application. Most tools of XEludo are operated entirely from menus and buttons. The kernel of the tool is Prolog based, the choice of Prolog as the programming language coming from its high level of compatibility with the dynamic sematics of the LOTOS language.
ELUDO contains other sub-tools, such as a LOTOS Model Checker (LMC) and a canonical test generator (LOTEST).
ISLA stands for Interactive System for LOTOS Applications. It also used to be the name of the toolkit, at that time when ISLA itself consisted of most of ELUDO functionnality. ISLA is the Step-by-Step mode of execution of a specification.
The step-by-step execution of a LOTOS specification performed by ISLA can be represented as a tree, where the root of the tree is the initial behavior, the intermediate nodes are derived behavior expressions, and the branches of the tree represent the LOTOS actions used to derive successive behaviors. Once a LOTOS specification is written, the user can invoke ISLA to simulate the sequence of possible actions that are permitted by the specification. The user may choose to simulate the whole specification at once (the main behavior), or only parts of it (specific processes).
At each step during simulation, the user is prompted with a list of actions that might be used to derive the current behavior. The user chooses the next action to be executed and, if the selected action requires data to be supplied by the environment (the user plays the role of the environment), then data must be entered for the simulation to continue. A menu-driven facility (value expression editor) prompts the user with appropriate choices for data.
Also, at any point during simulation, the user may ask to see the current behavior of the system or the behavior that will result by executing one of the possible next actions; or have the current behaviour displayed and updated as actions are being executed.
Furthermore, ISLA displays the complete set of execution paths that have been exercised by the user during the current simulation session, in the form of a tree. This permits to check, for example, where, in the execution tree, certain value identifiers were instantiated. So, if certain chosen values did not lead to the desired sequence (e.g. rendered the evaluation of a guard or predicate to be false, or prevented experiments value matching), the user can back up to a point where a different value can be entered. Therefore, the user may return to a previous execution point, and redo execution from that point with different choices.
Moreover, ISLA may be asked to automatically replay a sequence of actions in the current path, starting at a node involving data acquisition by the user, located above the current one up to the root. Such a sequence is replayed entirely, or to the extent where some previously executed action can no more be executed due to experiments matching, guards or predicates.
The state of an ISLA simulation session (specification, initial behavior and all executed events) maybe be saved to file. This information may then be used to resume the state of simulation, thereby gaining the possibility of continuing the simulation, at a later time, from where it was left off.
SELA stands for Symbolic Expander of LOTOS Applications.
The Symbolic Expander generates a tree made of all possible traces of execution. The specific qualitative symbolic relates the fact that each time a derivation would ordinarily require a value from the environment, a symbolic value is substituted in its place. This allows to user to keep track of value definitions and uses. It also implies the generation of many execution branches that might have been pruned given a bad value had been provided by the environment, or in cases like impossible conditions imposed by the specifier (e.g. [(X > 5) AND (X < 4)]).
The step-by-step execution mode is very useful but it is also time consuming. SELA allows one to compute the tree of all possible next actions from the current behavior of ISLA , or any given process in the specification. This is known as the symbolic execution tree because expressions are computed in terms of (not necessarily) bounded value identifiers.
In terms of LOTOS theory, the calculation of this tree is called expansion. When generating a symbolic tree, guards and predicates, whose values depend on interactions with the environment, are assumed to be true. In addition, the user is required to set limits on the depths and widths of the symbolic tree to be generated.
Optional detection of recursion provides a means of reducing the generated tree, by having branches of the symbolic tree pruned whenever it is recognized that a state previously encountered is reached for a second time and a loop is generated in the tree.
Sometimes, recursion depends on the identification of certain parameters; the interpreter is able of identifying these and generate smaller symbolic trees.
Although calculation of the symbolic tree may not terminate, it can yield finite initial subtrees of an infinite monolithic specification equivalent to the original one.
The expanded tree of a specification is also intended to be used by other tools, such as a logical model checker (LMC) and canonical test generator (LOTEST).
GOE stands for Goal-Oriented Execution.
In a nutshell, GOE is a tool that assists the user in finding future events in the behaviour without going through the lengthy operation of derivation.The dynamic semantics of LOTOS are defined in terms of axioms and inference rules which generate, from a given behaviour expression, the next possible actions and their resulting behaviour expressions. GOE introduces a new type of inference rules, which are capable of generating traces of actions leading to a pre-selected action in the specification. These inference rules are guided by the static derivation path of the pre-selected action, which locates the action in the abstract syntactic tree of the current behaviour statically. This allows a considerable reduction of the search space. Such a technique often permits the analysis of divergent specifications that are generally beyond the capabilities of verification tools based on traces.
Both ISLA and SELA suffer the well-known problem of state explosion: for most practical specifications, execution trees grow very quickly. Goal-oriented execution attempts to relieve this problem.Check out The GOE Tool page for further details.
LMC stands for LOTOS Model Checker. LMC executes CTL model-checking on the tree produced by SELA, using the well-known algorithms of Clarke, Emerson and Sistla.
Check out The LMC Tool page for further details.
LOTEST is a LOTOS Canonical Test Generator. LOTEST performs test case generation for LOTOS specifications, according to the standard CO-OP method.
The LOTOS to Prolog Translator is a sub-tool of XEludo that pre-processes the LOTOS specification. It verifies that the syntactical and static semantical rules of the language are respected. Once the LOTOS specification is error-free, it is translated into a Prolog form suitable for simulation by the other tools of XEludo.
The functions of the translator are applied in sequence, each step requiring that the previous one succeeds in order to be executed. E.g. the static semantics rules are not verified until the syntactil rules are error-free.Additional information may optionally be extracted from the specification. The main steps and options supported by the translator are the following: