Participating 
     Organizations 
  Research   
     Topics 
  People 
   

formalWARE 
    results 
 
  Overview 
  Publications 
  Presentation 
  Tools   
  Methods 
  Examples   
  Training 

formalWARE  
  information  

  Events 
  Index  
  Links   
  Contacts

DISCLAIMER: These tools are research prototypes. The purpose of these tools is to demonstrate research findings. The tools are provided as is and are not maintained. The University of British Columbia and the author of the tool disclaim all warranties with regard to this software, including all implied warranties of merchantability and fitness. In no event shall the University of British Columbia nor the author of the tool be liable for any special, indirect or consequential damages or any damages whatsoever resulting from loss of use, data or profits, whether in an action of contract, negligence or other tortious action, arising out of or in connection with the use or performance of this software.

Overview

formalWARE researchers are developing software tools as part of their project related research.

Contents of this section include:

• FUSS
• FUSION
• TCG
• APE
• s2lp
• SL

FUSS  

Fuss is a typechecker for a specification notation called "S" based on typed, predicate logic; the use of this tool to typecheck formal specifications written in "S" is analogous to the use of typecheckers for "Z" (e.g., Fuzz); in addition to typechecking, Fuss includes a software interface which allows users to use Fuss as a parser for analysis tools based on "S". 

For more information on S and Fuss, please see the following titles on the "publications" page of the formalWARE project: 
  

S - A General-Purpose Specification Notation (Technical Teport) 
  
Practical Experience Applying Formal Methods to Air Traffic Management Software (Conference Paper) 
  
S: A Machine Readable Specification Notation based on Higher Order Logic (Conference Paper) 
 

FUSION  

Fusion is a tool developed by Nancy Day which provides support for various kinds of analysis of "S" based specifications; analysis functions provided by Fusion include completeness and consistency checking as well as symbolic function evaluation, symbolic simulation and model checking. 

For more information on Fusion, please see the following titles on the "Publications" and "Presentations" pages of the formalWARE project: 

A Framework for Multi-Notation, Model-Oriented Requirements Analysis (Ph.D. Dissertation) 

Specification and Tool-based Analysis of an Aircraft Separation Minima (Presentation)

Formal Validation of System Specifications (Presentation) 

Formalization and Analysis of the Separation Minima for Aircraft in the North Atlantic Region: Complete Specifications and Analysis Results (Technical Report)  

Formalization and Analysis of the Separation Minima for Aircraft in the North Atlantic Region (Conference Paper) 

Formal Analysis of System Specifications (Presentation) 

TCG  

TCG is a tool developed by Michael Donat for generating test cases from formal specifications written in S notation; a variant of this tool, called "QTCG", generated test cases from formal specifications written in an experimental notation called "Q" which supports an "English-like" style of formal specification. 

Several unix versions of the TCG and QTCG tools are available. The links in the table below point to uncompressed binaries. The startup.s and startup.q files are useful.

Sun4 Solaris (sun4sol)	TCG QTCG
Sun4 (sun4)	TCG QTCG
Digital's Alpha (dec3000)	TCG QTCG
HP 700 (hp700)	TCG QTCG

For more information on TCG, please see the following titles on the "Publications" and "Presentations" pages of the formalWARE project: 
  

A Discipline of Specification-Based Test Derivation (Ph.D. Dissertation) 

Applying an Automated Test Description Tool to Testing Based on System Level Requirements (Conference Paper) 

Automatically Generated Test Frames from an S Specification of Separation Minima for the North Atlantic Region (Technical Report) 

Automatically Generated Test Frames from a Q Specification of ICAO Flight Plan Form Instructions (Technical Report) 

Test Generation from System-level Requirements Specification (Presentation) 

Automating formal specification-based testing (Conference Paper) 

APE  

APE is a tool developed by Dan Hoffman and others for generating Ada test drivers from test scripts; this is an Ada adaptation of the PGMGEN tool described in a textbook co-authored by Dan. 

For more information on APE, please see the following titles on the "publications" and "Presentations" pages of the formalWARE project: 
 

Testing Generic Ada Packages with APE (conference submission) 

Automated Package Testing (Presentation) 

 

s2lp  

s2lp is a tool developed by Jamie Andrews which translates an S specification into the higher order logic programming language Lambda Prolog; the translated specification can be executed like a logic program; this allows users to validate the original specification to make sure it is specifying something sensible; the program is an adaptation of the Fuss typechecker. 

For more information on S2lp, please see the following titles on the "publications" and "Presentations" pages of the formalWARE project: 
 

Executing Formal Specifications by Translation to Higher Order Logic Programming (Conference Paper) 

Executing Formal Specifications by Translation to Higher Order Logic Programming (Presentation) 

 

SL  

SL is an interpreter-like tool for the S specification notation developed by Michael Donat; it uses repeated rewriting as a means of evaluating an S expression. This allows (slow) logic programs to be written in S. 

Several unix versions of the SL tool are available. The links in the table below point to uncompressed binaries. The startup.s file is useful.

Sun4 Solaris (sun4sol)	SL
Sun4 (sun4)	SL
Digital's Alpha (dec3000)	SL
HP 700 (hp700)	SL

For more information on SL, please see the following titles on the "publications" and "Presentations" pages of the formalWARE project: 

A Discipline of Specification-Based Test Derivation (Ph.D. Dissertation)