{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2023,11,7]],"date-time":"2023-11-07T13:09:47Z","timestamp":1699362587906},"reference-count":39,"publisher":"Springer Science and Business Media LLC","issue":"1","license":[{"start":{"date-parts":[[2015,12,19]],"date-time":"2015-12-19T00:00:00Z","timestamp":1450483200000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Innovations Syst Softw Eng"],"published-print":{"date-parts":[[2016,3]]},"DOI":"10.1007\/s11334-015-0269-z","type":"journal-article","created":{"date-parts":[[2015,12,19]],"date-time":"2015-12-19T14:32:45Z","timestamp":1450535565000},"page":"1-26","update-policy":"http:\/\/dx.doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":4,"title":["From verified model to executable program: the PAT approach"],"prefix":"10.1007","volume":"12","author":[{"given":"Huiquan","family":"Zhu","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Jing","family":"Sun","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Jin Song","family":"Dong","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Shang-Wei","family":"Lin","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2015,12,19]]},"reference":[{"key":"269_CR1","volume-title":"Principles of model checking","author":"C Baier","year":"2008","unstructured":"Baier C, Katoen J (2008) Principles of model checking. The MIT Press, Cambridge"},{"key":"269_CR2","unstructured":"Bj\u00f8rndalen JM, Vinter B, Anshus OJ (2007) PyCSP\u2014communicating sequential processes for python. In: McEwan AA, Schneider SA, Ifill W, Welch PH (eds) The 30th communicating process architectures conference (CPA\u201907), pp 229\u2013248"},{"key":"269_CR3","unstructured":"Brown N (2007) C++CSP2: a many-to-many threading model for multicore architectures. In: Communicating process architectures 2007: WoTUG-30, pp 183\u2013205"},{"key":"269_CR4","first-page":"139","volume":"2003","author":"N Brown","year":"2003","unstructured":"Brown N, Welch P (2003) An introduction to the Kent C++ CSP Library. Commun Process Archit 2003:139\u2013156","journal-title":"Commun Process Archit"},{"key":"269_CR5","first-page":"185","volume":"2004","author":"NC Brown","year":"2004","unstructured":"Brown NC (2004) C++ CSP networked. Commun Process Archit 2004:185\u2013200","journal-title":"Commun Process Archit"},{"key":"269_CR6","first-page":"233","volume":"27","author":"I East","year":"2004","unstructured":"East I, Martin J, Welch P, Duce D, Green M (2004) gCSP: a graphical tool for designing CSP systems. Commun Process Archit 2004 27:233","journal-title":"Commun Process Archit 2004"},{"key":"269_CR7","doi-asserted-by":"crossref","unstructured":"Freitas L (2002) JACK: a process algebra implementation in Java. Ph.D. thesis, Centro de Informatica, Universidade Federal de Pernambuco","DOI":"10.5753\/sbes.2002.23941"},{"key":"269_CR8","unstructured":"Gardner W (2000) CSP++: an object-oriented application framework for software synthesis from CSP specifications. Ph.D. thesis, Politecnico di Milano, Italy"},{"key":"269_CR9","doi-asserted-by":"crossref","unstructured":"Gardner W (2003) Bridging CSP and C++ with selective formalism and executable specifications. In: Proceedings of first ACM and IEEE international conference on formal methods and models for co-design (MEMOCODE\u201903). IEEE, pp 237\u2013245","DOI":"10.1109\/MEMCOD.2003.1210108"},{"key":"269_CR10","unstructured":"Gardner W (2005) CSP++: how faithful to CSPm. In: Proc. communicating process architectures 2005 (WoTUG-27), pp 129\u2013146"},{"key":"269_CR11","doi-asserted-by":"crossref","unstructured":"Hilderink G, Bakkers A, Broenink J (2000) A distributed real-time Java system based on CSP. In: Proceedings of third IEEE international symposium on object-oriented real-time distributed computing (ISORC\u201900). IEEE, pp 400\u2013407","DOI":"10.1109\/ISORC.2000.839557"},{"issue":"10","key":"269_CR12","doi-asserted-by":"crossref","first-page":"549","DOI":"10.1145\/355620.361161","volume":"17","author":"C Hoare","year":"1974","unstructured":"Hoare C (1974) Monitors: an operating system structuring concept. Commun ACM 17(10):549\u2013557","journal-title":"Commun ACM"},{"key":"269_CR13","unstructured":"Hoare C (1985) Communicating sequential processes. In: Prentice-Hall international series in computer science. Prentice\/Hall International, London"},{"issue":"5","key":"269_CR14","doi-asserted-by":"crossref","first-page":"273","DOI":"10.1145\/360051.360079","volume":"19","author":"JH Howard","year":"1976","unstructured":"Howard JH (1976) Proving monitors. Commun ACM 19(5):273\u2013279. doi: 10.1145\/360051.360079","journal-title":"Commun ACM"},{"key":"269_CR15","volume-title":"Programming in Occam","author":"G Jones","year":"1986","unstructured":"Jones G (1986) Programming in Occam. Prentice-Hall International, London"},{"key":"269_CR16","unstructured":"Kleine M (2009) Using CSP for software verification. In: Proceedings of formal methods 2009 doctoral symposium. Eindhoven University of Technology, pp 8\u201313"},{"key":"269_CR17","doi-asserted-by":"crossref","unstructured":"Kleine M (2011) CSP as a coordination language. In: Coordination models and languages. Springer, New York, pp 65\u201379","DOI":"10.1007\/978-3-642-21464-6_5"},{"issue":"1","key":"269_CR18","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1007\/s10703-010-0099-4","volume":"37","author":"SJ Lee","year":"2010","unstructured":"Lee SJ, Dobbie G, Sun J, Groves L (2010) Theorem prover approach to semistructured data design. Form Methods Syst Des 37(1):1\u201360. doi: 10.1007\/s10703-010-0099-4","journal-title":"Form Methods Syst Des"},{"key":"269_CR19","first-page":"13","volume":"2006","author":"A Lehmberg","year":"2006","unstructured":"Lehmberg A, Olsen M (2006) An introduction to CSP.NET. Commun Process Archit 2006:13\u201330","journal-title":"Commun Process Archit"},{"issue":"2","key":"269_CR20","doi-asserted-by":"crossref","first-page":"176","DOI":"10.1007\/s10703-013-0197-1","volume":"44","author":"Y Li","year":"2014","unstructured":"Li Y, Dong JS, Sun J, Liu Y, Sun J (2014) Model checking approach to automated planning. Form Methods in Syst Des 44(2):176\u2013202. doi: 10.1007\/s10703-013-0197-1","journal-title":"Form Methods in Syst Des"},{"key":"269_CR21","unstructured":"Liang H, Dong JS, Sun J (2007) Evolution and runtime monitoring of software systems. In: SEKE\u201907: Proceedings of the 19th international conference on software engineering and knowledge engineering. Knowledge Systems Institute Graduate School, Skokie, pp 343\u2013348"},{"key":"269_CR22","doi-asserted-by":"crossref","unstructured":"Liang H, Dong JS, Sun J, Duke R, Seviora RE (2006) Formal specification-based online monitoring. In: ICECCS\u201906: proceedings of the 11th IEEE international conference on engineering of complex computer systems. IEEE Computer Society, Washington, DC, pp 152\u2013160. doi: 10.1109\/ICECCS.2006.1690364","DOI":"10.1109\/ICECCS.2006.1690364"},{"key":"269_CR23","doi-asserted-by":"crossref","unstructured":"Lin SW, Liu Y, Hsiung PA, Sun J, Dong JS (2012) Automatic generation of provably correct embedded systems. In: Formal methods and software engineering. Springer, New York, pp 214\u2013229","DOI":"10.1007\/978-3-642-34281-3_17"},{"key":"269_CR24","doi-asserted-by":"crossref","unstructured":"Liu Y, Sun J, Dong JS (2011) PAT 3: an extensible architecture for building multi-domain model checkers. In: ISSRE, pp 190\u2013199","DOI":"10.1109\/ISSRE.2011.19"},{"key":"269_CR25","doi-asserted-by":"crossref","unstructured":"Mahony B, Dong JS (1998) Blending object-Z and timed CSP: an introduction to TCOZ. In: Proceedings of the 20th international conference on software engineering (ICSE\u201998). IEEE Computer Society, pp 95\u2013104","DOI":"10.1109\/ICSE.1998.671106"},{"key":"269_CR26","unstructured":"Schaller N, Hilderink G, Welch P (2000) Using Java for parallel computing: JCSP versus CTJ, a comparison. In: Communicating process architectures, pp 205\u2013226"},{"key":"269_CR27","volume-title":"Programming in Go: creating applications for the 21st century","author":"M Summerfield","year":"2012","unstructured":"Summerfield M (2012) Programming in Go: creating applications for the 21st century. Addison-Wesley Professional, Menlo Park"},{"key":"269_CR28","doi-asserted-by":"crossref","unstructured":"Sun J, Dong JS, Jarzabek S, Wang H (2006) Computer-aided dispatch system family architecture and verification: an integrated formal approach. IEE Proc Softw 153(3):102\u2013112. doi: 10.1049\/ip-sen:20050014","DOI":"10.1049\/ip-sen:20050014"},{"key":"269_CR29","doi-asserted-by":"crossref","unstructured":"Sun J, Liu Y, Dong JS, Chen C (2009) Integrating specification and programs for system modeling and verification. In: Proceedings of the third IEEE international symposium on theoretical aspects of software engineering (TASE\u201909), pp 127\u2013135","DOI":"10.1109\/TASE.2009.32"},{"key":"269_CR30","doi-asserted-by":"crossref","unstructured":"Sun J, Liu Y, Dong JS, Liu Y, Shi L (2013) \u00c9tienne Andr\u00e9: modeling and verifying hierarchical real-time systems using stateful timed CSP. ACM Trans Softw Eng Methodol 22(1):3:1\u20133:29. doi: 10.1145\/2430536.2430537","DOI":"10.1145\/2430536.2430537"},{"key":"269_CR31","doi-asserted-by":"crossref","unstructured":"Sun J, Liu Y, Dong JS, Pang J (2009) PAT: towards flexible verification under fairness. In: Proceedings of the 21th international conference on computer aided verification (CAV\u201909). Lecture notes in computer science, vol 5643. Springer, New York, pp 709\u2013714","DOI":"10.1007\/978-3-642-02658-4_59"},{"issue":"4","key":"269_CR32","doi-asserted-by":"crossref","first-page":"368","DOI":"10.1007\/s11704-008-0035-6","volume":"2","author":"J Sun","year":"2008","unstructured":"Sun J, Liu Y, Dong JS, Sun J (2008) Compositional encoding for bounded model checking. Front Comput Sci China 2(4):368\u2013379. doi: 10.1007\/s11704-008-0035-6","journal-title":"Front Comput Sci China"},{"issue":"65","key":"269_CR33","first-page":"349","volume":"2007","author":"P Welch","year":"2007","unstructured":"Welch P, Brown N, Moores J, Chalmers K, Sputh B (2007) Integrating and extending JCSP. Commun Process Archit 2007(65):349\u2013370","journal-title":"Commun Process Archit"},{"key":"269_CR34","doi-asserted-by":"crossref","unstructured":"Welch P, Martin J (2000) A CSP model for Java multithreading. In: Proceedings of international symposium on software engineering for parallel and distributed systems, pp 114\u2013122","DOI":"10.1109\/PDSE.2000.847856"},{"key":"269_CR35","first-page":"275","volume":"58","author":"P Welch","year":"2000","unstructured":"Welch P, Martin J (2000) Formal analysis of concurrent java systems. Commun Process Archit 58:275\u2013301","journal-title":"Commun Process Archit"},{"key":"269_CR36","first-page":"67","volume":"65","author":"L Yang","year":"2007","unstructured":"Yang L, Poppleton M (2007) JCSProB: implementing integrated formal specifications in concurrent Java. Commun Process Archit 65:67\u201388","journal-title":"Commun Process Archit"},{"issue":"8","key":"269_CR37","doi-asserted-by":"crossref","first-page":"1007","DOI":"10.1002\/cpe.1425","volume":"22","author":"L Yang","year":"2010","unstructured":"Yang L, Poppleton M (2010) Java implementation platform for the integrated state-and event-based specification in PROB. Concurr Comput Pract Exp 22(8):1007\u20131022","journal-title":"Concurr Comput Pract Exp"},{"key":"269_CR38","doi-asserted-by":"crossref","unstructured":"Yuan L, Dong JS, Sun J, Basit HA (2006) Generic fault tolerant software architecture reasoning and customization. IEEE Trans Reliab 55(3):421\u2013435. doi: 10.1109\/TR.2006.879605","DOI":"10.1109\/TR.2006.879605"},{"key":"269_CR39","doi-asserted-by":"crossref","unstructured":"Zhang J, Liu Y, Sun J, Dong JS, Sun J (2012) Model checking software architecture design. In: 2012 IEEE 14th international symposium on high-assurance systems engineering (HASE), pp 193\u2013200. doi: 10.1109\/HASE.2012.12","DOI":"10.1109\/HASE.2012.12"}],"container-title":["Innovations in Systems and Software Engineering"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s11334-015-0269-z.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s11334-015-0269-z\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s11334-015-0269-z","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,8,16]],"date-time":"2023-08-16T06:46:26Z","timestamp":1692168386000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s11334-015-0269-z"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015,12,19]]},"references-count":39,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2016,3]]}},"alternative-id":["269"],"URL":"https:\/\/doi.org\/10.1007\/s11334-015-0269-z","relation":{},"ISSN":["1614-5046","1614-5054"],"issn-type":[{"value":"1614-5046","type":"print"},{"value":"1614-5054","type":"electronic"}],"subject":[],"published":{"date-parts":[[2015,12,19]]}}}