Formal Specification and Implementation of Priority Queue using Stream Functions

Formal Specification and Implementation of Priority Queue using Stream Functions

Gongzhu Hu (Central Michigan University, Mount Pleasant, MI, USA), Jin Zhang (Hainan University, Haikou, China) and Roger Lee (Department of Computer Science, Central Michigan University, Mount Pleasant, MI, USA)
Copyright: © 2013 |Pages: 10
DOI: 10.4018/ijsi.2013070105
OnDemand PDF Download:
$30.00
List Price: $37.50

Abstract

Formal specification of software components, as a core research area in software engineering, has been widely studied for decades. Although quite a few formal models have been proposed for this purpose, specification of concrete software components is still a challenging task due to the complexity of the functionalities of the components. In this paper, the authors use the stream function model to specify the behavior of priority queue, a commonly used software component. This specification formally defines the regular behavior and fault tolerance behavior of priority queue. In particular, a priority-concatenation operator is defined to handle the ordering of data items to ensure the highest-priority item is removed first. A finite state machine is built based on this specification as an implementation of priority queue. In addition, the authors also discuss a priority upgrading approach to handle possible starvation situation of low-priority data items in the priority queue.
Article Preview

Stream Function

First, we briefly review the basic concept of stream function as formal model for component specification.

Given an alphabet A, the set A* comprises all streams A = (α1, α2, …, αk) of length

|A| = k with element αi. Several operations can be applied to communication streams, one of the basic operator is concatenation defined as& . A* x A* → A*of two streams A = (α1, α2, …, αk) and B = (b1, b2, …, bk), that yields the stream

A & B = (α1, α2, …, αk, b1, b2, …, bk) (1)

A stream function f . A* → B* maps an input stream to an output stream (Stephens, 1997).

Complete Article List

Search this Journal:
Reset
Open Access Articles: Forthcoming
Volume 6: 4 Issues (2018): 1 Released, 3 Forthcoming
Volume 5: 4 Issues (2017)
Volume 4: 4 Issues (2016)
Volume 3: 4 Issues (2015)
Volume 2: 4 Issues (2014)
Volume 1: 4 Issues (2013)
View Complete Journal Contents Listing