{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,4,10]],"date-time":"2025-04-10T04:19:07Z","timestamp":1744258747280,"version":"3.40.4"},"publisher-location":"Berlin, Heidelberg","reference-count":25,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642340314"},{"type":"electronic","value":"9783642340321"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2012]]},"DOI":"10.1007\/978-3-642-34032-1_29","type":"book-chapter","created":{"date-parts":[[2012,9,26]],"date-time":"2012-09-26T00:44:41Z","timestamp":1348620281000},"page":"308-322","source":"Crossref","is-referenced-by-count":3,"title":["Checking Correctness of Services Modeled as Priced Timed Automata"],"prefix":"10.1007","author":[{"given":"Aida","family":"\u010cau\u0161evi\u0107","sequence":"first","affiliation":[]},{"given":"Cristina","family":"Seceleanu","sequence":"additional","affiliation":[]},{"given":"Paul","family":"Pettersson","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"issue":"2","key":"29_CR1","doi-asserted-by":"publisher","first-page":"183","DOI":"10.1016\/0304-3975(94)90010-8","volume":"126","author":"R. Alur","year":"1994","unstructured":"Alur, R., Dill, D.L.: A theory of timed automata. Theoretical Computer Science\u00a0126(2), 183\u2013235 (1994), citeseer.nj.nec.com\/alur94theory.html","journal-title":"Theoretical Computer Science"},{"key":"29_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"49","DOI":"10.1007\/3-540-45351-2_8","volume-title":"Hybrid Systems: Computation and Control","author":"R. Alur","year":"2001","unstructured":"Alur, R., La Torre, S., Pappas, G.J.: Optimal Paths in Weighted Timed Automata. In: Di Benedetto, M.D., Sangiovanni-Vincentelli, A.L. (eds.) HSCC 2001. LNCS, vol.\u00a02034, pp. 49\u201362. Springer, Heidelberg (2001)"},{"key":"29_CR3","unstructured":"Andrews, T., Curbera, F., Dholakia, H., Goland, Y., Klein, J., Leymann, F., Liu, K., Roller, D., Smith, D., Thatte, S., Trickovic, I., Weerawarana, S.: BPEL4WS, Business Process Execution Language for Web Services Version 1.1. IBM (2003)"},{"key":"29_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"147","DOI":"10.1007\/3-540-45351-2_15","volume-title":"Hybrid Systems: Computation and Control","author":"G. Behrmann","year":"2001","unstructured":"Behrmann, G., Fehnker, A., Hune, T., Larsen, K.G., Pettersson, P., Romijn, J., Vaandrager, F.: Minimum-Cost Reachability for Priced Timed Automata. In: Di Benedetto, M.D., Sangiovanni-Vincentelli, A. (eds.) HSCC 2001. LNCS, vol.\u00a02034, pp. 147\u2013161. Springer, Heidelberg (2001)"},{"key":"29_CR5","unstructured":"Causevic, A., Seceleanu, C., Pettersson, P.: Formal reasoning of resource-aware services. Technical Report ISSN 1404-3041 ISRN MDH-MRTC-245\/2010-1-SE, M\u00e4lardalen University (June 2010)"},{"key":"29_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"82","DOI":"10.1007\/978-3-642-16561-0_14","volume-title":"Leveraging Applications of Formal Methods, Verification, and Validation","author":"A. \u010cau\u0161evi\u0107","year":"2010","unstructured":"\u010cau\u0161evi\u0107, A., Seceleanu, C., Pettersson, P.: Modeling and Reasoning about Service Behaviors and Their Compositions. In: Margaria, T., Steffen, B. (eds.) ISoLA 2010, Part II. LNCS, vol.\u00a06416, pp. 82\u201396. Springer, Heidelberg (2010)"},{"key":"29_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"128","DOI":"10.1007\/11867340_10","volume-title":"Formal Modeling and Analysis of Timed Systems","author":"A. David","year":"2006","unstructured":"David, A., H\u00e5kansson, J., Larsen, K.G., Pettersson, P.: Model checking timed automata with priorities using DBM subtraction. In: Asarin, E., Bouyer, P. (eds.) FORMATS 2006. LNCS, vol.\u00a04202, pp. 128\u2013142. Springer, Heidelberg (2006)"},{"key":"29_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"230","DOI":"10.1007\/11549970_17","volume-title":"Formal Techniques for Computer Systems and Business Processes","author":"G. D\u00edaz","year":"2005","unstructured":"D\u00edaz, G., Pardo, J.-J., Cambronero, M.-E., Valero, V., Cuartero, F.: Automatic Translation of WS-CDL Choreographies to Timed Automata. In: Bravetti, M., Kloul, L., Zavattaro, G. (eds.) EPEW\/WS-EM 2005. LNCS, vol.\u00a03670, pp. 230\u2013242. Springer, Heidelberg (2005)"},{"issue":"8","key":"29_CR9","doi-asserted-by":"publisher","first-page":"453","DOI":"10.1145\/360933.360975","volume":"18","author":"E.W. Dijkstra","year":"1975","unstructured":"Dijkstra, E.W.: Guarded commands, nondeterminacy and formal derivation of programs. Commun. ACM\u00a018(8), 453\u2013457 (1975)","journal-title":"Commun. ACM"},{"key":"29_CR10","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4612-3228-5","volume-title":"Predicate calculus and program semantics","author":"E.W. Dijkstra","year":"1990","unstructured":"Dijkstra, E.W., Scholten, C.S.: Predicate calculus and program semantics. Springer-Verlag New York, Inc., New York (1990)"},{"key":"29_CR11","doi-asserted-by":"publisher","first-page":"287","DOI":"10.1007\/s10270-010-0155-y","volume":"10","author":"S. Gilmore","year":"2011","unstructured":"Gilmore, S., G\u00f6nczy, L., Koch, N., Mayer, P., Tribastone, M., Varr\u00f3, D.: Non-functional properties in the model-driven development of service-oriented systems. Software and Systems Modeling\u00a010, 287\u2013311 (2011), doi:10.1007\/s10270-010-0155-y","journal-title":"Software and Systems Modeling"},{"key":"29_CR12","first-page":"539","volume-title":"Proceedings of the 11th IEEE International Conference on Embedded and Real-Time Computing Systems and Applications, RTCSA 2005","author":"P.-A. Hsiung","year":"2005","unstructured":"Hsiung, P.-A., Lin, S.-W.: Model checking timed systems with priorities. In: Proceedings of the 11th IEEE International Conference on Embedded and Real-Time Computing Systems and Applications, RTCSA 2005, pp. 539\u2013544. IEEE Computer Society Press, Washington, DC (2005)"},{"key":"29_CR13","unstructured":"Ivanov, D.: Integrating formal analysis methods in PROGRESS IDE. Master of science thesis, Malardalen Research and Technology Centre, Vasteras, Sweden (June 2011)"},{"key":"29_CR14","doi-asserted-by":"crossref","unstructured":"Ivanov, D., Orlic, M., Seceleanu, C., Vulgarakis, A.: Remes tool-chain - a set of integrated tools for behavioral modeling and analysis of embedded systems. In: Proceedings of the 25th IEEE\/ACM International Conference on Automated Software Engineering, ASE 2010 (September 2010)","DOI":"10.1145\/1858996.1859076"},{"key":"29_CR15","unstructured":"Kavantzas, N., Burdett, D., Ritzinger, G., Fletcher, T., Lafon, Y., Barreto, C.: Web services choreography description language version 1.0. World Wide Web Consortium, Candidate Recommendation CR-ws-cdl-10-20051109 (November 2005)"},{"key":"29_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"493","DOI":"10.1007\/3-540-44585-4_47","volume-title":"Computer Aided Verification","author":"K.G. Larsen","year":"2001","unstructured":"Larsen, K.G., Behrmann, G., Brinksma, E., Fehnker, A., Hune, T., Pettersson, P., Romijn, J.: As Cheap as Possible: Efficient Cost-Optimal Reachability for Priced Timed Automata. In: Berry, G., Comon, H., Finkel, A. (eds.) CAV 2001. LNCS, vol.\u00a02102, pp. 493\u2013505. Springer, Heidelberg (2001), http:\/\/portal.acm.org\/citation.cfm?id=647770.734117"},{"key":"29_CR17","doi-asserted-by":"publisher","first-page":"197","DOI":"10.1016\/j.tcs.2007.09.021","volume":"390","author":"K.G. Larsen","year":"2008","unstructured":"Larsen, K.G., Rasmussen, J.I.: Optimal reachability for multi-priced timed automata. Theor. Comput. Sci.\u00a0390, 197\u2013213 (2008), http:\/\/portal.acm.org\/citation.cfm?id=1330765.1330861","journal-title":"Theor. Comput. Sci."},{"key":"29_CR18","doi-asserted-by":"publisher","first-page":"77","DOI":"10.1145\/511446.511457","volume-title":"WWW 2002: Proceedings of the 11th International Conference on World Wide Web","author":"S. Narayanan","year":"2002","unstructured":"Narayanan, S., McIlraith, S.A.: Simulation, verification and automated composition of web services. In: WWW 2002: Proceedings of the 11th International Conference on World Wide Web, pp. 77\u201388. ACM, New York (2002)"},{"key":"29_CR19","unstructured":"Object Management Group (OMG): Business Process Modeling Notation (BPMN) version 1.1 (January 2008), http:\/\/www.omg.org\/spec\/BPMN\/1.1\/"},{"key":"29_CR20","unstructured":"Orli\u0107, M.: Resource usage prediction in component-based software systems. Phd thesis, Faculty of electrical engineering and computing, University of Zagreb (November 2010)"},{"issue":"1","key":"29_CR21","doi-asserted-by":"crossref","first-page":"77","DOI":"10.3233\/APO-2005-000008","volume":"1","author":"D. Roman","year":"2005","unstructured":"Roman, D., Keller, U., Lausen, H., de Bruijn, J., Lara, R., Stollberg, M., Polleres, A., Feier, C., Bussler, C., Fensel, D.: Web service modeling ontology. Applied Ontology\u00a01(1), 77\u2013106 (2005)","journal-title":"Applied Ontology"},{"key":"29_CR22","doi-asserted-by":"publisher","first-page":"43","DOI":"10.1109\/ICWS.2004.1314722","volume-title":"ICWS 2004: Proceedings of the IEEE International Conference on Web Services","author":"G. Sala\u00fcn","year":"2004","unstructured":"Sala\u00fcn, G., Bordeaux, L., Schaerf, M.: Describing and reasoning on web services using process algebra. In: ICWS 2004: Proceedings of the IEEE International Conference on Web Services, p. 43. IEEE Computer Society Press, Washington, DC (2004)"},{"key":"29_CR23","doi-asserted-by":"crossref","unstructured":"Seceleanu, C., Vulgarakis, A., Pettersson, P.: Remes: A resource model for embedded systems. In: In Proc. of the 14th IEEE International Conference on Engineering of Complex Computer Systems (ICECCS 2009). IEEE Computer Society (June 2009)","DOI":"10.1109\/ICECCS.2009.49"},{"issue":"5","key":"29_CR24","first-page":"1","volume":"1","author":"M.H. Beek Ter","year":"2007","unstructured":"Ter Beek, M.H., Bucchiarone, A., Gnesi, S.: Formal methods for service composition. Annals of Mathematics, Computing & Teleinformatics\u00a01(5), 1\u201310 (2007), http:\/\/journals.teilar.gr\/amct\/ ; In: Annals of Mathematics, Computing & Teleinformatics, vol. 1(5), pp. 1\u201310. Technological Education Institute of Larissa (TEIL), Greece (2007)","journal-title":"Annals of Mathematics, Computing & Teleinformatics"},{"key":"29_CR25","doi-asserted-by":"publisher","first-page":"271","DOI":"10.1007\/s10619-010-7060-9","volume":"27","author":"I. Weber","year":"2010","unstructured":"Weber, I., Hoffmann, J., Mendling, J.: Beyond soundness: on the verification of semantic business process models. Distrib. Parallel Databases\u00a027, 271\u2013343 (2010), http:\/\/dx.doi.org\/10.1007\/s10619-010-7060-9","journal-title":"Distrib. Parallel Databases"}],"container-title":["Lecture Notes in Computer Science","Leveraging Applications of Formal Methods, Verification and Validation. Applications and Case Studies"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-34032-1_29.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,4,9]],"date-time":"2025-04-09T13:14:42Z","timestamp":1744204482000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-34032-1_29"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012]]},"ISBN":["9783642340314","9783642340321"],"references-count":25,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-34032-1_29","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2012]]}}}