Sage (Service Attribute Generator)

Lotos Logo

See the download page to obtain this program

Description

These files generate OSI (Open Systems Interconnection) service specifications in LOTOS. Services are described using the Sage language that builds services from their constituent facilities. See An engineering approach to formal methods and Exploiting the m4 macro language for more details. Be warned that macros in this package are very intricate!

Note the following relative to the PSTV paper cited above:

Usage

As an example, consider a connection-oriented service with the following characteristics:

The Sage description required to define this service is as follows:

  include(sage.m4)

  divert

  define(Conn12,
    facility(12,user_confirmed,reliable,Conn(Addr1,Addr2),Conn()))
  define(Data12,
    facility(12,provider_confirmed,unreliable,Data(Data),Ack()))
  define(Data21,
    facility(21,provider_confirmed,unreliable,Data(Data),Ack()))
  define(Exp21,
    facility(21,unconfirmed,reliable,Exp(Data)))
  define(Reset12,
    facility(12,unconfirmed,reliable,Reset(Reas)))
  define(Disc21,
    facility(21,unconfirmed,consecutive,Disc()))

  global(cs,
    withheld(Conn,
      forall_ids(
	disables(Disc21,
	  enables(Conn12,
	    interrupts(
	      colliding(Reset12),
		interleaves(Data12,
		  overtakes(Exp21,Data21))))))))
  

Licence

This program is free software. You can redistribute it and/or modify it under the terms of the GNU General Public License as published by the Free Software Foundation - either version 2 of the License, or (at your option) any later version.

This program is distributed in the hope that it will be useful but without any warranty, without even the implied warranty of merchantability or fitness for a particular purpose. See the GNU General Public License for more details.

History

First public version Ken Turner, 04/06/96


Up Arrow Up one level to LOTOS Utilities

Web Ken Turner Home   Email    Search Search Web Pages

Last Update: 18th October 2007
URL: http://www.cs.stir.ac.uk/~kjt/software/lotos/sage.html