The week's pick
Random Articles
Reseach Article
A Formal Framework for Specifying Concurrent Systems
| International Journal of Computer Applications |
| Foundation of Computer Science (FCS), NY, USA |
| Volume 68 - Number 3 |
| Year of Publication: 2013 |
| Authors: Sara Sharifirad, Hassan Haghighi |
10.5120/11559-6841
|
Sara Sharifirad, Hassan Haghighi . A Formal Framework for Specifying Concurrent Systems. International Journal of Computer Applications. 68, 3 ( April 2013), 17-24. DOI=10.5120/11559-6841
Abstract
Concurrent systems are very complex and error-prone because these systems are associated with significant issues, such as deadlock, starvation, communication, non-deterministic behavior and synchronization. Using formal methods, which are based on mathematical notions and theories, can help to increase confidence in these systems. Thus in recent years, most efforts have focused to specify, verify and develop concurrent systems formally. However, with specifications that have been done up to this time, several important aspects of concurrent systems, such as dynamic process creation, scheduling, starvation and infinite execution have not been specified formally yet. On the other hand, some specified aspects, such as deadlock, synchronization and communication have not been described as completely and accurately and/or have been specified using a combination of several different methods and formalisms so that the integration of existing specifications needs too much effort. It can be said unequivocally that until now there is no specification framework, based on a single formalism, for concurrent systems in which all important aspects of these systems are considered. Thus, our previous work tried to present an integrated formal specification framework of all the extracted aspects based on just one formal notation, i. e. , the Z language. In this paper, the details of the mentioned formal framework are first presented. Then, this framework is evaluated from two viewpoints: comprehensiveness of the framework itself and appropriateness of Z to write an integrated formal specification of concurrent systems.
References
- P. Brinch Hansen, "Operating System Principles", Prentic-Hall, 1973.
- A. J. Bijoy, D. P. Hiren, "Generating Multi-Threaded Code from Polychronous Specifications", ElsevierJournal, ENTCS, vol. 238, 2009, 57–69.
- 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.
- H. Haghighi, "Towards a Formal Framework for Developing Concurrent Programs: Modeling Dynamic Behavior", Proc. AICCSA-10, Tunisia, 2010.
- S. C. Harpreet, W. B. John, M. W. Jeanette, "Formal Specification of Concurrent Systems", Advances In Engineering Software, vol. 30, 1999, 211–224.
- D. Safranek, "Visual Specification of Systems with Heterogeneous Coordination Models", ENTCS, 2007 107-121.
- P. Stocks, K. Raymond, D. Carrington, A. Lister, "Modeling Open Distributed Systems in Z", Elsevier computer Communications, vol. 15, 1992, 103–113.
- D. E. Cook, "Formal Specification of Resource-Deadlock Prone Petri Net", Elsevier Systems Software Journal, vol. 11, 1990, 53–69.
- S. Sharifirad, H. Haghighi, "A Comprehensive and Integrated Framework for Formal Specification of Concurrent Systems", International conference on software engineering and technology, Venice, Italy, November 2011.
- J. Woodcock, J. Davies, "Using Z, Specification, Refinment and Proof", Prentic Hall, 1996.
- H. Haghighi, S. H. Mirian-Hosseinabadi, "Nondeterminism in Constructive Z", Fundamenta Informatica, vol. 88, 2008, 109-134.
- R. Duke, I. J. Hayes, P. King, G. A. Rose, "Protocol Specification and Verification Using Z", In IFIP Eighth International Workshop on Protocol Specification, Testing and Verification, North-Holland, 1988, 33–46.
- L. Lamport, "TLZ", Proceeding of the 8th Z Users Meeting, Cambridge, Springer Verlage, 1994.
- J. C. P. Woodcook, C. Morgan, "Refinement of State-Based Concurrent Systems", Proc. VDM 90, Springer Verlag, 1990, 341–351.
- D. Safranek, "Visual Specification of Concurrent Systems", IEEE International Conference on Automated Software Engineering, 2003.
- A. S. Evans, "Specifying & Verifying Concurrent Systems Using Z", In: ISCIS XI, Turkey, 1994.
- J. C. P. Woodcock, A. Cavalcanti, "A Concurrent Language for Refinement", Irish Workshop in Formal Methods, 2001, 1–16.
- M. Pilling, A. Buruns, K. Raymond, "Formal Specification and Proof of Inheritance Protocols for Real_Time Scheduling", IEEE Software Engineering Journal, vol. 5, 1990, 236-279.
- X. He, "PZ nets_a formal method integrating petrinets whit Z", Elsevier Information and Software Technology, vol. 43, 2001, 1–18.
- C. Chu Chiang, "Development of Concurrent Systems through Coordination", IEEE International Conference on Information Technology, 2005.
- V. Kumar Garg, "Specification and Analysis of Concurrent Systems Using STOCS model", IEEE Computer Networking Symposium, 1988.
- N. D. Francesco, G. Vaglini, "Modular Verification of Correctness Properties in Enviorment for Concurrent Systems Specification Deadlock Case", Elsevier Information Software Technology, vol. 32, 1990, 133–148.
Index Terms
Keywords