home *** CD-ROM | disk | FTP | other *** search
/ NetNews Usenet Archive 1993 #1 / NN_1993_1.iso / spool / comp / specific / 609 < prev    next >
Encoding:
Text File  |  1993-01-08  |  9.0 KB  |  218 lines
  1. Newsgroups: comp.specification
  2. Path: sparky!uunet!mcsun!sun4nl!utrcu1!infnews!infnews!lagemaat
  3. From: lagemaat@cs.utwente.nl (Jeroen van de Lagemaat)
  4. Subject: Re: Formal spec languages on top of C/C++ ?
  5. Message-ID: <1993Jan8.110527@cs.utwente.nl>
  6. Sender: usenet@cs.utwente.nl
  7. Nntp-Posting-Host: utis09
  8. Organization: University of Twente, Dept. of Computer Science
  9. References:  <1993Jan6.212736.1456@news.acns.nwu.edu>
  10. Date: Fri, 8 Jan 1993 10:05:27 GMT
  11. Lines: 205
  12.  
  13. In article <1993Jan6.212736.1456@news.acns.nwu.edu>, kanth@andersen.uucp (Kanth Miriyala) writes:
  14. |> 
  15. |> Are there any formal specification languages available on top
  16. |> of C/C++ environments? I am looking for formal spec languages
  17. |> that are automatically translated down to C or C++ (perhaps
  18. |> inefficiently or partially).
  19. |> 
  20. |> Please send me email. Thanks. 
  21. |> 
  22. |> -Kanth
  23. |> 
  24. |> kanth@andersen.com
  25.  
  26. I would like to inform you about available LOTOS tools.
  27.  
  28.  
  29.               Lotos Integrated Tool Environment
  30. 1. What lite is about
  31.  
  32. LITE is an integrated tool environment for LOTOS
  33. that aims to support:
  34.  
  35. --specification writing, reading, and maintenance
  36. --validation of requirements via simulation
  37. --verification of steps towards product realization
  38. --product derivation via compiling
  39. --support for testing (conformance, validation, ...)
  40.  
  41.  
  42.     |-------------------------------------------------------------|
  43.     |             edition: structure, graphical                   |
  44.     |                 source to source transformations            |
  45.     |-------------------------------------------------------------|
  46.     |  report generation:                  verification:          |
  47.     |      cross references               completion         |
  48.     |      gate sorts                   expansion          |
  49.     |      ADT sanity checks               basic LOTOS        |    
  50.     |                                                             |
  51.     |  simulation:                  compilation:            |
  52.     |      single step                       behaviour & data   |
  53.     |      predicate solver               rapid prototyping  |
  54.     |      objective driven               C, Ada, LWP        |
  55.     |-------------------------------------------------------------|
  56.     |             testing: behaviour and data                     |
  57.     |                 conformance and validation                  |
  58.     |-------------------------------------------------------------|
  59.  
  60. LITE: an open architecture for further extensions:
  61.  
  62. --LOTOS: ISO Language Of Temporal Ordering Specification.
  63. --CR: Common Representation.
  64.   It is both an external and internal representation,
  65.   and a set of tools to handle it.
  66.  
  67. LITE appears as open to further extensions,
  68. users may easily plug in their tools,
  69. and take benefit of each other's functionalities.
  70.  
  71. 2. Compiler Tools for LOTOS
  72.  
  73. Within the LOTOS Integrated Tool Environment (lite) the
  74. following tools for compilation are incorporated: TOPO and
  75. COLOS.
  76.  
  77. --TOPO provides automatic translation of behaviour and data part of a
  78.   LOTOS specification into code for an abstract machine,
  79.   so-called the lambda\beta machine. The lambda\beta machine code
  80.   is then translated into C.
  81.  
  82.   Annotations can be used to relate real events (i.e., interrupts,
  83.   signals, timer events, transmission and receptions of PDUs, etc.)
  84.   with abstract LOTOS events, to take into account efficient
  85.   implementations of LOTOS data types, to realize time delays
  86.   in event offerings, and to define default values in
  87.   ambiguous sum(choice)-expressions.
  88.  
  89. --COLOS is restricted to a subset of the behaviour part of a LOTOS
  90.   specification. The behaviour part is translated into an abstract machine,
  91.   so-called SAP ( system of automata and ports ). The SAP machine code
  92.   is then translated into C. LOTOS data types have to be defined and
  93.   implemented by hand using C.
  94.  
  95.   In addition, hand-coded implementations for the LOTOS data types
  96.   must be given by the implementor. COLOS facilitates the integration
  97.   of hand-coded data types by means of annotations (as in TOPO).
  98.  
  99.   The formal gates of the specification are used to relate the generated
  100.   implementation with its environment. This is also achieved by means of
  101.   annotations: formal gates are mapped on members of a predefined set of
  102.   environment ports. These environment ports are the only means in
  103.   which information can be read from and be passed to the
  104.   environment.
  105.  
  106. 3. Editing Tools for LOTOS
  107.  
  108. The LOTOS Integrated Tool Environment (lite) contains
  109. a graphical LOTOS editor, called GLOTOS, and a
  110. structure LOTOS editor, called CRIE.
  111. GLOTOS offers syntax driven graphical editing,
  112. CRIE offers textual and structural editing,
  113. including so-called correctness preserving transformations (CPTs),
  114. combined with interactive syntax and static semantics checking.
  115.  
  116. The editing in GLOTOS is menu driven; GLOTOS allows to transform a placeholder
  117. in its graphical or textual form. GLOTOS loads textual files or files in the
  118. editor's internal format.
  119.  
  120. CRIE offers structural editing as well as textual editing of any selected
  121. LOTOS expression.
  122. Editing applying CPTs is supported by the SPLITTING-tool and the RPPT-tool;
  123. the tools are available in CRIE when the selected LOTOS expression
  124. satisfies the applicability condition of the transformation.
  125.  
  126. CRIE automatically detects errors against static semantics,
  127. using incremental attribute recomputation,
  128. and flags them by LOTOS comments containing appropriate
  129. error messages at the location of the error.
  130.  
  131. CRIE automatically pretty prints the specification.
  132. CRIE can show the result sort of value expressions and the functionality
  133. of behaviour expression.
  134. It has additional browsers that show respectively the error messages,
  135. the headers of the process definitions or the headers of the data types
  136. of the specification.
  137. It is possible to do the static semantics checking on demand,
  138. allowing a user to postpone lengthy reevaluations.
  139. CRIE can compute the common representation of a specifcation.
  140.  
  141. 4. Report Generating Tools for LOTOS
  142.  
  143. Within the LOTOS Integrated Tool Environment (lite) the
  144. following tools for report generation and browsing are incorporated:
  145. LS1 and LS2, two phases of a syntax and semantic checker,
  146. a datatype analyzer, called REP-ADT, a gate-sortlist analyzer,
  147. called GSL, a
  148. cross reference generator, called REP-XREF, and a report browser,
  149. called LOBROW.
  150.  
  151. 5. Simulation Tools for LOTOS
  152.  
  153. Within the LOTOSPHERE Integrated Tool Environment (lite) a
  154. symbolic LOTOS simulation tool, called SMILE, has been
  155. incorporated. This tool offers functionalities for the analysis
  156. of the dynamic properties of both the process
  157. and the data type part of a specification.
  158.  
  159. SMILE can be used 
  160. (1) to gain more confidence in the dynamic behaviour of the 
  161.     system;
  162. (2) to test the abstract data type specification; 
  163. (3) to transform a specification into a finite state machine.
  164.     Such a finite state machine can then subsequently
  165.     be used as a starting point for an implementation;
  166. (4) to run test-sequences against a specification; or
  167. (5) to generate test-sequences from a specification.
  168.  
  169. SMILE is an interactive tool with an X11-based user interface.
  170. It has two different windows: one devoted to the analysis of
  171. the abstract data type part of the specification, and one
  172. for the behavioural part of the specification.
  173.  
  174. Any behaviour expression in the LOTOS specification can
  175. be analyzed either step by step (unfolding every state
  176. manually) or automatically (symbolic execution of the
  177. specification) up to a user-provided number of steps.
  178. SMILE offers a number of functions to control the
  179. actual behaviour of the simulation and for the interpretation
  180. of the results of the simulation.
  181.  
  182. 6. Test generation tool for Basic LOTOS
  183.  
  184. Within the LOTOSPHERE Integrated Tool Environment (lite) a
  185. test generation tool for Basic LOTOS has been incorporated.
  186. This tool computes a canonical tester from a Basic LOTOS specification.
  187.  
  188. 7. Verification Tools for LOTOS
  189.  
  190. The LOTOS Integrated Tool Environment (LITE) provides a number of
  191. verification tools and functions,
  192. including a completion tool COMPLOT,
  193. a tool for the construction and analysis of finite automata AUTO,
  194. a model checker for temporal logic CHECKER,
  195. and functions for building Basic Lotos approximations from Lotos
  196. specifications.
  197.  
  198. The behaviour verification functions can be used both as a debugging
  199. tool in the first steps of a specification development, and also later
  200. during refinement steps for proving that a refined specification is
  201. indeed a refinement of the previous version of the specification.
  202. The tools can be applied to an automaton encoding the complete
  203. extended finite state machine of the specification, when this is
  204. possible (e.g. through Smile or Lola), orelse to an automaton encoding a
  205. Basic Lotos finite approximation of the specification.
  206. -- 
  207.     ___
  208.  __/   \__________  Jeroen van de Lagemaat    <lagemaat@cs.utwente.nl>
  209. |  \___/          |         
  210. |___     __   ___ | University of Twente     
  211. | |  |  /  \ (__  | Tele-Informatics & Open Systems
  212. | |__|__\__/____) | P.O. Box 217  NL-7500 AE Enschede  The Netherlands
  213. |_________________| tel. +31 53 893684              tfx. +31 53 333815
  214.  
  215.                     Humour, you're making me laugh.
  216.                                     - Herman Finkers, Dutch comedian -
  217.  
  218.