Top

Cluster Computing

Published in:

09-02-2017

Software model checking for resources race

Authors: Hong Wang, Tao Zhang

Published in: Cluster Computing | Issue 1/2017

Activate our intelligent search to find suitable subject content or patents.

search-config

AI-assisted search

Off

Abstract

The difficulty of finding resources race is well known. Such errors are hard to be detected, because they often happen irregularly and reproduce difficultly. Especially, the kind race conflicts exist among processes, threads, and interrupts. This paper provided a novel approach to detect the resources race, namely software model checking. It constructed Boolean program and Promela models for resources race. Furthermore, the Promela models have been tested by using the model checker, SPIN. Software model checking can detect resources race in concurrent program without running, although the program had used timing control or mutual exclusion lock to avoid the race. Furthermore, it can find deadlock also, if the program use the mutual locks in a wrong way.

previous article Study on similarity based on connection degree in social network

next article The research on the mechanism and spatial–temporal differentiation of the coupling coordination development based on industrial cluster agglomeration

Dont have a licence yet? Then find out more about our products and how to get one now:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

über 102.000 Bücher
über 537 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Finance + Banking
Management + Führung
Marketing + Vertrieb
Maschinenbau + Werkstoffe
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

inform now

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 390 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Maschinenbau + Werkstoffe

Jetzt Wissensvorsprung sichern!

inform now

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 340 Zeitschriften

aus folgenden Fachgebieten:

Bauwesen + Immobilien
Business IT + Informatik
Finance + Banking
Management + Führung
Marketing + Vertrieb
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

inform now

Tchamgoue, G.M., Kim, K.H., Jun, Y.K.: Verification of data races in concurrent interrupt handlers. Int. J. Distrib. Sens. Netw. 2013, 1–15 (2013)

Banerjee, U., Bliss, B., Ma, Z., Petersen, P.: A theory of data race detection. In: PADTAD-IV ACM, pp. 69–78, Portland (2006)

Tchamgoue, G.M., Kim, K.H., Jun, Y.K.: Dynamic race detection techniques for interrupt-driven programs. In: FGIT, LNCS 7709, pp. 148–153. Springer, Berlin (2012)

Ping, W., Yiyun, C., Jian, Z.: Static data-race detection for multithread programs. J. Comput. Res. Dev. 43, 329–337 (2006)CrossRef

Engler, D., Ashcraft, K.: RacerX: effective, static detection of race conditions and deadlocks. In: Proceedings of the SOSP’03, Bolton Landing, New York, USA, October 19–22, pp. 237–252 (2003)

Tchamgoue, G.M., Kim, K.H., Jun, Y.K.: Dynamic race detection Techniques for interrupt-driven programs. In: FGIT, :LNCS 7709, pp. 148–153. Springer, Berlin (2012)

Flanagan, C., Freund, S.N.: FastTrack: efficient and precise dynamic race detection. ACM Sigplan Not. 44, 121–133 (2009)CrossRef

křena, B., Letko, Z., Tzoref, R.: Healing data races on-the-fly. In: Proceedings of the 2007 ACM workshop on Parallel and distributed systems: testing and debugging, pp. 54–64. ACM (2007)

Kahlon, V., Sinha, N., Zhang, Y.: Static data race detection for concurrent programs with asynchronous calls. In: ESEC/FSE ’09 Proceedings of the the 7th joint meeting of the European software engineering conference and the ACM SIGSOFT symposium on The foundations of software engineering, pp. 13–22 (2009)

10.

Yang, Y., Gringauze, A., Wu, D., Rohde, H.K.: Detecting data race and atomicity violation via typestate-guided static analysis. US Patent 8,510,722 (2013)

11.

Carr, S., Mayo, J., Shene, C.K.: Race conditions : a case study. J. Comput. Small Coll. 17: 88–102 (2001)

12.

Clarke, E.M., Emerson, A., Sifakis, J.: Model checking: algorithmic verification and debugging. Commun. ACM 52(11), 74–84 (2007)CrossRef

13.

Clarke, E.M.: The birth of model checking. 25 Years of Model Checking (2008)

14.

Thomas, W.: Computation tree logic and regular omega-languages. J. Linear Time Branch. Time Partial Order Log. Models Concurr. 66(3): 1011–1057 (1989)

15.

Hammer, M., Knapp, A., Merz, S.: Truly on-the-fly LTL model checking. In: Halbwachs, N., Zuck, L. (eds.), TACAS, LCNS 3440. Springer, Heidelberg (2005)

16.

Kupferman, O., Vardi, M.Y.: Model checking of safety properties. J. Form. Methods Syst. Des. 19(3), 291–314 (2001)CrossRefMATH

17.

McMillan, K.L.: Parameterized verification of the FLASH cache coherence protocol by compositional model checking. In: CHARME 01: IFIP Working Conference on Correct Hardware Design and Verification Methods: LNCS 2144, pp. 179–195. Springer, Heidelberg (2001)

18.

Norman, G., Parker, D., Sproston, J.: Model checking for probabilistic timed automata. J. Form. Methods Syst. Des. 43(2), 164–190 (2013)CrossRefMATH

19.

Visser, W.: Model checking programs. In: 15th IEEE International Conference on Automated Software Engineering, pp. 203–232. IEEE Press, New York (2000)

20.

Ball, T., Levin, V., Rajamani, S.K.: A decade of software model checking with SLAM. Commun. ACM 54(7), 68–76 (2011)CrossRef

21.

Cimatti, A., et al.: NuSMV 2: an opensource tool for symbolic model checking. In: International Conference on Computer Aided Verification, pp. 359–364. Springer, Berlin (2010)

22.

Holzmann, G.J.: Software model checking with spin. Adv. Comput. 65(05), 77–108 (2005)CrossRef

23.

Graf, S., Saidi, H.: Construction of abstract state graphs with PVS. In: Proceedings of the Computer-aided Verication (CAV 97), pp. 72–83. Springer, Berlin (1997)

24.

Holzmann, G.J., Smith, M.H.: Software model checking: extracting verification models from source code. Softw. Test. Verif. Reliab. 11(2), 481–497 (2001)CrossRef

25.

Cimatti, A., Narasamdya, I., Roveri, M.: Software model checking SystemC. IEEE Trans. Comput.-Aided Des. Integr. Circuits Syst. 32(5), 774–787 (2013)CrossRef

26.

Visser, W., Corina, S.P., Khurshid, S.: Test Input Generation with Java PathFinder. ISSTA’04. Boston. Massachusetts, USA (2004)

27.

Holzmann, G.J.: SPIN Model Checker. The Primer and Reference Manual. Addison-Wesley Professional, Los Angeles (2003)

Title: Software model checking for resources race
Authors: Hong Wang
Tao Zhang
Publication date: 09-02-2017
Publisher: Springer US
Published in: Cluster Computing / Issue 1/2017
Print ISSN: 1386-7857
Electronic ISSN: 1573-7543
DOI: https://doi.org/10.1007/s10586-017-0757-z

Springer Professional

Abstract

Please log in to get access to your license.

Dont have a licence yet? Then find out more about our products and how to get one now:

Springer Professional "Wirtschaft+Technik"

Springer Professional "Technik"

Springer Professional "Wirtschaft"

Other articles of this Issue 1/2017

Principal agent model based design and outsourcing of information value

Multi-model recursive identification for nonlinear systems with non-uniformly sampling

Expansion slot backfill scheduling for concurrent workflows with deadline on heterogeneous resources

A terms mining and clustering technique for surveying network and content analysis of academic groups exploration

Applying the locality principle to improve the shortest path algorithm

A nanocommunication system for endocrine diseases

Premium Partner