{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,26]],"date-time":"2025-03-26T04:22:21Z","timestamp":1742962941008,"version":"3.40.3"},"publisher-location":"Berlin, Heidelberg","reference-count":64,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642285240"},{"type":"electronic","value":"9783642285257"}],"license":[{"start":{"date-parts":[[2012,1,1]],"date-time":"2012-01-01T00:00:00Z","timestamp":1325376000000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2012]]},"DOI":"10.1007\/978-3-642-28525-7_7","type":"book-chapter","created":{"date-parts":[[2012,2,20]],"date-time":"2012-02-20T02:24:41Z","timestamp":1329704681000},"page":"192-216","source":"Crossref","is-referenced-by-count":0,"title":["A Logical Approach to Data-Aware Automated Sequence Generation"],"prefix":"10.1007","author":[{"given":"Sylvain","family":"Hall\u00e9","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Roger","family":"Villemaire","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Omar","family":"Cherkaoui","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Rudy","family":"Deca","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"7_CR1","unstructured":"Proceedings of the 20th Conference on Systems Administration (LISA 2006), Washington, D.C., USA, December 3-8. USENIX (2006)"},{"key":"7_CR2","unstructured":"Amazon e-commerce service (2009), http:\/\/docs.amazonwebservices.com\/AWSEcommerceService\/2005-03-23\/"},{"key":"7_CR3","unstructured":"soapUI: the web services testing tool (2009), http:\/\/www.soapui.org\/"},{"key":"7_CR4","unstructured":"Cisco IOS switching services command reference, release 12.3 (2010), http:\/\/www.cisco.com\/en\/US\/docs\/ios\/12_3\/switch\/command\/reference\/swtch_r.html"},{"issue":"11","key":"7_CR5","doi-asserted-by":"publisher","first-page":"832","DOI":"10.1145\/182.358434","volume":"26","author":"J.F. Allen","year":"1983","unstructured":"Allen, J.F.: Maintaining knowledge about temporal intervals. Communications of the ACM\u00a026(11), 832\u2013843 (1983)","journal-title":"Communications of the ACM"},{"key":"7_CR6","volume-title":"Web Services, Concepts, Architectures and Applications","author":"G. Alonso","year":"2004","unstructured":"Alonso, G., Casati, F., Kuno, H., Machiraju, V.: Web Services, Concepts, Architectures and Applications. Springer, Heidelberg (2004)"},{"key":"7_CR7","doi-asserted-by":"crossref","unstructured":"Andr\u00e9ka, H., van Benthem, J., N\u00e9meti, I.: Modal languages and bounded fragments of predicate logic. Journal of Philosophical Logic\u00a0(27), 217\u2013274 (1998)","DOI":"10.1023\/A:1004275029985"},{"key":"7_CR8","unstructured":"Arnold II, T.R.: Visual Test 6 Bible. Wiley (1998)"},{"key":"7_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"44","DOI":"10.1007\/978-3-540-24622-0_5","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"H. Barringer","year":"2004","unstructured":"Barringer, H., Goldberg, A., Havelund, K., Sen, K.: Rule-Based Runtime Verification. In: Steffen, B., Levi, G. (eds.) VMCAI 2004. LNCS, vol.\u00a02937, pp. 44\u201357. Springer, Heidelberg (2004)"},{"key":"7_CR10","doi-asserted-by":"crossref","unstructured":"Barringer, H., Rydeheard, D., Havelund, K.: Rule systems for run-time monitoring: From Eagle to RuleR. Journal of Logic and Computation (2008)","DOI":"10.1093\/logcom\/exn076"},{"key":"7_CR11","series-title":"Perspectives in Mathematical Logic","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-59207-2","volume-title":"The Classical Decision Problem","author":"E. B\u00f6rger","year":"1997","unstructured":"B\u00f6rger, E., Gr\u00e4del, E., Gurevich, Y.: The Classical Decision Problem. Perspectives in Mathematical Logic. Springer, Heidelberg (1997)"},{"key":"7_CR12","unstructured":"Burgess, M., Couch, A.: Modeling next generation configuration management tools. In: LISA [1], pp. 131\u2013147"},{"key":"7_CR13","unstructured":"Christensen, E., Curbera, F., Meredith, G., Weerawarana, S.: Web services description language (WSDL) 1.1, W3C note (2001)"},{"key":"7_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"359","DOI":"10.1007\/3-540-45657-0_29","volume-title":"Computer Aided Verification","author":"A. Cimatti","year":"2002","unstructured":"Cimatti, A., Clarke, E.M., Giunchiglia, E., Giunchiglia, F., Pistore, M., Roveri, M., Sebastiani, R., Tacchella, A.: NuSMV 2: An OpenSource Tool for Symbolic Model Checking. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol.\u00a02404, pp. 359\u2013364. Springer, Heidelberg (2002)"},{"key":"7_CR15","unstructured":"Claessen, K., S\u00f6rensson, N.: New techniques that improve MACE-style model finding. In: Proc. of Workshop on Model Computation, MODEL (2003)"},{"key":"7_CR16","unstructured":"Clarke, E.M., Grumberg, O., Peled, D.A.: Model Checking. MIT Press (2000)"},{"issue":"1","key":"7_CR17","doi-asserted-by":"publisher","first-page":"58","DOI":"10.4018\/jebr.2006010104","volume":"2","author":"F. Daniel","year":"2006","unstructured":"Daniel, F., Pernici, B.: Insights into web service orchestration and choreography. Int. Journal of E-Business Research\u00a02(1), 58\u201377 (2006)","journal-title":"Int. Journal of E-Business Research"},{"key":"7_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"249","DOI":"10.1007\/3-540-48683-6_23","volume-title":"Computer Aided Verification","author":"M. Daniele","year":"1999","unstructured":"Daniele, M., Giunchiglia, F., Vardi, M.Y.: Improved Automata Generation for Linear Temporal Logic. In: Halbwachs, N., Peled, D. (eds.) CAV 1999. LNCS, vol.\u00a01633, pp. 249\u2013260. Springer, Heidelberg (1999)"},{"key":"7_CR19","unstructured":"Demri, S., Jensen, C.S. (eds.): 15th International Symposium on Temporal Representation and Reasoning, TIME 2008, Universit\u00e9 du Qu\u00e9bec \u00e0 Monte\u00e9al, Canada, June 16-18. IEEE Computer Society (2008)"},{"key":"7_CR20","unstructured":"Desai, N., Bradshaw, R., Lueninghoener, C.: Directing change using Bcfg2. In: LISA [1], pp. 215\u2013220"},{"key":"7_CR21","doi-asserted-by":"crossref","unstructured":"Deutsch, A., Sui, L., Vianu, V.: Specification and verification of data-driven web services. In: Deutsch, A. (ed.) PODS, pp. 71\u201382. ACM (2004)","DOI":"10.1145\/1055558.1055571"},{"key":"7_CR22","doi-asserted-by":"crossref","unstructured":"Dixon, C., Fisher, M., Konev, B., Lisitsa, A.: Practical first-order temporal reasoning. In: Demri, Jensen (eds.) [19], pp. 156\u2013163","DOI":"10.1109\/TIME.2008.15"},{"key":"7_CR23","doi-asserted-by":"crossref","unstructured":"Duret-Lutz, A., Poitrenaud, D.: Spot: An extensible model checking library using transition-based generalized b\u00fcchi automata. In: DeGroot, D., Harrison, P.G., Wijshoff, H.A.G., Segall, Z. (eds.) MASCOTS, pp. 76\u201383. IEEE Computer Society (2004)","DOI":"10.1109\/MASCOT.2004.1348184"},{"key":"7_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"177","DOI":"10.1007\/11687818_14","volume-title":"Autonomic Communication","author":"D. Ga\u00efti","year":"2006","unstructured":"Ga\u00efti, D., Pujolle, G., Salaun, M., Zimmermann, H.: Autonomous Network Equipments. In: Stavrakakis, I., Smirnov, M. (eds.) WAC 2005. LNCS, vol.\u00a03854, pp. 177\u2013185. Springer, Heidelberg (2006)"},{"key":"7_CR25","doi-asserted-by":"crossref","unstructured":"Gerth, R., Peled, D., Vardi, M.Y., Wolper, P.: Simple on-the-fly automatic verification of linear temporal logic. In: Dembinski, P., Sredniawa, M. (eds.) PSTV. IFIP Conference Proceedings, vol.\u00a038, pp. 3\u201318. Chapman & Hall (1995)","DOI":"10.1007\/978-0-387-34892-6_1"},{"issue":"1","key":"7_CR26","doi-asserted-by":"publisher","first-page":"1719","DOI":"10.2307\/2586808","volume":"64","author":"E. Gr\u00e4del","year":"1999","unstructured":"Gr\u00e4del, E.: On the restraining power of guards. Journal of Symbolic Logic\u00a064(1), 1719\u20131742 (1999)","journal-title":"Journal of Symbolic Logic"},{"key":"7_CR27","series-title":"Texts in Theoretical Computer Science. An EATCS Series","volume-title":"Finite Model Theory and Its Applications","author":"E. Gr\u00e4del","year":"2007","unstructured":"Gr\u00e4del, E., Kolaitis, P.G., Libkin, L., Marx, M., Spencer, J., Vardi, M.Y., Venema, Y., Weinstein, S.: Finite Model Theory and Its Applications. Texts in Theoretical Computer Science. An EATCS Series. Springer, Heidelberg (2007)"},{"key":"7_CR28","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"42","DOI":"10.1007\/978-3-642-19589-1_3","volume-title":"WS-FM","author":"S. Hall\u00e9","year":"2011","unstructured":"Hall\u00e9, S.: Automated Generation of Web Service Stubs Using LTL Satisfiability Solving. In: Bravetti, M., Bultan, T. (eds.) WS-FM 2010. LNCS, vol.\u00a06551, pp. 42\u201355. Springer, Heidelberg (2011)"},{"key":"7_CR29","doi-asserted-by":"crossref","unstructured":"Hall\u00e9, S.: Causality in message-based contract violations: A temporal logic \u201cwhodunit\u201d. In: EDOC, pp. 171\u2013180. IEEE Computer Society (2011)","DOI":"10.1109\/EDOC.2011.21"},{"key":"7_CR30","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"147","DOI":"10.1007\/978-3-540-30184-4_13","volume-title":"Utility Computing","author":"S. Hall\u00e9","year":"2004","unstructured":"Hall\u00e9, S., Deca, R., Cherkaoui, O., Villemaire, R., Puche, D.: A Formal Validation Model for the Netconf Protocol. In: Sahai, A., Wu, F. (eds.) DSOM 2004. LNCS, vol.\u00a03278, pp. 147\u2013158. Springer, Heidelberg (2004)"},{"key":"7_CR31","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"516","DOI":"10.1007\/978-3-642-10383-4_38","volume-title":"Service-Oriented Computing","author":"S. Hall\u00e9","year":"2009","unstructured":"Hall\u00e9, S., Hughes, G., Bultan, T., Alkhalaf, M.: Generating Interface Grammars from WSDL for Automated Verification of Web Services. In: Baresi, L., Chi, C.-H., Suzuki, J. (eds.) ICSOC-ServiceWave 2009. LNCS, vol.\u00a05900, pp. 516\u2013530. Springer, Heidelberg (2009)"},{"key":"7_CR32","doi-asserted-by":"crossref","unstructured":"Hall\u00e9, S., Villemaire, R.: Runtime monitoring of message-based workflows with data. In: EDOC, pp. 63\u201372. IEEE Computer Society (2008)","DOI":"10.1109\/EDOC.2008.32"},{"key":"7_CR33","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"337","DOI":"10.1007\/978-3-540-88871-0_23","volume-title":"On the Move to Internet Systems: OTM 2008","author":"S. Hall\u00e9","year":"2008","unstructured":"Hall\u00e9, S., Villemaire, R.: XML Methods for Validation of Temporal Properties on Message Traces with Data. In: Meersman, R., Tari, Z. (eds.) OTM 2008. LNCS, vol.\u00a05331, pp. 337\u2013353. Springer, Heidelberg (2008)"},{"issue":"5","key":"7_CR34","doi-asserted-by":"publisher","first-page":"669","DOI":"10.1109\/TSE.2009.29","volume":"35","author":"S. Hall\u00e9","year":"2009","unstructured":"Hall\u00e9, S., Villemaire, R., Cherkaoui, O.: Specifying and validating data-aware temporal web service properties. IEEE Trans. Software Eng.\u00a035(5), 669\u2013683 (2009)","journal-title":"IEEE Trans. Software Eng."},{"key":"7_CR35","doi-asserted-by":"crossref","unstructured":"Hall\u00e9, S., Villemaire, R., Cherkaoui, O.: Logical methods for self-configuration of network devices. In: Formal and Practical Aspects of Autonomic Computing and Networking: Specification, Development and Verification, pp. 189\u2013216 (2011)","DOI":"10.4018\/978-1-60960-845-3.ch008"},{"key":"7_CR36","unstructured":"Hinnelund, P.: Autonomic computing. Master\u2019s thesis, School of Computer Science and Engineering, Royal Institute of Engineering (March 2004)"},{"key":"7_CR37","doi-asserted-by":"publisher","first-page":"205","DOI":"10.1023\/A:1015178417181","volume":"70","author":"I.M. Hodkinson","year":"2002","unstructured":"Hodkinson, I.M.: Loosely guarded fragment of first-order logic has the finite model property. Studia Logica\u00a070, 205\u2013240 (2002)","journal-title":"Studia Logica"},{"key":"7_CR38","unstructured":"Holzmann, G.J.: The SPIN Model Checker: Primer and Reference Manual. Addison-Wesley Professional (2003)"},{"key":"7_CR39","doi-asserted-by":"crossref","unstructured":"Hughes, G., Bultan, T., Alkhalaf, M.: Client and server verification for web services using interface grammars. In: Bultan, T., Xie, T. (eds.) TAV-WEB, pp. 40\u201346. ACM (2008)","DOI":"10.1145\/1390832.1390839"},{"key":"7_CR40","doi-asserted-by":"crossref","unstructured":"Jackson, D., Schechter, I., Shlyakhter, I.: Alcoa: the Alloy constraint analyzer. In: ICSE, pp. 730\u2013733 (2000)","DOI":"10.1145\/337180.337616"},{"key":"7_CR41","unstructured":"Josephraj, J.: Web services choreography in practice (2005), http:\/\/www128.ibm.com\/developerworks\/webservices\/library\/ws-choreography\/"},{"key":"7_CR42","unstructured":"Kautz, H.A., Selman, B.: Planning as satisfiability. In: ECAI, pp. 359\u2013363 (1992)"},{"key":"7_CR43","doi-asserted-by":"crossref","unstructured":"Khurshid, S., Marinov, D.: TestEra: Specification-based testing of Java programs using SAT. Automated Software Engineering Journal\u00a011(4) (2004)","DOI":"10.1023\/B:AUSE.0000038938.10589.b9"},{"key":"7_CR44","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"325","DOI":"10.1007\/3-540-60045-0_60","volume-title":"Computer Aided Verification","author":"O. Kupferman","year":"1995","unstructured":"Kupferman, O.: Augmenting Branching Temporal Logics with Existential Quantification Over Atomic Propositions. In: Wolper, P. (ed.) CAV 1995. LNCS, vol.\u00a0939, pp. 325\u2013338. Springer, Heidelberg (1995)"},{"key":"7_CR45","doi-asserted-by":"publisher","first-page":"447","DOI":"10.1007\/BF01458217","volume":"76","author":"L. L\u00f6wenheim","year":"1915","unstructured":"L\u00f6wenheim, L.: Uber m\u00f6glichkeiten im relativkalk\u00fcl. Math. Annalen\u00a076, 447\u2013470 (1915)","journal-title":"Math. Annalen"},{"key":"7_CR46","doi-asserted-by":"crossref","unstructured":"Lutz, C., Wolter, F., Zakharyaschev, M.: Temporal description logics: A survey. In: Demri, Jensen (eds.) [19], pp. 3\u201314","DOI":"10.1109\/TIME.2008.14"},{"key":"7_CR47","unstructured":"Martin, D., Burstein, M., Hobbs, J., Lassila, O., McDermott, D., McIlraith, S., Narayanan, S., Paolucci, M., Parsia, B., Payne, T., Sirin, E., Srinivasan, N., Sycara, K.: OWL-S: Semantic markup for web services (2008), http:\/\/www.ai.sri.com\/daml\/services\/owl-s\/1.2\/overview"},{"key":"7_CR48","doi-asserted-by":"crossref","unstructured":"Martin, E., Basu, S., Xie, T.: Automated testing and response analysis of web services. In: ICWS, pp. 647\u2013654. IEEE Computer Society (2007)","DOI":"10.1109\/ICWS.2007.49"},{"key":"7_CR49","unstructured":"McCune, W.: A davis-putnam program and its application to finite first-order model search: Quasigroup existence problems. Technical report, Argonne National Laboratory (1994)"},{"key":"7_CR50","volume-title":"Introduction to Mathematical Logic","author":"E. Mendelson","year":"1997","unstructured":"Mendelson, E.: Introduction to Mathematical Logic, 4th edn. Springer, Heidelberg (1997)","edition":"4"},{"key":"7_CR51","unstructured":"Narain, S.: Towards a foundation for building distributed systems via configuration (2004) (retrieved February 11, 2010)"},{"key":"7_CR52","unstructured":"Narain, S.: Network configuration management via model finding. In: LISA, pp. 155\u2013168. USENIX (2005)"},{"key":"7_CR53","doi-asserted-by":"crossref","unstructured":"Narayanan, S., McIlraith, S.A.: Simulation, verification and automated composition of web services. In: WWW, pp. 77\u201388 (2002)","DOI":"10.1145\/511446.511457"},{"key":"7_CR54","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"257","DOI":"10.1007\/11527800_20","volume-title":"Unconventional Programming Paradigms","author":"M. Parashar","year":"2005","unstructured":"Parashar, M., Hariri, S.: Autonomic Computing: An Overview. In: Ban\u00e2tre, J.-P., Fradet, P., Giavitto, J.-L., Michel, O. (eds.) UPP 2004. LNCS, vol.\u00a03566, pp. 257\u2013269. Springer, Heidelberg (2005)"},{"key":"7_CR55","unstructured":"Pepelnjak, I., Guichard, J.: MPLS VPN Architectures. Cisco Press (2001)"},{"key":"7_CR56","doi-asserted-by":"crossref","unstructured":"Pnueli, A.: The temporal logic of programs. In: FOCS, pp. 46\u201357. IEEE (1977)","DOI":"10.1109\/SFCS.1977.32"},{"key":"7_CR57","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"43","DOI":"10.1007\/978-3-540-30581-1_5","volume-title":"Semantic Web Services and Web Process Composition","author":"J. Rao","year":"2005","unstructured":"Rao, J., Su, X.: A Survey of Automated Web Service Composition Methods. In: Cardoso, J., Sheth, A.P. (eds.) SWSWPC 2004. LNCS, vol.\u00a03387, pp. 43\u201354. Springer, Heidelberg (2005)"},{"key":"7_CR58","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"110","DOI":"10.1007\/11817949_8","volume-title":"CONCUR 2006 \u2013 Concurrency Theory","author":"A. Rensink","year":"2006","unstructured":"Rensink, A.: Model Checking Quantified Computation Tree Logic. In: Baier, C., Hermanns, H. (eds.) CONCUR 2006. LNCS, vol.\u00a04137, pp. 110\u2013125. Springer, Heidelberg (2006)"},{"key":"7_CR59","doi-asserted-by":"crossref","unstructured":"Rosen, E.C., Rekhter, Y.: BGP\/MPLS VPNs (RFC 2547) (March 1999)","DOI":"10.17487\/rfc2547"},{"key":"7_CR60","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"149","DOI":"10.1007\/978-3-540-73370-6_11","volume-title":"Model Checking Software","author":"K.Y. Rozier","year":"2007","unstructured":"Rozier, K.Y., Vardi, M.Y.: LTL Satisfiability Checking. In: Bo\u0161na\u010dki, D., Edelkamp, S. (eds.) SPIN 2007. LNCS, vol.\u00a04595, pp. 149\u2013167. Springer, Heidelberg (2007)"},{"key":"7_CR61","unstructured":"Tanenbaum, A.S.: Computer Networks, 4th edn. Prentice Hall (2002)"},{"key":"7_CR62","unstructured":"Trakhtenbrot, B.A.: Impossibility of an algorithm for the decision problem in finite classes. Doklady Akademii Nauk SSSR\u00a0(70), 569\u2013572 (1950)"},{"issue":"3","key":"7_CR63","doi-asserted-by":"publisher","first-page":"223","DOI":"10.1109\/TC.1982.1675978","volume":"31","author":"G. Bochmann von","year":"1982","unstructured":"von Bochmann, G.: Hardware specification with temporal logic: En example. IEEE Trans. Computers\u00a031(3), 223\u2013231 (1982)","journal-title":"IEEE Trans. Computers"},{"key":"7_CR64","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"308","DOI":"10.1007\/3-540-61511-3_96","volume-title":"Automated Deduction - Cade-13","author":"J. Zhang","year":"1996","unstructured":"Zhang, J., Zhang, H.: System Description: Generating Models by SEM. In: McRobbie, M.A., Slaney, J.K. (eds.) CADE 1996. LNCS, vol.\u00a01104, pp. 308\u2013312. Springer, Heidelberg (1996)"}],"container-title":["Lecture Notes in Computer Science","Transactions on Computational Science XV"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-28525-7_7","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,3,21]],"date-time":"2025-03-21T06:05:22Z","timestamp":1742537122000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-28525-7_7"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012]]},"ISBN":["9783642285240","9783642285257"],"references-count":64,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-28525-7_7","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2012]]}}}