Abstract
Formal specification of software components, as a core research area in software engineering, has been widely studied in 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, we 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 as an implementation is built based on this specification. In addition, we also discuss a priority upgrading approach to handle possible starvation situation of low-priority data items in the priority queue.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Bidoit, M., Hennicker, R.: An algebraic semantics for contract-based software components. In: Bevilacqua, V., Roşu, G. (eds.) AMAST 2008. LNCS, vol. 5140, pp. 216–231. Springer, Heidelberg (2008)
Breitling, M., Philipps, J.: Diagrams for dataflow. In: Proceedings of Formale Beschreibungstechniken für verteilte Systeme (FBT), pp. 101–110. Verlag Shaker (2000)
Dosch, W., Hu, G.: On irregular behaviours of interactive stacks. In: Proceedings of 4th International Conference on Information Technology: New Generations, pp. 693–700. IEEE Computer Society, Los Alamitos (2007)
Dosch, W., Ruanthong, W.: On history-sensitive models of interactive queues. In: Proceedings of the 5th International Conference on Computer and Information Science, pp. 271–278. IEEE Computer Society, Los Alamitos (2006)
Dosch, W., Stümpel, A.: Transforming stream processing functions into state transition machines. In: Dosch, W., Lee, R.Y., Wu, C. (eds.) SERA 2004. LNCS, vol. 3647, pp. 1–18. Springer, Heidelberg (2006)
Horst, J., Messina, E., Kramer, T., Huang, H.M.: Precise definition of software component specifications. In: Proceedings of the 7th Symposium on ComputerAided Control System Design, pp. 145–150 (1997)
Hu, G.: Formal specification of bounded buffer using stream functions. In: Proceedings of the IEEE International Conference on Information Reuse and Integration, pp. 230–235. IEEE System, Man, and Cybernetics Society, Las Vegas (2009)
Lau, K.-K., Ornaghi, M.: A formal approach to software component specification. In: Proceedings of Specification and Verification of Component-based Systems Workshop at OOPSLA 2001 (2001)
Object Management Group.: Unified modeling language: infrustrcture, version 2.0. Tech. rep., OMG (2003)
Övergaard, G.: Formal specification of object-oriented meta-modelling. In: FASE 2000. LNCS, vol. 1783, pp. 193–207. Springer, Heidelberg (2000)
Smith, G.: The Object-Z specification language. In: Advances in Formal Methods. Kluwer Academic, Dordrecht (2000)
Stephens, R.: A survey of stream processing. Acta-Informatica 34(7), 491–541 (1997)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2011 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Zhang, J., Hu, G., Lee, R. (2011). Formal Specification and Implementation of Priority Queue with Starvation Handling. In: Lee, R. (eds) Computer and Information Science 2011. Studies in Computational Intelligence, vol 364. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-21378-6_12
Download citation
DOI: https://doi.org/10.1007/978-3-642-21378-6_12
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-21377-9
Online ISBN: 978-3-642-21378-6
eBook Packages: EngineeringEngineering (R0)