{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,27]],"date-time":"2025-10-27T20:34:04Z","timestamp":1761597244097,"version":"3.38.0"},"reference-count":70,"publisher":"Springer Science and Business Media LLC","issue":"2","license":[{"start":{"date-parts":[[2010,12,24]],"date-time":"2010-12-24T00:00:00Z","timestamp":1293148800000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Form Methods Syst Des"],"published-print":{"date-parts":[[2011,4]]},"DOI":"10.1007\/s10703-010-0110-0","type":"journal-article","created":{"date-parts":[[2010,12,23]],"date-time":"2010-12-23T14:55:17Z","timestamp":1293116117000},"page":"119-157","source":"Crossref","is-referenced-by-count":5,"title":["A WSDL-based type system for asynchronous WS-BPEL processes"],"prefix":"10.1007","volume":"38","author":[{"given":"A.","family":"Lapadula","sequence":"first","affiliation":[]},{"given":"R.","family":"Pugliese","sequence":"additional","affiliation":[]},{"given":"F.","family":"Tiezzi","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2010,12,24]]},"reference":[{"issue":"3","key":"110_CR1","doi-asserted-by":"crossref","first-page":"131","DOI":"10.1016\/j.infsof.2006.11.004","volume":"50","author":"WMP Aalst van\u00a0der","year":"2008","unstructured":"van\u00a0der Aalst WMP, Lassen KB (2008) Translating unstructured workflow processes to readable BPEL: Theory and implementation. Inf Softw Technol 50(3):131\u2013159","journal-title":"Inf Softw Technol"},{"key":"110_CR2","series-title":"LNCS","first-page":"372","volume-title":"CONCUR","author":"L Acciai","year":"2008","unstructured":"Acciai L, Boreale M (2008) Spatial and behavioral types in the pi-calculus. In: CONCUR. LNCS, vol\u00a05201. Springer, Berlin, pp\u00a0372\u2013386"},{"key":"110_CR3","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"642","DOI":"10.1007\/978-3-540-68679-8_40","volume-title":"Concurrency, graphs and models","author":"L Acciai","year":"2008","unstructured":"Acciai L, Boreale M (2008) A type system for client progress in a service-oriented calculus. In: Concurrency, graphs and models. LNCS, vol 5065. Springer, Berlin, pp\u00a0642\u2013658"},{"issue":"2","key":"110_CR4","doi-asserted-by":"crossref","first-page":"291","DOI":"10.1016\/S0304-3975(97)00223-5","volume":"195","author":"R Amadio","year":"1998","unstructured":"Amadio R, Castellani I, Sangiorgi D (1998) On bisimulations for the asynchronous pi-calculus. Theor Comput Sci 195(2):291\u2013324","journal-title":"Theor Comput Sci"},{"key":"110_CR5","unstructured":"Arkin A, Askary S, Fordin S, Jekeli W, Kawaguchi K, Orchard D, Pogliani S, Riemer D, Struble S, Takacsi-Nagy P, Trickovic I, Zimek S (2002) Web service choreography interface (WSCI) 1.0. Tech rep, W3C. Available at http:\/\/www.w3.org\/TR\/wsci\/"},{"key":"110_CR6","unstructured":"Banerji A, Bartolini C, Beringer D, Chopella V, Govindarajan K, Karp A, Kuno H, Lemon M, Pogossiants G, Sharma S, Williams S (2002) Web services conversation language (WSCL) 1.0. Tech rep, W3C Note. Available at http:\/\/www.w3.org\/TR\/2002\/NOTE-wscl10-20020314"},{"key":"110_CR7","unstructured":"Battle S, Bernstein A, Boley H, Grosof B, Gruninger M, Hull R, Kifer M, Martin D, McIlraith S, McGuinness D, Su J, Tabet S (2005) Semantic web services framework (SWSF) 1.0. Tech rep, SWSL Committee. Available at http:\/\/www.daml.org\/services\/swsf\/1.0\/"},{"key":"110_CR8","series-title":"LNCS","first-page":"418","volume-title":"CONCUR","author":"L Bettini","year":"2008","unstructured":"Bettini L, Coppo M, D\u2019Antoni L, De Luca M, Dezani-Ciancaglini M, Yoshida N (2008) Global progress in dynamically interleaved multiparty sessions. In: CONCUR. LNCS, vol 5201. Springer, Berlin, pp\u00a0418\u2013433"},{"key":"110_CR9","unstructured":"Boag S, Chamberlin D, Fern\u00e1ndez M, Florescu D, Robie J, Sim\u00e9on J (2007) Xquery 1.0: an XML query language. Tech rep, W3C. Available at http:\/\/www.w3.org\/TR\/xquery\/"},{"key":"110_CR10","series-title":"LNCS","first-page":"124","volume-title":"FMOODS","author":"L Bocchi","year":"2003","unstructured":"Bocchi L, Laneve C, Zavattaro G (2003) A calculus for long-running transactions. In: FMOODS. LNCS, vol 2884. Springer, Berlin, pp\u00a0124\u2013138"},{"key":"110_CR11","series-title":"LNCS","first-page":"240","volume-title":"TGC","author":"E Bonelli","year":"2007","unstructured":"Bonelli E, Compagnoni AB (2007) Multipoint session types for a distributed calculus. In: TGC. LNCS, vol 4912. Springer, Berlin, pp\u00a0240\u2013256"},{"key":"110_CR12","series-title":"LNCS","first-page":"19","volume-title":"FMOODS","author":"M Boreale","year":"2008","unstructured":"Boreale M, Bruni R, De Nicola R, Loreti M (2008) Sessions and pipelines for structured service programming. In: FMOODS. LNCS, vol 5051. Springer, Berlin, pp\u00a019\u201338"},{"key":"110_CR13","unstructured":"van Breugel F, Koshkina M (2006) Models and verification of BPEL. Tech rep, Department of Computer Science and Engineering, York University. Available at http:\/\/www.cse.yorku.ca\/~franck\/research\/drafts\/tutorial.pdf"},{"key":"110_CR14","series-title":"LNCS","first-page":"383","volume-title":"CONCUR","author":"R Bruni","year":"2005","unstructured":"Bruni R, Butler M, Ferreira C, Hoare C, Melgratti H, Montanari U (2005) Comparing two approaches to compensable flow composition. In: CONCUR. LNCS, vol 3653. Springer, Berlin, pp\u00a0383\u2013397"},{"key":"110_CR15","doi-asserted-by":"crossref","first-page":"209","DOI":"10.1145\/1040305.1040323","volume-title":"POPL","author":"R Bruni","year":"2005","unstructured":"Bruni R, Melgratti H, Montanari U (2005) Theoretical foundations for compensations in flow composition languages. In: POPL. ACM, New York, pp\u00a0209\u2013220"},{"key":"110_CR16","series-title":"LNCS","first-page":"228","volume-title":"ICSOC","author":"N Busi","year":"2005","unstructured":"Busi N, Gorrieri R, Guidi C, Lucchi R, Zavattaro G (2005) Choreography and orchestration: a synergic approach for system design. In: ICSOC. LNCS, vol 3826. Springer, Berlin, pp\u00a0228\u2013240"},{"key":"110_CR17","series-title":"LNCS","first-page":"87","volume-title":"COORDINATION","author":"M Butler","year":"2004","unstructured":"Butler M, Ferreira C (2004) An operational semantics for StAC, a language for modelling long-running business transactions. In: COORDINATION. LNCS, vol 2949. Springer, Berlin, pp\u00a087\u2013104"},{"key":"110_CR18","series-title":"LNCS","first-page":"285","volume-title":"ESOP","author":"L Caires","year":"2009","unstructured":"Caires L, Vieira H (2009) Conversation types. In: ESOP. LNCS, vol 5502. Springer, Berlin, pp\u00a0285\u2013300"},{"key":"110_CR19","series-title":"ENTCS","first-page":"127","volume-title":"DCM","author":"M Carbone","year":"2007","unstructured":"Carbone M, Honda K, Yoshida N (2007) A calculus of global interaction based on session types. In: DCM. ENTCS, vol 171. Elsevier, Amsterdam, pp\u00a0127\u2013151"},{"key":"110_CR20","series-title":"LNCS","first-page":"2","volume-title":"ESOP","author":"M Carbone","year":"2007","unstructured":"Carbone M, Honda K, Yoshida N (2007) Structured communication-centred programming for web services. In: ESOP. LNCS, vol 4421. Springer, Berlin, pp\u00a02\u201317"},{"key":"110_CR21","series-title":"LNCS","first-page":"197","volume-title":"ESOP","author":"S Carpineti","year":"2006","unstructured":"Carpineti S, Laneve C (2006) A basic contract language for web services. In: ESOP. LNCS, vol 3924. Springer, Berlin, pp\u00a0197\u2013213"},{"issue":"10","key":"110_CR22","doi-asserted-by":"crossref","first-page":"777","DOI":"10.1016\/j.scico.2009.03.002","volume":"74","author":"S Carpineti","year":"2009","unstructured":"Carpineti S, Laneve C, Padovani L (2009) PiDuce\u2014a project for experimenting Web services technologies. Sci Comput Program 74(10):777\u2013811","journal-title":"Sci Comput Program"},{"key":"110_CR23","doi-asserted-by":"crossref","first-page":"5","DOI":"10.1145\/1538917.1538920","volume":"31","author":"G Castagna","year":"2009","unstructured":"Castagna G, Gesbert N, Padovani L (2009) A theory of contracts for Web services. ACM Trans Program Lang Syst 31:5","journal-title":"ACM Trans Program Lang Syst"},{"key":"110_CR24","doi-asserted-by":"crossref","first-page":"45","DOI":"10.1145\/503272.503278","volume-title":"POPL","author":"S Chaki","year":"2002","unstructured":"Chaki S, Rajamani SK, Rehof J (2002) Types as models: model checking message-passing programs. In: POPL. ACM, New York, pp\u00a045\u201357"},{"key":"110_CR25","unstructured":"Christensen E, Curbera F, Meredith G, Weerawarana S (2001) Web services description language (WSDL) 1.1. Tech rep, W3C. Available at http:\/\/www.w3.org\/TR\/wsdl\/"},{"key":"110_CR26","unstructured":"Clark J, DeRose S (1999) XML path language (XPath) Version 1.0. Tech rep, W3C. Available at http:\/\/www.w3.org\/TR\/xpath\/"},{"key":"110_CR27","series-title":"LNCS","first-page":"82","volume-title":"COORDINATION","author":"W Cook","year":"2006","unstructured":"Cook W, Patwardhan S, Misra J (2006) Workflow patterns in ORC. In: COORDINATION. LNCS, vol\u00a04038. Springer, Berlin, pp\u00a082\u201396"},{"key":"110_CR28","series-title":"LNCS","first-page":"92","volume-title":"WS-FM","author":"N Dragoni","year":"2010","unstructured":"Dragoni N, Mazzara M (2010) A formal semantics for the WS-BPEL recovery framework: the pi-calculus way. In: WS-FM. LNCS, vol 6194. Springer, Berlin, pp\u00a092\u2013109"},{"key":"110_CR29","volume-title":"SOA design patterns","author":"T Erl","year":"2009","unstructured":"Erl T (2009) SOA design patterns. Prentice Hall, New York"},{"key":"110_CR30","doi-asserted-by":"crossref","first-page":"771","DOI":"10.1145\/1134285.1134408","volume-title":"ICSE","author":"H Foster","year":"2006","unstructured":"Foster H, Uchitel S, Magee J, Kramer J (2006) LTSA-WS: a tool for model-based verification of web service compositions and choreography. In: ICSE. ACM, New York, pp\u00a0771\u2013774"},{"issue":"12","key":"110_CR31","doi-asserted-by":"crossref","first-page":"1042","DOI":"10.1109\/TSE.2005.141","volume":"31","author":"X Fu","year":"2005","unstructured":"Fu X, Bultan T, Su J (2005) Synchronizability of conversations among web services. IEEE Trans Softw Eng 31(12):1042\u20131055","journal-title":"IEEE Trans Softw Eng"},{"issue":"1","key":"110_CR32","doi-asserted-by":"crossref","first-page":"19","DOI":"10.1017\/S0956796809990268","volume":"20","author":"S Gay","year":"2010","unstructured":"Gay S, Vasconcelos V (2010) Linear type theory for asynchronous session types. J Funct Program 20(1):19\u201350","journal-title":"J Funct Program"},{"key":"110_CR33","series-title":"LNCS","first-page":"350","volume-title":"FM","author":"P Geguang","year":"2005","unstructured":"Geguang P, Xiangpeng Z, Shuling W, Zongyan Q (2005) Semantics of BPEL4WS-like fault and compensation handling. In: FM. LNCS, vol 3582. Springer, Berlin, pp\u00a0350\u2013365"},{"key":"110_CR34","series-title":"LNCS","first-page":"251","volume-title":"FMOODS","author":"P Geguang","year":"2006","unstructured":"Geguang P, Huibiao Z, Zongyan Q, Shuling W, Xiangpeng Z, Jifeng H (2006) Theoretical foundations of scope-based compensable flow language for web service. In: FMOODS. LNCS, vol 4037. Springer, Berlin, pp\u00a0251\u2013266"},{"key":"110_CR35","series-title":"ENTCS","first-page":"33","volume-title":"DCM","author":"P Geguang","year":"2006","unstructured":"Geguang P, Xiangpeng Z, Shuling W, Zongyan Q (2006) Towards the semantics and verification of BPEL4WS. In: DCM. ENTCS, vol 151. Elsevier, Amsterdam, pp\u00a033\u201352"},{"key":"110_CR36","unstructured":"Gudgin M, Hadley M, Rogers T (2006) Web services addressing 1.0\u2014Core. Tech rep, W3C. Available at http:\/\/www.w3.org\/TR\/ws-addr-core"},{"key":"110_CR37","series-title":"LNCS","first-page":"327","volume-title":"ICSOC","author":"C Guidi","year":"2006","unstructured":"Guidi C, Lucchi R, Gorrieri R, Busi N, Zavattaro G (2006) SOCK: a calculus for service oriented computing. In: ICSOC. LNCS, vol 4294. Springer, Berlin, pp\u00a0327\u2013338"},{"key":"110_CR38","first-page":"190","volume-title":"ACSD","author":"C Guidi","year":"2008","unstructured":"Guidi C, Lanese I, Montesi F, Zavattaro G (2008) On the interplay between fault handling and request-response service invocations. In: ACSD. IEEE, New York, pp\u00a0190\u2013198"},{"key":"110_CR39","series-title":"LNCS","first-page":"220","volume-title":"BPM","author":"S Hinz","year":"2005","unstructured":"Hinz S, Schmidt K, Stahl C (2005) Transforming BPEL to Petri nets. In: BPM. LNCS, vol 3649. Springer, Berlin, pp\u00a0220\u2013235"},{"key":"110_CR40","series-title":"LNCS","first-page":"122","volume-title":"ESOP","author":"K Honda","year":"1998","unstructured":"Honda K, Vasconcelos VT, Kubo M (1998) Language primitives and type discipline for structured communication-based programming. In: ESOP. LNCS, vol 1381. Springer, Berlin, pp\u00a0122\u2013138"},{"key":"110_CR41","doi-asserted-by":"crossref","first-page":"273","DOI":"10.1145\/1328438.1328472","volume-title":"POPL","author":"K Honda","year":"2008","unstructured":"Honda K, Yoshida N, Carbone M (2008) Multiparty asynchronous session types. In: POPL. ACM, New York, pp\u00a0273\u2013284"},{"issue":"1\u20133","key":"110_CR42","doi-asserted-by":"crossref","first-page":"121","DOI":"10.1016\/S0304-3975(03)00325-6","volume":"311","author":"A Igarashi","year":"2004","unstructured":"Igarashi A, Kobayashi N (2004) A generic type system for the pi-calculus. Theor Comput Sci 311(1\u20133):121\u2013163","journal-title":"Theor Comput Sci"},{"key":"110_CR43","first-page":"83","volume-title":"ICWS","author":"R Kazhamiakin","year":"2006","unstructured":"Kazhamiakin R, Pistore M (2006) Static verification of control and data inWeb service compositions. In: ICWS. IEEE, New York, pp\u00a083\u201390"},{"key":"110_CR44","series-title":"LNCS","first-page":"477","volume-title":"CONCUR","author":"D Kitchin","year":"2006","unstructured":"Kitchin D, Cook W, Misra J (2006) A language for task orchestration and its semantic properties. In: CONCUR. LNCS, vol 4137. Springer, Berlin, pp\u00a0477\u2013491"},{"key":"110_CR45","series-title":"LNCS","first-page":"439","volume-title":"UNU\/IIST","author":"N Kobayashi","year":"2003","unstructured":"Kobayashi N (2003) Type systems for concurrent programs. In: UNU\/IIST. LNCS, vol 2757. Springer, Berlin, pp\u00a0439\u2013453"},{"key":"110_CR46","series-title":"LNCS","first-page":"298","volume-title":"VMCAI","author":"N Kobayashi","year":"2006","unstructured":"Kobayashi N, Suenaga K, Wischik L (2006) Resource usage analysis for the \u03c0-calculus. In: VMCAI. LNCS, vol 3855. Springer, Berlin, pp\u00a0298\u2013312"},{"key":"110_CR47","unstructured":"Kobayashi N (2008) Typical: type-based static analyzer for the picalculus. Tool available at http:\/\/www.kb.ecei.tohoku.ac.jp\/koba\/typical"},{"issue":"5","key":"110_CR48","first-page":"35","volume":"23","author":"M Kov\u00e1cs","year":"2008","unstructured":"Kov\u00e1cs M, G\u00f6nczy L, Varr\u00f3 D (2008) Formal analysis of BPEL workflows with compensation by model checking. J Comput Syst Sci Eng 23(5):35\u201349","journal-title":"J Comput Syst Sci Eng"},{"key":"110_CR49","first-page":"305","volume-title":"SEFM","author":"I Lanese","year":"2007","unstructured":"Lanese I, Martins F, Ravara A, Vasconcelos V (2007) Disciplining orchestration and conversation in service-oriented computing. In: SEFM. IEEE, New York, pp\u00a0305\u2013314"},{"key":"110_CR50","series-title":"LNCS","first-page":"282","volume-title":"FoSSaCS","author":"C Laneve","year":"2005","unstructured":"Laneve C, Zavattaro G (2005) Foundations of web transactions. In: FoSSaCS. LNCS, vol 3441. Springer, Berlin, pp\u00a0282\u2013298"},{"key":"110_CR51","series-title":"LNCS","first-page":"182","volume-title":"TGC","author":"C Laneve","year":"2005","unstructured":"Laneve C, Zavattaro G (2005) Web-pi at work. In: TGC. LNCS, vol 3705. Springer, Berlin, pp\u00a0182\u2013194"},{"key":"110_CR52","series-title":"LNCS","first-page":"145","volume-title":"COORDINATION","author":"A Lapadula","year":"2006","unstructured":"Lapadula A, Pugliese R, Tiezzi F (2006) A WSDL-based type system for WS-BPEL. In: COORDINATION. LNCS, vol 4038. Springer, Berlin, pp\u00a0145\u2013163"},{"key":"110_CR53","series-title":"LNCS","first-page":"33","volume-title":"ESOP","author":"A Lapadula","year":"2007","unstructured":"Lapadula A, Pugliese R, Tiezzi F (2007) A calculus for orchestration of web services. In: ESOP. LNCS, vol 4421. Springer, Berlin, pp\u00a033\u201347"},{"key":"110_CR54","series-title":"LNCS","first-page":"275","volume-title":"ICTAC","author":"A Lapadula","year":"2007","unstructured":"Lapadula A, Pugliese R, Tiezzi F (2007) C WS: a timed service-oriented calculus. In: ICTAC. LNCS, vol 4711. Springer, Berlin, pp\u00a0275\u2013290"},{"key":"110_CR55","series-title":"LNCS","first-page":"199","volume-title":"COORDINATION","author":"A Lapadula","year":"2008","unstructured":"Lapadula A, Pugliese R, Tiezzi F (2008) A formal account of WS-BPEL. In: COORDINATION. LNCS, vol 5052. Springer, Berlin, pp\u00a0199\u2013215"},{"key":"110_CR56","unstructured":"Leymann F (2001) Web services flow language (WSFL 1.0). Tech rep, IBM. Available at http:\/\/xml.coverpages.org\/wsfl.html"},{"key":"110_CR57","series-title":"LNCS","first-page":"77","volume-title":"WSFM","author":"N Lohmann","year":"2008","unstructured":"Lohmann N (2008) A feature-complete Petri net semantics for WS-BPEL 2.0. In: WSFM. LNCS, vol\u00a04937. Springer, Berlin, pp\u00a077\u201391"},{"issue":"1","key":"110_CR58","doi-asserted-by":"crossref","first-page":"96","DOI":"10.1016\/j.jlap.2006.05.007","volume":"70","author":"M Mazzara","year":"2007","unstructured":"Mazzara M, Lucchi R (2007) A pi-calculus based semantics for WS-BPEL. J Log Algebr Program 70(1):96\u2013118","journal-title":"J Log Algebr Program"},{"issue":"10","key":"110_CR59","doi-asserted-by":"crossref","first-page":"41","DOI":"10.1145\/944217.944236","volume":"46","author":"L Meredith","year":"2003","unstructured":"Meredith L, Bjorg S (2003) Contracts and types. Commun ACM 46(10):41\u201347","journal-title":"Commun ACM"},{"key":"110_CR60","unstructured":"Mezzina LG (2008) Typses: a tool for type checking session types. Tool available at http:\/\/www.di.unipi.it\/mezzina"},{"key":"110_CR61","unstructured":"OASIS WSBPEL TC (2007) Web services business process execution language version 2.0. Tech rep, OASIS. Available at http:\/\/docs.oasis-open.org\/wsbpel\/2.0\/OS\/"},{"key":"110_CR62","unstructured":"Object Management Group (1996) The common object request broker: architecture and specification (CORBA 2.0). Tech rep, OMG. Available at http:\/\/www.corba.org\/"},{"key":"110_CR63","first-page":"285","volume-title":"ICWS","author":"C Ouyang","year":"2006","unstructured":"Ouyang C, Dumas M, ter Hofstede AHM, van\u00a0der Aalst WMP (2006) From BPMN process models to BPEL web services. In: ICWS. IEEE, New York, pp\u00a0285\u2013292"},{"issue":"2\u20133","key":"110_CR64","doi-asserted-by":"crossref","first-page":"162","DOI":"10.1016\/j.scico.2007.03.002","volume":"67","author":"C Ouyang","year":"2007","unstructured":"Ouyang C, Verbeek E, van\u00a0der Aalst W, Breutel S, Dumas M, ter Hofstede A (2007) Formal semantics and analysis of control flow in WS-BPEL. Sci Comput Program 67(2\u20133):162\u2013198","journal-title":"Sci Comput Program"},{"key":"110_CR65","series-title":"LNCS","first-page":"465","volume-title":"ICATPN","author":"K Schmidt","year":"2000","unstructured":"Schmidt K (2000) LoLA\u2014a low level analyser. In: ICATPN. LNCS, vol 1825. Springer, Berlin, pp\u00a0465\u2013474"},{"key":"110_CR66","unstructured":"Thatte S (2001) Xlang: Web services for business process design. Tech rep, Microsoft. Available at http:\/\/xml.coverpages.org\/xlang.html"},{"key":"110_CR67","series-title":"ENTCS","first-page":"51","volume-title":"WSFM","author":"M Viroli","year":"2004","unstructured":"Viroli M (2004) Towards a formal foundational to orchestration languages. In: WSFM. ENTCS, vol 105. Elsevier, Amsterdam, pp\u00a051\u201371"},{"issue":"1","key":"110_CR68","doi-asserted-by":"crossref","first-page":"38","DOI":"10.1006\/inco.1994.1093","volume":"115","author":"A Wright","year":"1994","unstructured":"Wright A, Felleisen M (1994) A syntactic approach to type soundness. Inf Comput 115(1):38\u201394","journal-title":"Inf Comput"},{"key":"110_CR69","unstructured":"XMethods (2010). http:\/\/www.xmethods.com"},{"key":"110_CR70","series-title":"ENTCS","first-page":"73","volume-title":"SecReT","author":"N Yoshida","year":"2007","unstructured":"Yoshida N, Vasconcelos VT (2007) Language primitives and type discipline for structured communication-based programming revisited: two systems for higher-order session communication. In: SecReT. ENTCS, vol 171\/4. Elsevier, Amsterdam, pp\u00a073\u201393"}],"container-title":["Formal Methods in System Design"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-010-0110-0.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10703-010-0110-0\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-010-0110-0","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,3,1]],"date-time":"2025-03-01T02:40:12Z","timestamp":1740796812000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10703-010-0110-0"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2010,12,24]]},"references-count":70,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2011,4]]}},"alternative-id":["110"],"URL":"https:\/\/doi.org\/10.1007\/s10703-010-0110-0","relation":{},"ISSN":["0925-9856","1572-8102"],"issn-type":[{"type":"print","value":"0925-9856"},{"type":"electronic","value":"1572-8102"}],"subject":[],"published":{"date-parts":[[2010,12,24]]}}}