Abstract
An important problem in Model Driven Engineering is maintaining the correctness of a specification under model transformations. We consider this issue for a framework that implements the transformation chain from the modeling language SLCO to Java. In particular, we verify the generic part of the last transformation step to Java code, involving change in granularity, focusing on the implementation of SLCO communication channels. To this end we use a parameterized modular approach; we apply a novel proof schema that supports fine grained concurrency and procedure-modularity, and use the separation logic based tool VeriFast. Our results show that such tool-assisted formal verification can be a viable addition to traditional techniques, supporting object orientation, concurrency via threads, and parameterized verification.
R. Kuiper, A. Wijs and D. Zhang—This work was done with financial support from the China Scholarship Council (CSC), the Netherlands Organisation for Scientific Research (NWO), and ARTEMIS Joint Undertaking project EMC2 (grant agreement 621429).
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Notes
- 1.
Here we disregard the usual side condition of the frame rule, since we assume a Java-like programming language not supporting global variables.
- 2.
In the classical Owicki-Gries framework this is directly forbidden by the interplay of the syntactic rules of the usage of the global variable and the side conditions of the axioms for CR and parallel composition.
References
van Amstel, M., van den Brand, M., Engelen, L.: An exercise in iterative domain-specific language design. In: EVOL/IWPSE. pp. 48–57. ACM (2010)
Baalen, J.V., Robinson, P., Lowry, M., Pressburger, T.: Explaining synthesized software. In: ASE. pp. 240–248. IEEE (1998)
Beckert, B., Hähnle, R., Schmitt, P. (eds.): Verification of Object-Oriented Software. LNCS (LNAI), vol. 4334. Springer, Heidelberg (2007)
Blech, J., Glesner, S., Leitner, J.: Formal verification of java code generation from UML models. In: Fujaba Days, pp. 49–56 (2005)
Bornat, R., Calcagno, C., O’Hearn, P., Parkinson, M.: Permission accounting in separation logic. ACM SIGPLAN Not. 40(1), 259–270 (2005)
Burdy, L., Cheon, Y., Cok, D., Ernst, M., Kiniry, J., Leavens, G., Leino, K., Poll, E.: An overview of JML tools and applications. STTT 7(3), 212–232 (2005)
Chaki, S., Clarke, E., Groce, A., Jha, S., Veith, H.: Modular verification of software components in C. In: ICSE, pp. 385–395. IEEE (2003)
Leavens, G.T., Poll, E., Kiniry, J.R., Chalin, P.: Beyond assertions: advanced specification and verification with JML and ESC/Java2. In: de Boer, F.S., Bonsangue, M.M., Graf, S., de Roever, W.-P. (eds.) FMCO 2005. LNCS, vol. 4111, pp. 342–363. Springer, Heidelberg (2006)
Denney, E., Fischer, B.: Generating customized verifiers for automatically generated code. In: GPCE, pp. 77–88. ACM (2008)
Denney, E., Fischer, B., Schumann, J., Richardson, J.: Automatic certification of kalman filters for reliable code generation. In: IEEE Aerospace Conference. pp. 1–10. IEEE (2005)
Dijkstra, E.W.: Cooperating sequential processes. In: Brinch Hansen, P. (ed.) The Origin of Concurrent Programming. From Semaphores to Remote Procedure Calls, pp. 65–138. Springer, New York (2002)
Fogelberg, C., Potanin, A., Noble, J.: Ownership meets java. In: IWACO, pp. 30–33 (2007)
Hoare, C.: An axiomatic basis for computer programming. Commun. ACM 12(10), 576–580 (1969)
Hoare, C.A.R.: Towards a Theory of Parallel Programming. In: Brinch Hansen, P. (ed.) The Origin of Concurrent Programming. From Semaphores to Remote Procedure Calls, pp. 231–244. Springer, New York (2002)
Jacobs, B.: VeriFast website. people.cs.kuleuven.be/\(\sim \)bart.jacobs/verifast/ (2012)
Jacobs, B., Piessens, F.: Expressive modular fine-grained concurrency specification. In: POPL, pp. 271–282. ACM (2011)
Jhala, R., Majumdar, R.: Software model checking. ACM Comput. Surv. 41(4), 21:1–21:54 (2009)
Kleppe, A., Warmer, J., Bast, W.: MDA Explained: The Model Driven Architecture(TM): Practice and Promise. Addison-Wesley Professional, Boston (2005)
Marché, C., Paulin-Mohring, C., Urbain, X.: The krakatoa tool for certification of java/javacard programs annotated in JML. J. Logic Algebraic Program. 58(1–2), 89–106 (2004)
O’Hearn, P.W., Reynolds, J.C., Yang, H.: Local reasoning about programs that alter data structures. In: Fribourg, L. (ed.) CSL 2001 and EACSL 2001. LNCS, vol. 2142, pp. 1–19. Springer, Heidelberg (2001)
Owicki, S., Gries, D.: Verifying properties of parallel programs: an axiomatic approach. Commun. ACM 19(5), 279–285 (1976)
Rahim, L., Whittle, J.: A survey of approaches for verifying model transformations. Softw. Syst. Model. 14(2), 1003–1028 (2015)
Reynolds, J.: Separation logic: a logic for shared mutable data structures. In: LICS, pp. 55–74. IEEE (2002)
Stenzel, K., Reif, W., Moebius, N.: 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)
Svendsen, K., Birkedal, L., Parkinson, M.: Joins: a case study in modular specification of a concurrent reentrant higher-order library. In: Castagna, G. (ed.) ECOOP 2013. LNCS, vol. 7920, pp. 327–351. Springer, Heidelberg (2013)
Parkinson, M., Birkedal, L., Svendsen, K.: Modular reasoning about separation of concurrent data structures. In: Felleisen, M., Gardner, P. (eds.) ESOP 2013. LNCS, vol. 7792, pp. 169–188. Springer, Heidelberg (2013)
Welch, P., Martin, J.: Formal analysis of concurrent java systems. In: CPA, pp. 275–301. IOS Press (2000)
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, Heidelberg (2014)
Wijs, A., Engelen, L.: Efficient property preservation checking of model refinements. In: Piterman, N., Smolka, S.A. (eds.) TACAS 2013 (ETAPS 2013). LNCS, vol. 7795, pp. 565–579. Springer, Heidelberg (2013)
Engelen, L., Wijs, A.: REFINER: towards formal verification of model transformations. In: Badger, J.M., Rozier, K.Y. (eds.) NFM 2014. LNCS, vol. 8430, pp. 258–263. Springer, Heidelberg (2014)
Wijs, A.: Achieving discrete relative timing with untimed process algebra. In: ICECCS, pp. 35–44. IEEE (2007)
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 (2014). CEUR-WS.org
Zibin, Y., Potanin, A., Li, P., Ali, M., Ernst, M.: Ownership and immutability in generic java. In: OOPSLA. ACM SIGPLAN Notices, vol. 45, pp. 598–617. ACM (2010)
Acknowledgments
We would like to thank Suzana Andova for the discussions in the early phases of the work described in this paper.
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2016 Springer International Publishing Switzerland
About this paper
Cite this paper
Bošnački, D. et al. (2016). Towards Modular Verification of Threaded Concurrent Executable Code Generated from DSL Models. In: Braga, C., Ölveczky, P. (eds) Formal Aspects of Component Software. FACS 2015. Lecture Notes in Computer Science(), vol 9539. Springer, Cham. https://doi.org/10.1007/978-3-319-28934-2_8
Download citation
DOI: https://doi.org/10.1007/978-3-319-28934-2_8
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-28933-5
Online ISBN: 978-3-319-28934-2
eBook Packages: Computer ScienceComputer Science (R0)