A RECURSIVE PROCESS ALGEBRA FOR QUEUES


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

FORMAL DESCRIPTION TECHNIQUES, VI, cilt.22, ss.285-300, 1994 (SCI İndekslerine Giren Dergi) identifier

  • Cilt numarası: 22
  • Basım Tarihi: 1994
  • Dergi Adı: FORMAL DESCRIPTION TECHNIQUES, VI
  • Sayfa Sayıları: ss.285-300

Özet

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.