A Comprehensive and Integrated Framework for Formal Specification of Concurrent Systems

Authors: Sara Sharifi Rad, Hassan Haghighi

Abstract:

Due to important issues, such as deadlock, starvation, communication, non-deterministic behavior and synchronization, concurrent systems are very complex, sensitive, and error-prone. Thus ensuring reliability and accuracy of these systems is very essential. Therefore, there has been a big interest in the formal specification of concurrent programs in recent years. Nevertheless, some features of concurrent systems, such as dynamic process creation, scheduling and starvation have not been specified formally yet. Also, some other features have been specified partially and/or have been described using a combination of several different formalisms and methods whose integration needs too much effort. In other words, a comprehensive and integrated specification that could cover all aspects of concurrent systems has not been provided yet. Thus, this paper makes two major contributions: firstly, it provides a comprehensive formal framework to specify all well-known features of concurrent systems. Secondly, it provides an integrated specification of these features by using just a single formal notation, i.e., the Z language.

Keywords: Concurrent systems, Formal methods, Formal specification, Z language

Digital Object Identifier (DOI): doi.org/10.5281/zenodo.1060958

References:

[1] P. Brinch Hansen, "Operating System Principles," Prentic-Hall,1973.
[2] J. Bacon, J. Van der Linden, "Concurrent Systems: an integrated approach to operating systems, distributed systems and databases," 3nd Edition, international computer science series, 2002.
[3] A.J. Bijoy, D.P. Hiren, "Generating Multi-Threaded Code from Polychronous Specifications," ElsevierJournal, Electronic Notes In Theoretical Computer Science, vol. 238, 2009, pp. 57-69.
[4] S.C. Harpreet, W.B John, and M.W Jeanette, " Formal Specification of Concurrent Systems," Elsevier Journal, Advances In Engineering Software, vol. 30, 1999, pp. 211-224.
[5] H. Haghighi, "Towards a Formal Framework for Developing Concurrent Programs: Modeling Dynamic Behavior," Proc. The eighth ACS/IEEE International Conference on Computer Systems and Applications (AICCSA-10), Hammamet, Tunisia, 2010.
[6] O. Mosbahi, L. Jemni Ben Ayed, and M. Khalgui ,"A Formal Approach for The Development of Reactive Systems," Elsevier Journal, Information and Software Technology,vol. 53, pp. 14-33, 2011.
[7] N. Aoumeur, K. Barkaoui, and G. Saake, "Towards MAUDE-TLA based Foundation for Complex Concurrent Systems Specification and Certification," IEEE Fifth International Conference on Information Technology: New Generation, 2008.
[8] M. Yusufa, G. Yusufu, "Comparison of SoftwareSpecification Methods Using a Case Study," IEEE International conference on computer science and software Engineering, 2008.
[9] R. Duke, I. J. Hayes, P. King, and G. A. Rose, "Protocol Specification and Verification Using Z" In IFIP Eighth International Workshop on Protocol Specification, Testing and Verification, North-Holland, 1988, pp. 33-46.
[10] E. Fergus, D. Ince, "Z Specifications and Modal Logic," Proceedings of Software Engineering 90, Brighton, Ed. Patrick Hall, Cambridge University Press, July 1990.
[11] L. Lamport, "TLZ," Proceeding of the 8th Z Users Meeting, Cambridge, Springer Verlage, 1994.
[12] J.C.P Woodcook, and C. Morgan, "Refinement of State-Based Concurrent Systems," Procs. Of VDM 90, Springer Verlag, 1990,pp.341-351
[13] D. Safranek, "Visual Specification of Concurrent Systems," IEEE International Conference on Automated Software Engineering, 2003.
[14] D. Safranek, "Visual Specification of Systems with Heterogeneous Coordination Models," Elsevier Electronic Notes in theoretical computer Science, 2007, pp. 107-121.
[15] A.S. Evans, "Specifying & Verifying Concurrent Systems Using Z," In: ISCIS XI, Turkey 1994.
[16] M. Pilling, A. Buruns, and K. Raymond, "Formal Specification and Proof of Inheritance Protocols for Real_Time Scheduling," IEEE Software Engineering Journal, vol. 5, September 1990, pp.236-279.
[17] X. He, "PZ nets_a formal method integrating petrinets whit Z," Elsevier Information and Software Technology, vol.43 ,2001, pp.1-18.
[18] P. Stocks, K. Raymond, D. Carrington, and A. Lister, "Modelling Open Distributed Systems in Z," Elsevier computer Communications, vol.15, March1992, pp. 103-113.
[19] C. Chu Chiang, "Development of Concurrent Systems Through Coordination," IEEE International Conference on Information Technology, 2005.
[20] V. Kumar Garg, "Specification and Analysis of Concurrent Systems Using STOCS model," IEEE Computer Networking Symposium, 1988.
[21] D.E. Cook, "Formal Specification of Resource-Deadlock Prone Petri Net," Elsevier Systems Software Journal, vol.11, 1990, pp.53-69.
[22] N.D. Francesco, G. Vaglini, "Modular Verification of Correctness Properties in Enviorment for Concurrent Systems Specification Deadlock Case," Elsevier Information Software Technology, vol.32, October 1990, pp.133-148.
[23] J. Woodcock, J. Davies, "Using Z, Specification, Refinment and Proof," Prentic Hall, 1996.
[24] H. Haghighi, S.H, Mirian-Hosseinabadi, "Nondeterminism in Constructive Z," Fundamenta Informatica, Vol.88, 2008, pp. 109-134.
[25] V. Varadharjan, "Use of a Formal Description Technique in the Specification of Authentication Protocols," Elsevier Computer Standards and Interfaces,vol. 9, 1990, pp.203-215.
[26] E. Spiliopoulou, "Concurrent and Distributed Functional Systems," PhD Thesis, Department of Computer Science, University of Bristol, 1999.
[27] H. Alex, S.Steven , and H. Steven, "On Deadlock,Livelock and Forward Progress," Technical Reports, university of cambridge, 2005.
[28] M.N. YousufAli, and M.Z.H. Sarker, "An Algorithm for Avoiding Deadlock,"IEEE INMIC, 9th International Multitopic Conference, 2005.
[29] K.Ch. Tai, "Definition and Detection of Deadlock, LiveLock, and Starvation in Concurrent Programs," IEEE Computer Society, International Conference on Parallel Processing, vol.2, 1994, pp.69-72.
[30] H.D. Karatza, "Scheduling Gang in a Distributed System," ninth IEEE Workshop ,I.J. of simulation, May 2003, pp.15-22.
[31] S.H. Mirian-Hosseinabadi, "Constructive Z," Ph.D. dissertation, Essex Univ., 1997.