nach oben

Erschienen in:

2017 | OriginalPaper | Buchkapitel

Verifying Atomicity Preservation and Deadlock Freedom of a Generic Shared Variable Mechanism Used in Model-To-Code Transformations

verfasst von : Dan Zhang, Dragan Bošnački, Mark van den Brand, Cornelis Huizing, Bart Jacobs, Ruurd Kuiper, Anton Wijs

Erschienen in: Model-Driven Engineering and Software Development

Verlag: Springer International Publishing

Einloggen

Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.

search-config

KI-gestützte Suche

Aus

Abstract

A challenging aspect of model-to-code transformations is to ensure that the semantic behavior of the input model is preserved in the output code. When constructing concurrent systems, this is mainly difficult due to the non-deterministic potential interaction between threads. In this paper, we consider this issue for a framework that implements a transformation chain from models expressed in the state machine based domain specific language SLCO to Java. In particular, we provide a fine-grained generic mechanism to preserve atomicity of SLCO statements in the Java implementation. We give its generic specification based on separation logic and verify it using the verification tool VeriFast. The solution can be regarded as a reusable module to safely implement atomic operations in concurrent systems. Moreover, we also prove with VeriFast that our mechanism does not introduce deadlocks. The specification formally ensures that the locks are not reentrant which simplifies the formal treatment of the Java locks.

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

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!

Jetzt informieren

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!

Jetzt informieren

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!

Jetzt informieren

Vorheriges Kapitel Empirical Investigation of Scrumban in Global Software Development

Nächstes Kapitel Process Oriented Training with ADOxx: A Model-Based Realisation in Learn PAd

There is an extended version of SLCO allowing multiple statements per transition. In this paper, we consider the basic language, since extended SLCO models can be translated to basic SLCO models [7].

The files can be obtained from http://www.mdsetechnology.org/attachments/article/3/LockingUnlockingSpec.zip.

http://www.eclipse.org/xtend.

Abadi, M., Flanagan, C., Freund, S.N.: Types for safe locking: static race detection for java. ACM Trans. Program. Lang. Syst. 28(2), 207–255 (2006)CrossRef

Biswas, S., Huang, J., Sengupta, A., Bond, M.D.: DoubleChecker: efficient sound and precise atomicity checking. In: ACM SIGPLAN Notices, vol. 49, pp. 28–39. ACM (2014)

Blech, J., Glesner, S., Leitner, J.: Formal verification of java code generation from UML models. In: Fujaba Days, pp. 49–56 (2005)

Bošnački, D., Brand, M., Gabriels, J., Jacobs, B., Kuiper, R., Roede, S., Wijs, A., Zhang, D.: Towards modular verification of threaded concurrent executable code generated from DSL models. In: Braga, C., Ölveczky, P.C. (eds.) FACS 2015. LNCS, vol. 9539, pp. 141–160. Springer, Cham (2016). doi:10.1007/978-3-319-28934-2_8 CrossRef

Chaki, S., Clarke, E., Groce, A., Jha, S., Veith, H.: Modular verification of software components in C. In: ICSE, pp. 385–395. IEEE (2003)

Choi, J.D., Lee, K., Loginov, A., O’Callahan, R., Sarkar, V., Sridharan, M.: Efficient and precise datarace detection for multithreaded object-oriented programs. In: ACM SIGPLAN Notices, vol. 37, pp. 258–269. ACM (2002)

Engelen, L.: From Napkin sketches to reliable software. Ph.D. thesis, Eindhoven University of Technology (2012)

Engler, D., Ashcraft, K.: RacerX: effective, static detection of race conditions and deadlocks. In: ACM SIGOPS Operating Systems Review, vol. 37, pp. 237–252. ACM (2003)

Farzan, A., Madhusudan, P.: Causal atomicity. In: Ball, T., Jones, R.B. (eds.) CAV 2006. LNCS, vol. 4144, pp. 315–328. Springer, Heidelberg (2006). doi:10.1007/11817963_30 CrossRef

10.

Flanagan, C., Qadeer, S.: A type and effect system for atomicity. In: ACM SIGPLAN Notices, vol. 38, pp. 338–349. ACM (2003)

11.

Havender, J.W.: Avoiding deadlock in multitasking systems. IBM Syst. J. 7(2), 74–84 (1968)CrossRef

12.

Jacobs, B., Smans, J., Philippaerts, P., Vogels, F., Penninckx, W., Piessens, F.: VeriFast: a powerful, sound, predictable, fast verifier for C and java. In: Bobaru, M., Havelund, K., Holzmann, G.J., Joshi, R. (eds.) NFM 2011. LNCS, vol. 6617, pp. 41–55. Springer, Heidelberg (2011). doi:10.1007/978-3-642-20398-5_4 CrossRef

13.

Jacobs, B., Bosnacki, D., Kuiper, R.: Modular termination verification: extended version. Technical report, Department of Computer Science, KU Leuven (2015)

14.

Jhala, R., Majumdar, R.: Software model checking. ACM Comput. Surv. 41(4), 1–54 (2009)CrossRef

15.

Kleppe, A., Warmer, J., Bast, W.: MDA Explained: the Model Driven Architecture: Practice and Promise. Addison-Wesley Professional, Boston (2005)

16.

Kolovos, D., Rose, L., Garca-Dominguez, A., Paige, R.: The Epsilon Book. Eclipse (2011)

17.

Leino, K.R.M., Müller, P., Smans, J.: Deadlock-free channels and locks. In: Gordon, A.D. (ed.) ESOP 2010. LNCS, vol. 6012, pp. 407–426. Springer, Heidelberg (2010). doi:10.1007/978-3-642-11957-6_22 CrossRef

18.

O’Hearn, P., Reynolds, J., Yang, H.: Local reasoning about programs that alter data structures. In: Fribourg, L. (ed.) CSL 2001. LNCS, vol. 2142, pp. 1–19. Springer, Heidelberg (2001). doi:10.1007/3-540-44802-0_1 CrossRef

19.

Owicki, S., Gries, D.: Verifying properties of parallel programs: an axiomatic approach. Commun. ACM 19(5), 279–285 (1976)MathSciNetCrossRefMATH

20.

Putter, S., Wijs, A.: Verifying a verifier: on the formal correctness of an LTS transformation verification technique. In: Stevens, P., Wąsowski, A. (eds.) FASE 2016. LNCS, vol. 9633, pp. 383–400. Springer, Heidelberg (2016). doi:10.1007/978-3-662-49665-7_23 CrossRef

21.

Rahim, L., Whittle, J.: A survey of approaches for verifying model transformations. Softw. Syst. Model. 14(2), 1003–1028 (2015)CrossRef

22.

Reynolds, J.C.: Separation logic: a logic for shared mutable data structures. In: 17th Annual IEEE Symposium on Logic in Computer Science, pp. 55–74. IEEE (2002)

23.

Stenzel, K., Moebius, N., Reif, W.: Formal verification of QVT transformations for code generation. In: Whittle, J., Clark, T., Kühne, T. (eds.) MODELS 2011. LNCS, vol. 6981, pp. 533–547. Springer, Heidelberg (2011). doi:10.1007/978-3-642-24485-8_39 CrossRef

24.

Tuerk, T.: A formalisation of smallfoot in HOL. In: Berghofer, S., Nipkow, T., Urban, C., Wenzel, M. (eds.) TPHOLs 2009. LNCS, vol. 5674, pp. 469–484. Springer, Heidelberg (2009). doi:10.1007/978-3-642-03359-9_32 CrossRef

25.

Visser, W., Havelund, K., Brat, G., Park, S., Lerda, F.: Model checking programs. Autom. Softw. Eng. 10(2), 203–232 (2003)CrossRef

26.

Wijs, A.: Define, verify, refine: correct composition and transformation of concurrent system semantics. In: Fiadeiro, J.L., Liu, Z., Xue, J. (eds.) FACS 2013. LNCS, vol. 8348, pp. 348–368. Springer, Cham (2014). doi:10.1007/978-3-319-07602-7_21

27.

Wijs, A., Engelen, L.: Efficient property preservation checking of model refinements. In: Piterman, N., Smolka, S.A. (eds.) TACAS 2013. LNCS, vol. 7795, pp. 565–579. Springer, Heidelberg (2013). doi:10.1007/978-3-642-36742-7_41 CrossRef

28.

Wijs, A., Engelen, L.: REFINER: towards formal verification of model transformations. In: Badger, J.M., Rozier, K.Y. (eds.) NFM 2014. LNCS, vol. 8430, pp. 258–263. Springer, Cham (2014). doi:10.1007/978-3-319-06200-6_21 CrossRef

29.

Zhang, D., Bošnački, D., van den Brand, M., Engelen, L., Huizing, C., Kuiper, R., Wijs, A.: Towards verified java code generation from concurrent state machines. In: AMT. CEUR Workshop Proceedings, vol. 1277, pp. 64–69. CEUR-WS.org (2014)

30.

Zhang, D., Bošnački, D., van den Brand, M., Huizing, C., Jacobs, B., Kuiper, R., Wijs, A.: Verification of atomicity preservation in model-to-code transformations. In: Fourth International Conference on Model-Driven Engineering and Software Development (MODELSWARD 2016), pp. 578–588. SCITEPRESS (2016)

Titel: Verifying Atomicity Preservation and Deadlock Freedom of a Generic Shared Variable Mechanism Used in Model-To-Code Transformations
verfasst von: Dan Zhang
Dragan Bošnački
Mark van den Brand
Cornelis Huizing
Bart Jacobs
Ruurd Kuiper
Anton Wijs
Verlag: Springer International Publishing
Buch: Model-Driven Engineering and Software Development
Print ISBN: 978-3-319-66301-2

Electronic ISBN: 978-3-319-66302-9

Copyright-Jahr: 2017
DOI: https://doi.org/10.1007/978-3-319-66302-9_13

Springer Professional

Abstract

Bitte loggen Sie sich ein, um Zugang zu Ihrer Lizenz zu erhalten.

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Springer Professional "Technik"

Springer Professional "Wirtschaft"