🚀 go-pugleaf

In article <1993Jan6.212736.1456@news.acns.nwu.edu>, kanth@andersen.uucp (Kanth Miriyala) writes:
|> 
|> Are there any formal specification languages available on top
|> of C/C++ environments? I am looking for formal spec languages
|> that are automatically translated down to C or C++ (perhaps
|> inefficiently or partially).
|> 
|> Please send me email. Thanks. 
|> 
|> -Kanth
|> 
|> kanth@andersen.com

I would like to inform you about available LOTOS tools.


              Lotos Integrated Tool Environment
1. What lite is about

LITE is an integrated tool environment for LOTOS
that aims to support:

--specification writing, reading, and maintenance
--validation of requirements via simulation
--verification of steps towards product realization
--product derivation via compiling
--support for testing (conformance, validation, ...)


    |-------------------------------------------------------------|
    |             edition: structure, graphical                   |
    |                 source to source transformations            |
    |-------------------------------------------------------------|
    |  report generation:                  verification:          |
    |      cross references		       completion         |
    |      gate sorts			       expansion          |
    |      ADT sanity checks		       basic LOTOS        |	
    |                                                             |
    |  simulation:		          compilation:            |
    |      single step		               behaviour & data   |
    |      predicate solver		       rapid prototyping  |
    |      objective driven		       C, Ada, LWP        |
    |-------------------------------------------------------------|
    |             testing: behaviour and data                     |
    |                 conformance and validation                  |
    |-------------------------------------------------------------|

LITE: an open architecture for further extensions:

--LOTOS: ISO Language Of Temporal Ordering Specification.
--CR: Common Representation.
  It is both an external and internal representation,
  and a set of tools to handle it.

LITE appears as open to further extensions,
users may easily plug in their tools,
and take benefit of each other's functionalities.

2. Compiler Tools for LOTOS

Within the LOTOS Integrated Tool Environment (lite) the
following tools for compilation are incorporated: TOPO and
COLOS.

--TOPO provides automatic translation of behaviour and data part of a
  LOTOS specification into code for an abstract machine,
  so-called the lambda\beta machine. The lambda\beta machine code
  is then translated into C.

  Annotations can be used to relate real events (i.e., interrupts,
  signals, timer events, transmission and receptions of PDUs, etc.)
  with abstract LOTOS events, to take into account efficient
  implementations of LOTOS data types, to realize time delays
  in event offerings, and to define default values in
  ambiguous sum(choice)-expressions.

--COLOS is restricted to a subset of the behaviour part of a LOTOS
  specification. The behaviour part is translated into an abstract machine,
  so-called SAP ( system of automata and ports ). The SAP machine code
  is then translated into C. LOTOS data types have to be defined and
  implemented by hand using C.

  In addition, hand-coded implementations for the LOTOS data types
  must be given by the implementor. COLOS facilitates the integration
  of hand-coded data types by means of annotations (as in TOPO).

  The formal gates of the specification are used to relate the generated
  implementation with its environment. This is also achieved by means of
  annotations: formal gates are mapped on members of a predefined set of
  environment ports. These environment ports are the only means in
  which information can be read from and be passed to the
  environment.

3. Editing Tools for LOTOS

The LOTOS Integrated Tool Environment (lite) contains
a graphical LOTOS editor, called GLOTOS, and a
structure LOTOS editor, called CRIE.
GLOTOS offers syntax driven graphical editing,
CRIE offers textual and structural editing,
including so-called correctness preserving transformations (CPTs),
combined with interactive syntax and static semantics checking.

The editing in GLOTOS is menu driven; GLOTOS allows to transform a placeholder
in its graphical or textual form. GLOTOS loads textual files or files in the
editor's internal format.

CRIE offers structural editing as well as textual editing of any selected
LOTOS expression.
Editing applying CPTs is supported by the SPLITTING-tool and the RPPT-tool;
the tools are available in CRIE when the selected LOTOS expression
satisfies the applicability condition of the transformation.

CRIE automatically detects errors against static semantics,
using incremental attribute recomputation,
and flags them by LOTOS comments containing appropriate
error messages at the location of the error.

CRIE automatically pretty prints the specification.
CRIE can show the result sort of value expressions and the functionality
of behaviour expression.
It has additional browsers that show respectively the error messages,
the headers of the process definitions or the headers of the data types
of the specification.
It is possible to do the static semantics checking on demand,
allowing a user to postpone lengthy reevaluations.
CRIE can compute the common representation of a specifcation.

4. Report Generating Tools for LOTOS

Within the LOTOS Integrated Tool Environment (lite) the
following tools for report generation and browsing are incorporated:
LS1 and LS2, two phases of a syntax and semantic checker,
a datatype analyzer, called REP-ADT, a gate-sortlist analyzer,
called GSL, a
cross reference generator, called REP-XREF, and a report browser,
called LOBROW.

5. Simulation Tools for LOTOS

Within the LOTOSPHERE Integrated Tool Environment (lite) a
symbolic LOTOS simulation tool, called SMILE, has been
incorporated. This tool offers functionalities for the analysis
of the dynamic properties of both the process
and the data type part of a specification.

SMILE can be used 
(1) to gain more confidence in the dynamic behaviour of the 
    system;
(2) to test the abstract data type specification; 
(3) to transform a specification into a finite state machine.
    Such a finite state machine can then subsequently
    be used as a starting point for an implementation;
(4) to run test-sequences against a specification; or
(5) to generate test-sequences from a specification.

SMILE is an interactive tool with an X11-based user interface.
It has two different windows: one devoted to the analysis of
the abstract data type part of the specification, and one
for the behavioural part of the specification.

Any behaviour expression in the LOTOS specification can
be analyzed either step by step (unfolding every state
manually) or automatically (symbolic execution of the
specification) up to a user-provided number of steps.
SMILE offers a number of functions to control the
actual behaviour of the simulation and for the interpretation
of the results of the simulation.

6. Test generation tool for Basic LOTOS

Within the LOTOSPHERE Integrated Tool Environment (lite) a
test generation tool for Basic LOTOS has been incorporated.
This tool computes a canonical tester from a Basic LOTOS specification.

7. Verification Tools for LOTOS

The LOTOS Integrated Tool Environment (LITE) provides a number of
verification tools and functions,
including a completion tool COMPLOT,
a tool for the construction and analysis of finite automata AUTO,
a model checker for temporal logic CHECKER,
and functions for building Basic Lotos approximations from Lotos
specifications.

The behaviour verification functions can be used both as a debugging
tool in the first steps of a specification development, and also later
during refinement steps for proving that a refined specification is
indeed a refinement of the previous version of the specification.
The tools can be applied to an automaton encoding the complete
extended finite state machine of the specification, when this is
possible (e.g. through Smile or Lola), orelse to an automaton encoding a
Basic Lotos finite approximation of the specification.
-- 
    ___
 __/   \__________  Jeroen van de Lagemaat    <lagemaat@cs.utwente.nl>
|  \___/          |         
|___     __   ___ | University of Twente     
| |  |  /  \ (__  | Tele-Informatics & Open Systems
| |__|__\__/____) | P.O. Box 217  NL-7500 AE Enschede  The Netherlands
|_________________| tel. +31 53 893684              tfx. +31 53 333815

                    Humour, you're making me laugh.
                                    - Herman Finkers, Dutch comedian -