A Comprehensive and Integrated Framework for Formal Specification of Concurrent Systems
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.
[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.
[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.
@article{"International Journal of Information, Control and Computer Sciences:54485", author = "Sara Sharifi Rad and Hassan Haghighi", title = "A Comprehensive and Integrated Framework for Formal Specification of Concurrent Systems", 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", volume = "5", number = "11", pages = "1279-9", }
