🚀 go-pugleaf

Kanth Miriyala (kanth@andersen.uucp) wrote:
: 
: 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

The NIST Estelle tools, Portable Estelle Translator (pet) and Distributed
Implementation Generator (dingo), can generate C and C++ from formal
specs.  Estelle is the extended state transition language developed in ISO
for OSI protocol specifications.  It's useful for distributed system specs
as well.  See the anonymous ftp directory pub/petdingo on osi.ncsl.nist.gov.

--

Rick Kuhn                                   Telephone: +1 301 975 3337       
Natl Institute of Standards & Technology    Fax:       +1 301 590 0932      
Technology Bldg. B266                       Internet: kuhn@swe.ncsl.nist.gov
Gaithersburg, Md.  20899  USA                       DRKuhn@dockmaster.ncsc.mil

In <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).

We are working on a formal specification language for C++, Larch/C++.
However it we have no plans for automatically generating executable code.
(On the other hand, we will automatically extract header files from the
specifications.)  If you are interested, send the message,
	send TR TR92-16a
to almanac@cs.iastate.edu to get a report describing the design.
We have a parser for the language, and are working on a reference manual
and documentation.  Watch for an announcement of availability...

However, I think what you want may be the RAISE tools.  You can get them from
CRI in Denmark (for real money).  This is a finely engineered and realistic
specification environment, which can generate (inefficient) C++ code from
certain specifications.  Contact jsp@csd.cri.dk (Jan Storbank-Pedersen)
or look up the following for more information.

@InCollection{Chalmers-etal91,
  Key = 	"D. L. Chalmers, {\em et al}",
  Author = 	"D. L. Chalmers and B. Dandanell and J. Gortz and J.
		 S. Pedersen and E. Zierau",
  Title = 	"Using RAISE --- First Impressions from the LaCoS Applications",
  BookTitle = 	"VDM '91 Formal Software Development Methods 4th
		 International Symposium of VDM Europe
		 Noordwijkerhout, The Netherlands, Volume 1:
		 Conference Contributions",
  Publisher = 	Springer-Verlag,
  Year = 	1991,
  Editor = 	"S. Prehn and W. J. Toetenel",
  Series = 	LNCS,
  Volume = 	551,
  Pages = 	"645-657",
  Address = 	NY,
  Month = 	Oct,
  Annote = 	"12 references."
}


@Article{Dandanell91,
  Key = 	"Dandanell",
  Author = 	"Bent Dandanell",
  Title = 	"Rigorous Development Using {RAISE}",
  Journal =	"Software Engineering Notes",
  Year = 	1991,
  Volume = 	16,
  Number = 	5,
  Month = 	Dec,
  Pages = 	"29-43",
  Note = 	"ACM SIGSOFT '91 Conference on Software for Critical Systems, New Orleans Louisiana, Dec. 4-6",
  Annote = 	"11 references."
}


@TechReport{Eriksen-Prehn91,
  Key = 	"Eriksen \& Prehn",
  Author = 	"Kirsten Eriksen and Soren Prehn",
  Title = 	"{RAISE} Overview",
  Institution = 	"Computer Resources International A/S",
  Year = 	1991,
  Number = 	"RAISE/CRI/DOC/9/V5",
  Address = 	"Denmark",
  Month = 	Oct,
  Annote = 	"17 references."
}

There is reportedly a book or two (to be) published by Prentice Hall about
RAISE.

	Gary Leavens

--
	229 Atanasoff Hall, Department of Computer Science
	Iowa State University, Ames, Iowa 50011-1040, USA
	phone: (515) 294-1580  fax: (515) 294-0258

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 -