A RECURSIVE PROCESS ALGEBRA FOR QUEUES

Date

1994-01-01

Author

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

Metadata

Show full item record

This work is licensed under a Creative Commons Attribution-NonCommercial-NoDerivatives 4.0 International License.

Item Usage Stats

104
views

0
downloads

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.

Subject Keywords

Software engineering, Software, Requirements/specifications, Tools and techniques, Program verification

URI

https://hdl.handle.net/11511/67867

Journal

FORMAL DESCRIPTION TECHNIQUES, VI

Collections

Department of Electrical and Electronics Engineering, Article

Suggestions

OpenMETU
Core

A quadtree-based adaptively-refined cartesian-grid algorithm for solution of the euler equations Bulkök, Murat; Aksel, Mehmet Haluk; Department of Mechanical Engineering (2005) A Cartesian method for solution of the steady two-dimensional Euler equations is produced. Dynamic data structures are used and both geometric and solution-based adaptations are applied. Solution adaptation is achieved through solution-based gradient information. The finite volume method is used with cell-centered approach. The solution is converged to a steady state by means of an approximate Riemann solver. Local time step is used for convergence acceleration. A multistage time stepping scheme is used to ...
VERIFICATION BY CONSECUTIVE PROJECTIONS HAGHVERDI, E; INAN, K (1993-01-01) A new complexity relief technique for verifying formal specifications based on finite state machines is described. The method uses a Hoare's CSP-like nondeterministic semantics instead of the more commonly used observational equivalence and thus offers greater simplification without an essential loss of information. The approach is based on two algebraic operators on processes that perform parallel composition and process projection. It is shown that under appropriate conditions the complexity raising opera...
An improved algorithm for iterative matrix-vector multiplications over finite fields Mangır, Ceyda; Cenk, Murat; Manguoğlu, Murat (2018-11-09) Cryptographic computations such as factoring integers and computing discrete logarithms over finite fields require solving a large system of linear equations. When dealing with such systems iterative approaches such as Wiedemann or Lanczos are used. Both methods are based on the computation of a Krylov subspace in which the computational cost is often dominated by successive matrix-vector products. We introduce a new algorithm for computing iterative matrix-vector multiplications over finite fields. The pro...
A Stagnation aware cooperative breakout local search algorithm for the quadratic assignment problem on a multi-core architecture Aksan, Yağmur; Coşar, Ahmet; Dökeroğlu, Tansel; Department of Computer Engineering (2016) The quadratic assignment problem (QAP) is one of the most challenging NP-Hard combinatorial optimization problems with its several real life applications. Layout design, scheduling, and assigning gates to planes at an airport are some of the interesting applications of the QAP. In this thesis, we improve the talents of a recent local search heuristic Breakout Local Search Algorithm (BLS) by using adapted Levenshtein Distance metric for similarity checking of the previously explored permutations of the QAP p...
A NOVEL PARTITIONING METHOD FOR ACCELERATING THE BLOCK CIMMINO ALGORITHM Torun, F. Sukru; Manguoğlu, Murat; Aykanat, Cevdet (2018-01-01) We propose a novel block-row partitioning method in order to improve the convergence rate of the block Cimmino algorithm for solving general sparse linear systems of equations. The convergence rate of the block Cimmino algorithm depends on the orthogonality among the block rows obtained by the partitioning method. The proposed method takes numerical orthogonality among block rows into account by proposing a row inner-product graph model of the coefficient matrix. In the graph partitioning formulation define...

Citation Formats

H. YENIGUN, E. HAGHVERDI, S. BILGEN, and K. INAN, “A RECURSIVE PROCESS ALGEBRA FOR QUEUES,” FORMAL DESCRIPTION TECHNIQUES, VI, pp. 285–300, 1994, Accessed: 00, 2020. [Online]. Available: https://hdl.handle.net/11511/67867.