A RECURSIVE PROCESS ALGEBRA FOR QUEUES


YENIGUN H., HAGHVERDI E., BILGEN S., INAN K.

FORMAL DESCRIPTION TECHNIQUES, VI, vol.22, pp.285-300, 1994 (SCI-Expanded) identifier

  • Publication Type: Article / Article
  • Volume: 22
  • Publication Date: 1994
  • Journal Name: FORMAL DESCRIPTION TECHNIQUES, VI
  • Journal Indexes: Science Citation Index Expanded (SCI-EXPANDED)
  • Page Numbers: pp.285-300
  • Middle East Technical University Affiliated: No

Abstract

We present a new algebra for processes that involve queueing operations. The algebra uses operators from CSP with extensions that uses dynamical event alphabets [1] and a new process operator for modeling FIFO process queueing. Two methods are suggested for deriving a buffered automaton from a given I/O (Mealy) automaton and the second one is applied to derive a general algebraic model for an SDL program. The algebra has the power to express the global state of an SDL program in terms of an algebraic expression and Can be used as a tool for verification and animation purposes. The idea, in principle, is applicable to the specification language ESTELLE and can also be integrated in LOTOS to avoid using ADTs for FIFO queues.