Participating 
     Organizations 
  Research   
     Topics 
  People 
   

formalWARE 
    results 
 
  Overview 
  Publications 
  Presentation 
  Tools   
  Methods 
  Examples   
  Training 

formalWARE  
  information  

  Events 
  Index  
  Links   
  Contacts

A notation called "S" is used for several aspects of the formalWARE project. This notation, developed by Dr. Jeff Joyce (RSC), Nancy Day (UBC Computer Science) and Michael Donat (UBC Computer Science), is based on typed, predicate logic. An extensible parser called "Fuss" has been developed within formalWARE for the S notation. A form of automated validation called "typechecking" is built into Fuss. The use of Fuss to validate a formal specification written in S notation is analogous to the use of tools such as "Fuzz" to validate a formal specification written in Z notation. Fuss may be extended by users to incorporate user-defined analysis functions. A public domain release of Fuss and supporting documentation is anticipated to appear in April 1998.  

The formalWARE project maintains a partnership with an independent research effort at UBC (funded separately by NSERC) focused on the development of tool support for a system of mathematical reasoning called NadSyL, developed by Dr. Paul Gilmore. NaDSyL provides a foundation for logic and programming languages which acts as a less complex and constrained alternative to the conventional one (typed higher order logic). This formalism supports a more simple and direct semantic embedding of other formal notations such as Statecharts. It may also allow easier proofs of properties of systems described in terms of such formal notations. We anticipate that NaDSyL, with supporting software tools, will be particularly useful as a means of validating (as a task within the scope of formalWARE) the semantic definitions of specialized notations used in formalWARE.  

Several other notations and mathematical formalisms are used within formalWARE. This includes the use of value-passing CCS by Dilian Gurov (UVic Computer Science), Georgi Kostadinov (UVic Computer Science) and Jamie Andrews (UBC Computer Science) as well as the use of Statecharts by Nancy Day (UBC Computer Science).