{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,9,10]],"date-time":"2025-09-10T21:51:29Z","timestamp":1757541089738,"version":"3.37.3"},"reference-count":29,"publisher":"Springer Science and Business Media LLC","issue":"1","license":[{"start":{"date-parts":[[2017,2,13]],"date-time":"2017-02-13T00:00:00Z","timestamp":1486944000000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"funder":[{"DOI":"10.13039\/501100003339","name":"Consejo Superior de Investigaciones Cient\u00edficas","doi-asserted-by":"publisher","award":["StrongSoft - TIN2012-39391-C04-03"],"award-info":[{"award-number":["StrongSoft - TIN2012-39391-C04-03"]}],"id":[{"id":"10.13039\/501100003339","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100012818","name":"Comunidad de Madrid","doi-asserted-by":"crossref","award":["N-Greens Software - S2013\/ICE-2731"],"award-info":[{"award-number":["N-Greens Software - S2013\/ICE-2731"]}],"id":[{"id":"10.13039\/100012818","id-type":"DOI","asserted-by":"crossref"}]}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Softw Syst Model"],"published-print":{"date-parts":[[2019,2]]},"DOI":"10.1007\/s10270-017-0581-1","type":"journal-article","created":{"date-parts":[[2017,2,13]],"date-time":"2017-02-13T03:00:28Z","timestamp":1486954828000},"page":"71-105","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":3,"title":["Synthesis of verifiable concurrent Java components from formal models"],"prefix":"10.1007","volume":"18","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-2665-7612","authenticated-orcid":false,"given":"Julio","family":"Mari\u00f1o","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0001-7688-1447","authenticated-orcid":false,"given":"Ra\u00fal N. N.","family":"Alborodo","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-8296-4609","authenticated-orcid":false,"given":"Lars-\u00c5ke","family":"Fredlund","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-6433-5681","authenticated-orcid":false,"given":"\u00c1ngel","family":"Herranz","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2017,2,13]]},"reference":[{"issue":"1","key":"581_CR1","doi-asserted-by":"publisher","first-page":"32","DOI":"10.1007\/s10270-004-0058-x","volume":"4","author":"W Ahrendt","year":"2005","unstructured":"Ahrendt, W., Baar, T., Beckert, B., Bubel, R., Giese, M., H\u00e4hnle, R., Menzel, W., Mostowski, W., Roth, A., Schlager, S., Schmitt, H.P.: The key tool. Soft. Syst. Model. 4(1), 32\u201354 (2005). doi: 10.1007\/s10270-004-0058-x","journal-title":"Soft. Syst. Model."},{"key":"581_CR2","unstructured":"Alborodo, R.N.N., Mari\u00f1o, J., \u00c1ngel H.: The shared resources home page. http:\/\/babel.upm.es\/~rnnalborodo\/sr_web\/ (2014)"},{"key":"581_CR3","doi-asserted-by":"publisher","unstructured":"Ara\u00fajo, J.E., Reb\u00ealo, H., Lima, R., Mota, A., Kulesza, U., Sant\u2019Anna, C.: An annotation-based approach for jcsp concurrent programming: a quantitative study. In: Proceedings of the 1st Workshop on Modularity in Systems Software, MISS \u201911, pp. 7\u201311. ACM, New York, NY (2011). doi: 10.1145\/1960518.1960521","DOI":"10.1145\/1960518.1960521"},{"key":"581_CR4","doi-asserted-by":"publisher","first-page":"476","DOI":"10.1007\/11557432_36","volume-title":"Model-Driven Engineering in a Large Industrial Context\u2014Motorola Case Study","author":"P Baker","year":"2005","unstructured":"Baker, P., Loh, S., Weil, F.: Model-Driven Engineering in a Large Industrial Context\u2014Motorola Case Study, pp. 476\u2013491. Springer, Berlin (2005). doi: 10.1007\/11557432_36"},{"key":"581_CR5","doi-asserted-by":"crossref","unstructured":"Ball, T., Cook, B., Levin, V., Rajamani, S., Ball, T.: Slam and static driver verifier: technology transfer of formal methods inside microsoft. Technical Report (2004)","DOI":"10.1007\/978-3-540-24756-2_1"},{"key":"581_CR6","doi-asserted-by":"crossref","unstructured":"Beckert, B., H\u00e4hnle, R., Schmitt, P.H. (eds.): Verification of Object-Oriented Software: The KeY Approach. LNCS 4334. Springer (2007)","DOI":"10.1007\/978-3-540-69061-0"},{"issue":"7","key":"581_CR7","doi-asserted-by":"publisher","first-page":"574","DOI":"10.1145\/361454.361473","volume":"15","author":"P Brinch-Hansen","year":"1972","unstructured":"Brinch-Hansen, P.: Structured multiprogramming. Commun. ACM 15(7), 574\u2013578 (1972). (One of Brinch\u2013Hansen\u2019s seminal works on monitors)","journal-title":"Commun. ACM"},{"issue":"1","key":"581_CR8","doi-asserted-by":"publisher","first-page":"63","DOI":"10.1145\/214037.214100","volume":"27","author":"PA Buhr","year":"1995","unstructured":"Buhr, P.A., Fortier, M., Coffin, M.H.: Monitor classification. ACM Comput. Surv. 27(1), 63\u2013107 (1995). doi: 10.1145\/214037.214100","journal-title":"ACM Comput. Surv."},{"key":"581_CR9","unstructured":"BV, V.S.T.: Dezyne home page. http:\/\/www.verum.com\/ (2015)"},{"issue":"1","key":"581_CR10","doi-asserted-by":"publisher","first-page":"5:1","DOI":"10.1145\/2414446.2414451","volume":"13","author":"M Carro","year":"2013","unstructured":"Carro, M., Herranz, \u00c1ngel, Mari\u00f1o, J.: A model-driven approach to teaching concurrency. Trans. Comput. Educ. 13(1), 5:1\u20135:19 (2013)","journal-title":"Trans. Comput. Educ."},{"key":"581_CR11","unstructured":"Carro, M., Mari\u00f1o, J., \u00c1ngel Herranz, Moreno-Navarro, J.J.: Teaching how to derive correct concurrent programs (from state-based specifications and code patterns). In: Dean, C., Boute, R. (eds.) Teaching Formal Methods, CoLogNET\/FME Symposium, TFM 2004, Ghent, Belgium, LNCS, vol. 3294, pp. 85\u2013106. Springer, NewYork (2004). ISBN 3-540-23611-2"},{"key":"581_CR12","doi-asserted-by":"publisher","unstructured":"Cok, D.R.: Openjml: software verification for Java 7 using JML, openjdk, and eclipse. In: Proceedings 1st Workshop on Formal Integrated Development Environment, F-IDE 2014, Grenoble, France, April 6, 2014, pp. 79\u201392 (2014). doi: 10.4204\/EPTCS.149.8","DOI":"10.4204\/EPTCS.149.8"},{"key":"581_CR13","doi-asserted-by":"crossref","unstructured":"Fredlund, L., Herranz-Nieva, \u00c1., Alborodo, R.N.N., Mari\u00f1o, J.: A testing-based approach to ensure the safety of shared resource concurrent systems (revised version of conference publication). J. Risk Reliab. (2015) (Accepted for publication, to appear in 2016)","DOI":"10.1007\/978-3-319-15201-1_8"},{"key":"581_CR14","unstructured":"Galeotti, J.P., Rosner, N., Lopez\u00a0Pombo, C., Frias, M.: Taco: analysis of invariants for efficient bounded verification. In: Orso, T. (eds.) International Symposium on Software Testing and Analysis. Trento (2010). http:\/\/publicaciones.dc.uba.ar\/Publications\/2010\/GRLF10a"},{"key":"581_CR15","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-25156-1_3","volume-title":"Using Patterns to Map OCL Constraints to JML Specifications","author":"A Hamie","year":"2015","unstructured":"Hamie, A.: Using Patterns to Map OCL Constraints to JML Specifications. Springer, Cham (2015). doi: 10.1007\/978-3-319-25156-1_3"},{"key":"581_CR16","doi-asserted-by":"publisher","unstructured":"Herranz, A., Mari\u00f1o, J.: A verified implementation of priority monitors in Java. In: Proceedings of the 2011 International Conference on Formal Verification of Object-Oriented Software, FoVeOOS\u201911, pp. 160\u2013177. Springer, Berlin (2012). doi: 10.1007\/978-3-642-31762-0_11","DOI":"10.1007\/978-3-642-31762-0_11"},{"key":"581_CR17","doi-asserted-by":"publisher","unstructured":"Herranz, A., Mari\u00f1o, J., Carro, M., Moreno\u00a0Navarro, J.J.: Modeling concurrent systems with shared resources. In: Alpuente, M., Cook, B., Joubert, C. (eds.) Formal Methods for Industrial Critical Systems. Lecture Notes in Computer Science, vol. 5825, pp. 102\u2013116. Springer, Berlin (2009). doi: 10.1007\/978-3-642-04570-7_9","DOI":"10.1007\/978-3-642-04570-7_9"},{"key":"581_CR18","unstructured":"Hilderink, G., Broenink, J., Vervoort, W., Bakkers, A.: Communicating java threads. In: Parallel Programming and Java. Concurrent Systems Engineering Series, vol.\u00a050, pp. 48\u201376. IOS Press, Amsterdam (1997). http:\/\/doc.utwente.nl\/16613\/"},{"issue":"10","key":"581_CR19","doi-asserted-by":"publisher","first-page":"549","DOI":"10.1145\/355620.361161","volume":"17","author":"CAR Hoare","year":"1974","unstructured":"Hoare, C.A.R.: Monitors: an operating system structuring concept. Commun. ACM 17(10), 549\u2013557 (1974). doi: 10.1145\/355620.361161","journal-title":"Commun. ACM"},{"key":"581_CR20","unstructured":"Howard, J.H.: Signaling in monitors. In: Proceedings of the 2nd International Conference on Software Engineering, ICSE \u201976, pp. 47\u201352. IEEE Computer Society Press, Los Alamitos, CA (1976). http:\/\/dl.acm.org\/citation.cfm?id=800253.807647"},{"key":"581_CR21","unstructured":"Klein, J., Levinson, H., Marchetti, J.: Model-driven engineering: automatic code generation and beyond. Technical Report CMU\/SEI-2015-TN-005, Software Engineering Institute, Carnegie Mellon University, Pittsburgh, PA (2015). http:\/\/resources.sei.cmu.edu\/library\/asset-view.cfm?AssetID=435414"},{"key":"581_CR22","doi-asserted-by":"publisher","first-page":"134","DOI":"10.1007\/s100090050010","volume":"1","author":"KG Larsen","year":"1997","unstructured":"Larsen, K.G., Pettersson, P., Yi, W.: Uppaal in a nutshell. STTT 1, 134\u2013152 (1997)","journal-title":"STTT"},{"key":"581_CR23","doi-asserted-by":"publisher","unstructured":"Leavens, G.T., Baker, A.L., Ruby, C.: JML: A notation for detailed design. In: Kilov, H., Rumpe, B., Simmonds, I. (eds.) Behavioral Specifications of Businesses and Systems. The Springer International Series in Engineering and Computer Science, vol. 523, pp. 175\u2013188. Springer, NewYork (1999). doi: 10.1007\/978-1-4615-5229-1_12","DOI":"10.1007\/978-1-4615-5229-1_12"},{"key":"581_CR24","unstructured":"Mari\u00f1o, J., Alborodo, R.N.N.: Communicating Process Architectures, chap. A Model-driven Methodology for Generating and Verifying CSP-based Java Code, pp. 85\u2013108. Open Channel Publishing Ltd., Oxford (2015) (Accepted for publication, to appear in 2016)"},{"key":"581_CR25","doi-asserted-by":"publisher","unstructured":"Pajic, M., Jiang, Z., Lee, I., Sokolsky, O., Mangharam, R.: From verification to implementation: a model translation tool and a pacemaker case study. In: 2012 IEEE 18th Real Time and Embedded Technology and Applications Symposium, Beijing, April 16\u201319, 2012, pp. 173\u2013184 (2012). doi: 10.1109\/RTAS.2012.25","DOI":"10.1109\/RTAS.2012.25"},{"key":"581_CR26","doi-asserted-by":"publisher","unstructured":"Robby, Dwyer, M.B., Hatcliff, J.: Bogor: An extensible and highly-modular software model checking framework. In: Proceedings of the 9th European Software Engineering Conference Held Jointly with 11th ACM SIGSOFT International Symposium on Foundations of Software Engineering, ESEC\/FSE-11, pp. 267\u2013276. ACM, New York, NY (2003). doi: 10.1145\/940071.940107","DOI":"10.1145\/940071.940107"},{"key":"581_CR27","doi-asserted-by":"publisher","unstructured":"Rodr\u00edguez, E., Dwyer, M., Flanagan, C., Hatcliff, J., Leavens, G., Robby: extending JML for modular specification and verification of multi-threaded programs. In: Black, A. (ed.) ECOOP 2005\u2014Object-Oriented Programming, Lecture Notes in Computer Science, vol. 3586, pp. 551\u2013576. Springer, Berlin (2005). doi: 10.1007\/11531142_24","DOI":"10.1007\/11531142_24"},{"key":"581_CR28","unstructured":"Schaller, N.C., Hilderink, G.H., Welch, P.H.: Using Java for parallel computing: JCSP versus CTJ, a comparison. In: Welch, P.H., Bakkers, A.W.P. (eds.) Communicating Process Architectures, pp. 205\u2013226 (2000)"},{"key":"581_CR29","unstructured":"Welch, P.H., Austin, P.D., Brown, N.C.C.: Communicating Sequential Processes for Java (JCSP). http:\/\/www.cs.kent.ac.uk\/projects\/ofa\/JCSP\/ (2012)"}],"container-title":["Software & Systems Modeling"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10270-017-0581-1\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10270-017-0581-1.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10270-017-0581-1.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,9,18]],"date-time":"2019-09-18T12:04:55Z","timestamp":1568808295000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10270-017-0581-1"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017,2,13]]},"references-count":29,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2019,2]]}},"alternative-id":["581"],"URL":"https:\/\/doi.org\/10.1007\/s10270-017-0581-1","relation":{},"ISSN":["1619-1366","1619-1374"],"issn-type":[{"type":"print","value":"1619-1366"},{"type":"electronic","value":"1619-1374"}],"subject":[],"published":{"date-parts":[[2017,2,13]]},"assertion":[{"value":"20 March 2016","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"4 January 2017","order":2,"name":"revised","label":"Revised","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"10 January 2017","order":3,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"13 February 2017","order":4,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}