A Framework to Automatic Deadlock Detection in Concurrent Programs

• Autorzy: Mahdian F. , Rafe V. , Rafeh R.

Warianty tytułu

PL

Struktura automatycznego wykrywania zakleszczeń w oprogramowaniu charakteryzującym się zgodnością

• Języki publikacji: EN

Abstrakty

EN

Nowadays, concurrency is one of the most common features of software systems. In such systems, different parts of the system either are working together or separately. In these cases, deadlock is a common defect. In many systems –especially safety critical ones- deadlock is a serious problem. Hence, it is very important to find them before deploying the system. Since model checking is an accurate mechanism to automatically verify software and hardware systems, using this technique is a proper solution to automatic deadlock detection. In this paper, we present an approach to automatic deadlock detection using Bogor – a well known model checker. To do so, at first, we determine global variables, shared resources and in general, all parts that may cause a deadlock. Then, we translate them to BIR – the input language of the Bogor. Bogor generates the transition system and shows that if there is any deadlock in the program. In the cases in which Bogor finds a deadlock, it shows a counter example to help programmers to fix the problem. To illustrate all the main concepts of the approach, we use different concurrent Java programs as case studies.

PL

oprogramowaniu charakteryzującym się zgodnością różne części mogą pracować niezależnie lub wspólnie. Największym problemem w tego typu programach jest stan zakleszczenia (deadlock). Dlatego ważne jest stworzenie mechanizmu automatycznego wykrywania takiej sytuacji. W artykule opisano metodę Bogor, w tym także BIR – język wejściowy do Bogor.

Słowa kluczowe

EN

verification; concurrent programming; model checking; Bogor; BIR

PL

Bogor; zakleszczenia programu; zgodnośc oprogramnowania

• Wydawca: Wydawnictwo SIGMA-NOT
• Czasopismo: Przegląd Elektrotechniczny
• Rocznik: 2012
• Tom: R. 88, nr 1b
• Strony: 182--184
• Opis fizyczny: Bibliogr. 13 poz., rys., schem.

Twórcy

autor

Mahdian F.

autor

Rafe V.

autor

Rafeh R.

• Department of Computer Engineering, Toyserkan Branch, Islamic Azad University, Toyserkan, Iran,

Bibliografia

• [1] C. Baier and J.P. Katoen. Principals of Model Checking. The MIT Press, (2008)
• [2] E.M. Clarke, O. Grumberg, and D.A. Peled.: Model Checking. The MIT Press (2000)
• [3] R.H. Carver and K.C. Tal, Modern multithreading : implementing, testing, and debugging multithreaded Java and C++/Pthreads/Win32 programs, Wiley, (2006)
• [4] M. Sirjani, "formal specification and verification of concurrent and reactive systems", Doctoral Dissertation, Dep. of Computer Sciences, Sharif University of Technology, Iran (2004)
• [5] Robby, Dwyer, M.B., Hatcliff, J.: Bogor: An extensible and highly-modular software model checking framework. Proc. of the 9th European software engineering Conf. (2003) 267–276
• [6] V. Rafe, A. T. Rahmani, L. Baresi, P. Spoletini: “Towards Automated Verification of Layered Graph Transformation Specifications”, Journal of IET Software, Vol.3 No.4, pp. 276- 291 (2009).
• [7] V. Rafe and A. T. Rahmani: “A Novel Approach to verify graph Schema-Based software systems”, Journal of Software Engineering and Knowledge Engineering (IJSEKE), Vol. 19, No. 6, pp 857-870, (2009).
• [8] V. Rafe and A. T. Rahmani: “Towards Automated Software Model Checking Using Graph Transformation Systems and Bogor”, journal of Zhejiang University- Science A (JZUS), No.8, pp. 1093-1105 (2009).
• [9] G. Brat, K. Havelund, S. Park and W. Visser, "Model Checking Programs," Proc. ASE'00: 15th IEEE Int'l Conf. on Automated Software Engineering, Grenoble, France, pp. 3-11, 2000.
• [10] M. Huisman and B. Jacobs, “Java Program Verification via Hoare Logic with Abrupt Termination”, In Proc. of the Third Internationsl Conf. on Fundamental Approaches to Software Eng. Held as Part of the European Joint Conferences on the Theory and Practice of Software. (ETAPS), pp.284-303, (2000)
• [11] NuSMV, nusmv.irst.itc.it/NuSMV/.
• [12] SPIN, netlib.belllabs.com/netlib/spin/
• [13] H. Liu and J.S. Moore, "Java program verification via a JVM deep embedding in ACL2", In Proc. of the 17th International Conference on Theorem Proving in Higher Order Logics (TPHOLs), pp. 184-200, (2004)