Sage (Service Attribute Generator)

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:

• It is required that the group name of a facility not be part of another (e.g. Data and ExpData are not allowed together).
• If a facility has several parameters of the same sort, these must be numbered to distinguish them, e.g. Datagram(Addr1,Addr2,Data).
• If a facility has no parameters they must be given as empty, e.g. Ack().
• The Opt predefined type is not available.
• Depending on the particular combinators, it may be necessary to change specification or process functionality from noexit to exit or vice versa.
• Some simulators may require the output from Sage to be fixed up by insertion of i; before recursive calls to prevent a "state not guardedly well-defined" error. This is typically required in processes such as:

        process P ...
  	PAux
        |||
  	i; P
        endproc
        

Usage

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

• There is just a pair of users, 1 and 2.
• User 1 may initiate a connection. This is user-confirmed, reliable and has primitives:

        ConnReq (Addr1, Addr2)
        ConnInd (Addr1, Addr2)
        ConnRes ()
        ConnCon ()
        

  A connection initiation attempt may be withheld (e.g. due to lack of resources). Completion of connection enables data transfer: normal data, expedited data, reset. Connections may be established for any pair of interaction group identifiers.

• Either user may initiate normal data transfer. This is provider-confirmed, unreliable and has primitives:

        DataReq (Data)
        DataInd (Data)
        AckInd ()
        

• User 2 may initiate expedited data transfer. This is unconfirmed, reliable and has primitives:

        ExpReq (Data)
        ExpInd (Data)
        

  Expedited data from user 2 may overtake normal data from user 2. Normal and expedited data in either direction is interleaved.

• User 1 may initiate reset. This is unconfirmed, reliable and has primitives:

        ResetReq (Reas)
        ResetInd (Reas)
        

  Simultaneous resets by both users acknowledge each other. Reset interrupts then resumes data transfer.

• User 2 may initiate disconnection. This is unconfirmed, occurs strictly consecutively and has primitives:

        DiscReq ()
        DiscInd ()
        

  Disconnection breaks any existing connection then allows a further connection attempt.

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 one level to LOTOS Utilities