{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,27]],"date-time":"2025-03-27T05:40:28Z","timestamp":1743054028989,"version":"3.40.3"},"publisher-location":"Berlin, Heidelberg","reference-count":44,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642005893"},{"type":"electronic","value":"9783642005909"}],"license":[{"start":{"date-parts":[[2009,1,1]],"date-time":"2009-01-01T00:00:00Z","timestamp":1230768000000},"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":[[2009]]},"DOI":"10.1007\/978-3-642-00590-9_24","type":"book-chapter","created":{"date-parts":[[2009,3,27]],"date-time":"2009-03-27T08:05:58Z","timestamp":1238141158000},"page":"333-347","source":"Crossref","is-referenced-by-count":7,"title":["Tisa: A Language Design and Modular Verification Technique for Temporal Policies in Web Services"],"prefix":"10.1007","author":[{"given":"Hridesh","family":"Rajan","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Jia","family":"Tao","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Steve","family":"Shaner","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Gary T.","family":"Leavens","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"issue":"10","key":"24_CR1","doi-asserted-by":"publisher","first-page":"24","DOI":"10.1145\/944217.944233","volume":"46","author":"M.P. Papazoglou","year":"2003","unstructured":"Papazoglou, M.P., Georgakopoulos, D.: Service-oriented computing: Introduction. Commun. ACM\u00a046(10), 24\u201328 (2003)","journal-title":"Commun. ACM"},{"key":"24_CR2","unstructured":"Christensen, E., Curbera, F., Meredith, G., Weerawarana, S.: Web services description language (WSDL) 1.1. Technical report, World Wide Web Consortium (March 2001)"},{"key":"24_CR3","doi-asserted-by":"crossref","unstructured":"Barth, A., Mitchell, J., Datta, A., Sundaram, S.: Privacy and utility in business processes. In: CSF 2007, pp. 279\u2013294 (2007)","DOI":"10.1109\/CSF.2007.26"},{"issue":"3","key":"24_CR4","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/1127878.1127884","volume":"31","author":"G.T. Leavens","year":"2006","unstructured":"Leavens, G.T., Baker, A.L., Ruby, C.: Preliminary design of JML: a behavioral interface specification language for Java. SIGSOFT Softw. Eng. Notes\u00a031(3), 1\u201338 (2006)","journal-title":"SIGSOFT Softw. Eng. Notes"},{"key":"24_CR5","doi-asserted-by":"crossref","unstructured":"Barbon, F., Traverso, P., Pistore, M., Trainotti, M.: Run-time monitoring of instances and classes of web service compositions. In: ICWS 2006, pp. 63\u201371 (2006)","DOI":"10.1109\/ICWS.2006.113"},{"key":"24_CR6","doi-asserted-by":"crossref","unstructured":"Baresi, L., Ghezzi, C., Guinea, S.: Smart monitors for composed services. In: ICSOC 2004, pp. 193\u2013202 (2004)","DOI":"10.1145\/1035167.1035195"},{"key":"24_CR7","doi-asserted-by":"crossref","unstructured":"Castagna, G., Gesbert, N., Padovani, L.: A theory of contracts for web services. In: POPL 2008, pp. 261\u2013272 (2008)","DOI":"10.1145\/1328438.1328471"},{"key":"24_CR8","doi-asserted-by":"crossref","unstructured":"Kuo, D., Fekete, A., Greenfield, P., Nepal, S., Zic, J., Parastatidis, S., Webber, J.: Expressing and reasoning about service contracts in service-oriented computing. In: ICWS 2006, pp. 915\u2013918 (2006)","DOI":"10.1109\/ICWS.2006.62"},{"key":"24_CR9","doi-asserted-by":"crossref","unstructured":"Wada, H., Suzuki, J., Oba, K.: Modeling non-functional aspects in service oriented architecture. In: IEEE International Conference on Services Computing (SCC 2006), pp. 222\u2013229 (2006)","DOI":"10.1109\/SCC.2006.74"},{"key":"24_CR10","doi-asserted-by":"crossref","unstructured":"Parnas, D.L.: On the criteria to be used in decomposing systems into modules\u00a015(12), 1053\u20131058 (1972)","DOI":"10.1145\/361598.361623"},{"key":"24_CR11","unstructured":"B\u00fcchi, M., Weck, W.: The greybox approach: When blackbox specifications hide too much. Technical Report 297, Turku Center for Computer Science (August 1999)"},{"key":"24_CR12","doi-asserted-by":"crossref","unstructured":"Back, R.J.R., von Wright, J.: Refinement calculus, part i: sequential nondeterministic programs. In: REX workshop, pp. 42\u201366 (1990)","DOI":"10.1007\/3-540-52559-9_60"},{"issue":"3","key":"24_CR13","doi-asserted-by":"publisher","first-page":"287","DOI":"10.1016\/0167-6423(87)90011-6","volume":"9","author":"J.M. Morris","year":"1987","unstructured":"Morris, J.M.: A theoretical basis for stepwise refinement and the programming calculus. Sci. Comput. Program.\u00a09(3), 287\u2013306 (1987)","journal-title":"Sci. Comput. Program."},{"key":"24_CR14","volume-title":"Model checking","author":"M. Edmund","year":"1999","unstructured":"Edmund, M., Clarke, J., Grumberg, O., Peled, D.A.: Model checking. MIT Press, Cambridge (1999)"},{"key":"24_CR15","doi-asserted-by":"crossref","unstructured":"Shaner, S.M., Leavens, G.T., Naumann, D.A.: Modular verification of higher-order methods with mandatory calls specified by model programs. In: OOPSLA 2007, pp. 351\u2013368 (2007)","DOI":"10.1145\/1297027.1297053"},{"key":"24_CR16","doi-asserted-by":"crossref","unstructured":"Necula, G.C.: Proof-carrying code. In: POPL 1997, pp. 106\u2013119 (1997)","DOI":"10.1145\/263699.263712"},{"key":"24_CR17","doi-asserted-by":"crossref","unstructured":"Rajan, H., Hosamani, M.: Tisa: Towards trustworthy services in a service-oriented architecture. IEEE Transactions on Services Computing (SOC) 1(2) (2008)","DOI":"10.1109\/TSC.2008.18"},{"key":"24_CR18","doi-asserted-by":"crossref","unstructured":"Hosamani, M., Narayanappa, H., Rajan, H.: How to trust a web service monitor deployed in an untrusted environment? In: NWESP 2007: Proceedings of the Third International Conference on Next Generation Web Services Practices, pp. 79\u201384 (2007)","DOI":"10.1109\/NWESP.2007.25"},{"issue":"3","key":"24_CR19","doi-asserted-by":"publisher","first-page":"381","DOI":"10.1145\/2166.357215","volume":"5","author":"B. Liskov","year":"1983","unstructured":"Liskov, B., Scheifler, R.: Guardians and actions: Linguistic support for robust, distributed programs. TOPLAS\u00a05(3), 381\u2013404 (1983)","journal-title":"TOPLAS"},{"issue":"3","key":"24_CR20","doi-asserted-by":"publisher","first-page":"277","DOI":"10.1007\/s00165-004-0058-1","volume":"17","author":"A.D. Gordon","year":"2005","unstructured":"Gordon, A.D., Pucella, R.: Validating a web service security abstraction by typing. Formal Aspects of Computing\u00a017(3), 277\u2013318 (2005)","journal-title":"Formal Aspects of Computing"},{"key":"24_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"155","DOI":"10.1007\/978-3-540-70592-5_8","volume-title":"ECOOP 2008 \u2013 Object-Oriented Programming","author":"H. Rajan","year":"2008","unstructured":"Rajan, H., Leavens, G.T.: Ptolemy: A language with quantified typed events. In: Vitek, J. (ed.) ECOOP 2008. LNCS, vol.\u00a05142, pp. 155\u2013179. Springer, Heidelberg (2008)"},{"issue":"3","key":"24_CR22","doi-asserted-by":"publisher","first-page":"321","DOI":"10.1016\/j.scico.2006.02.009","volume":"63","author":"C. Clifton","year":"2006","unstructured":"Clifton, C., Leavens, G.T.: MiniMAO1: Investigating the semantics of proceed. Science of Computer Programming\u00a063(3), 321\u2013374 (2006)","journal-title":"Science of Computer Programming"},{"key":"24_CR23","doi-asserted-by":"crossref","unstructured":"Igarashi, A., Pierce, B., Wadler, P.: Featherweight Java: A minimal core calculus for Java and GJ. In: OOPSLA 1999, pp. 132\u2013146 (1999)","DOI":"10.1145\/320385.320395"},{"key":"24_CR24","doi-asserted-by":"crossref","unstructured":"Flatt, M., Krishnamurthi, S., Felleisen, M.: A programmer\u2019s reduction semantics for classes and mixins. In: Formal Syntax and Semantics of Java, pp. 241\u2013269 (1999)","DOI":"10.1007\/3-540-48737-9_7"},{"key":"24_CR25","unstructured":"Clifton, C.: A design discipline and language features for modular reasoning in aspect-oriented programs. Technical Report 05-15, Iowa State University (Jul 2005)"},{"issue":"1","key":"24_CR26","doi-asserted-by":"publisher","first-page":"38","DOI":"10.1006\/inco.1994.1093","volume":"115","author":"A.K. Wright","year":"1994","unstructured":"Wright, A.K., Felleisen, M.: A syntactic approach to type soundness. Information and Computation\u00a0115(1), 38\u201394 (1994)","journal-title":"Information and Computation"},{"key":"24_CR27","unstructured":"Rajan, H., Tao, J., Shaner, S.M., Leavens, G.T.: Reconciling trust and modularity in web services. Technical Report 08-07, Dept. of Computer Sc., Iowa State U. (July 2008)"},{"key":"24_CR28","unstructured":"Vardi, M.Y., Wolper, P.: An automata-theoretic approach to automatic program verification. In: Proceedings of the First Symposium on Logic in Computer Science, pp. 322\u2013331 (1986)"},{"key":"24_CR29","unstructured":"Buchi, J.: On a decision method in restricted second order arithmetic. In: Proc. Internat. Congr. Logic, Method. and Philos. Sci., pp. 1\u201312 (1960)"},{"issue":"3","key":"24_CR30","doi-asserted-by":"publisher","first-page":"199","DOI":"10.1016\/S0164-1212(02)00041-9","volume":"65","author":"M. Barnett","year":"2003","unstructured":"Barnett, M., Schulte, W.: Runtime verification of .net contracts. Journal of Systems and Software\u00a065(3), 199\u2013208 (2003)","journal-title":"Journal of Systems and Software"},{"key":"24_CR31","unstructured":"Barnett, M., Schulte, W.: Spying on components: A runtime verification technique. In: Workshop on Specification and Verification of Component-Based Systems (2001)"},{"issue":"4","key":"24_CR32","first-page":"517","volume":"25","author":"M. Barnett","year":"2001","unstructured":"Barnett, M., Schulte, W.: The ABCs of specification: AsmL, Behavior, and Components. Informatica\u00a025(4), 517\u2013526 (2001)","journal-title":"Informatica"},{"issue":"6","key":"24_CR33","doi-asserted-by":"publisher","first-page":"826","DOI":"10.1145\/268999.269003","volume":"44","author":"H. Wasserman","year":"1997","unstructured":"Wasserman, H., Blum, M.: Software reliability via run-time result-checking. J. ACM\u00a044(6), 826\u2013849 (1997)","journal-title":"J. ACM"},{"key":"24_CR34","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-540-24617-6_1","volume-title":"Formal Approaches to Software Testing","author":"B. Tyler","year":"2004","unstructured":"Tyler, B., Soundarajan, N.: Black-box testing of grey-box behavior. In: Petrenko, A., Ulrich, A. (eds.) FATES 2003. LNCS, vol.\u00a02931, pp. 1\u201314. Springer, Heidelberg (2004)"},{"key":"24_CR35","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"34","DOI":"10.1007\/978-3-540-77351-1_4","volume-title":"Software Composition","author":"M. Bravetti","year":"2007","unstructured":"Bravetti, M., Zavattaro, G.: Towards a unifying theory for choreography conformance and contract compliance. In: Lumpe, M., Vanderperren, W. (eds.) SC 2007. LNCS, vol.\u00a04829, pp. 34\u201350. Springer, Heidelberg (2007)"},{"issue":"2","key":"24_CR36","doi-asserted-by":"publisher","first-page":"110","DOI":"10.1016\/j.scico.2008.02.001","volume":"71","author":"L. Acciai","year":"2008","unstructured":"Acciai, L., Boreale, M.: XPi: A typed process calculus for XML messaging. Science of Computer Programming\u00a071(2), 110\u2013143 (2008)","journal-title":"Science of Computer Programming"},{"key":"24_CR37","doi-asserted-by":"crossref","unstructured":"Bartoletti, M., Degano, P., Ferrari, G.L.: Types and effects for secure service orchestration. In: CSFW, pp. 57\u201369 (2006)","DOI":"10.1109\/CSFW.2006.31"},{"issue":"1","key":"24_CR38","doi-asserted-by":"publisher","first-page":"33","DOI":"10.1109\/TSE.2007.70740","volume":"34","author":"M. Bartoletti","year":"2008","unstructured":"Bartoletti, M., Degano, P., Ferrari, G.L., Zunino, R.: Semantics-based design for secure web services. IEEE Trans. Software Eng.\u00a034(1), 33\u201349 (2008)","journal-title":"IEEE Trans. Software Eng."},{"key":"24_CR39","doi-asserted-by":"crossref","unstructured":"Wei, J., Singaravelu, L., Pu, C.: Guarding sensitive information streams through the jungle of composite web services. In: ICWS 2007, pp. 455\u2013462 (2007)","DOI":"10.1109\/ICWS.2007.93"},{"key":"24_CR40","doi-asserted-by":"crossref","unstructured":"Srivatsa, M., Iyengar, A., Mikalsen, T., Rouvellou, I., Yin, J.: An access control system for web service compositions. In: ICWS 2007, pp. 1\u20138 (2007)","DOI":"10.1109\/ICWS.2007.31"},{"key":"24_CR41","doi-asserted-by":"crossref","unstructured":"Skalka, C., Wang, X.S.: Trust but verify: authorization for web services. In: SWS, pp. 47\u201355 (2004)","DOI":"10.1145\/1111348.1111354"},{"key":"24_CR42","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"107","DOI":"10.1007\/978-3-540-30477-7_8","volume-title":"Programming Languages and Systems","author":"C. Skalka","year":"2004","unstructured":"Skalka, C., Smith, S.F.: History effects and verification. In: Chin, W.-N. (ed.) APLAS 2004. LNCS, vol.\u00a03302, pp. 107\u2013128. Springer, Heidelberg (2004)"},{"key":"24_CR43","doi-asserted-by":"crossref","unstructured":"Biskup, J., Carminati, B., Ferrari, E., Muller, F., Wortmann, S.: Towards secure execution orders for composite web services. In: ICWS 2007, pp. 489\u2013496 (2007)","DOI":"10.1109\/ICWS.2007.179"},{"key":"24_CR44","doi-asserted-by":"crossref","unstructured":"Vorobiev, A., Han, J.: Specifying dynamic security properties of web service based systems. In: SKG 2006, p. 34 (2006)","DOI":"10.1109\/SKG.2006.99"}],"container-title":["Lecture Notes in Computer Science","Programming Languages and Systems"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-00590-9_24","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,19]],"date-time":"2019-05-19T00:23:47Z","timestamp":1558225427000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-00590-9_24"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2009]]},"ISBN":["9783642005893","9783642005909"],"references-count":44,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-00590-9_24","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2009]]}}}