publication . Preprint . 2010

SMT-based Verification of LTL Specifications with Integer Constraints and its Application to Runtime Checking of Service Substitutability

Bersani, Marcello M.; Cavallaro, Luca; Frigeri, Achille; Pradella, Matteo; Rossi, Matteo;
Open Access English
  • Published: 16 Apr 2010
Abstract
An important problem that arises during the execution of service-based applications concerns the ability to determine whether a running service can be substituted with one with a different interface, for example if the former is no longer available. Standard Bounded Model Checking techniques can be used to perform this check, but they must be able to provide answers very quickly, lest the check hampers the operativeness of the application, instead of aiding it. The problem becomes even more complex when conversational services are considered, i.e., services that expose operations that have Input/Output data dependencies among them. In this paper we introduce a f...
Subjects
free text keywords: Computer Science - Logic in Computer Science, Computer Science - Software Engineering
Funded by
EC| SMSCOM
Project
SMSCOM
Self-Managing Situated Computing
  • Funder: European Commission (EC)
  • Project Code: 227977
  • Funding stream: FP7 | SP2 | ERC
Download from
27 references, page 1 of 2

[1] V. De Antonellis, M. Melchiori, L. De Santis, M. Mecella, E. Mussi, B. Pernici, and P. Plebani, “A layered architecture for flexible web service invocation,” Softw. Pract. Exper., vol. 36, no. 2, pp. 191-223, 2006.

[2] K. Verma, K. Gomadam, A. Sheth, J. Miller, and Z. Wu, “The METEOR-S approach for configuring and executing dynamic web processes,” LSDIS Lab, University of Georgia, Athens, Georgia, Tech. Rep. LSDIS Technical Report 05-001, 2005.

[3] L. Cavallaro, E. Di Nitto, and M. Pradella, “An automatic approach to enable replacement of conversational services,” in ICSOC/ServiceWave, 2009, pp. 159-174. [OpenAIRE]

[4] L. Cavallaro, E. Di Nitto, P. Pelliccione, M. Pradella, and M. Tivoli, “Synthesizing adapters for conversational webservices from their WSDL interface,” in SEAMS '10. ACM, 2010. [OpenAIRE]

[5] S. Ranise and C. Tinelli, standard: Version 1.2,” Tech. http://combination.cs.uiowa.edu/smtlib/.

[6] L. Cavallaro, G. Ripa, and M. Zuccala`, “Adapting service requests to actual service interfaces through semantic annotations,” in Proceedings of PESOS, 2009. [OpenAIRE]

[7] M. M. Bersani, A. Frigeri, M. Pradella, M. Rossi, A. Morzenti, and P. San Pietro, “SMT-based Bounded Model Checking with Difference Logic Constraints,” http://arXiv:submit/0018237, Politecnico di Milano, Tech. Rep., 2010.

[8] H. Comon and V. Cortier, “Flatness Is Not a Weakness,” in CSL, 2000, pp. 262-276.

[9] A. Biere, A. Cimatti, E. M. Clarke, O. Strichman, and Y. Zhu, “Bounded model checking,” Advances in Computers, vol. 58, pp. 118-149, 2003.

[10] A. Biere, K. Heljanko, T. A. Junttila, T. Latvala, and V. Schuppan, “Linear encodings of bounded ltl model checking,” Logical Methods in Computer Science, vol. 2, no. 5, 2006. [OpenAIRE]

[11] M. Pradella, A. Morzenti, and P. San Pietro, “The symmetry of the past and of the future: bi-infinite time in the verification of temporal properties,” in ESEC/SIGSOFT FSE, 2007, pp. 312-320. [OpenAIRE]

[12] M. Pradella, A. Morzenti and P. San Pietro, “A metric encoding for bounded model checking,” in FM 2009: Formal Methods, ser. Lecture Notes in Computer Science, A. Cavalcanti and D. Dams, Eds., vol. 5850. Springer, 2009, pp. 741-756. [OpenAIRE]

[13] C. Drumm, “Improving schema mapping by exploiting domain knowledge,” Ph.D. dissertation, Universitat Karlsruhe, Fakultat fur Informatik, 2008. [OpenAIRE]

[14] M. Fredj, N. Georgantas, V. Issarny, and A. Zarras, “Dynamic service substitution in service-oriented architectures,” in Proceedings of SERVICES, 2008. [OpenAIRE]

[15] T. Schaeck and R. Thompson, “WS-ResourceProperties,” http://docs.oasis-open.org/wsrp/Misc/, 2003.

27 references, page 1 of 2
Abstract
An important problem that arises during the execution of service-based applications concerns the ability to determine whether a running service can be substituted with one with a different interface, for example if the former is no longer available. Standard Bounded Model Checking techniques can be used to perform this check, but they must be able to provide answers very quickly, lest the check hampers the operativeness of the application, instead of aiding it. The problem becomes even more complex when conversational services are considered, i.e., services that expose operations that have Input/Output data dependencies among them. In this paper we introduce a f...
Subjects
free text keywords: Computer Science - Logic in Computer Science, Computer Science - Software Engineering
Funded by
EC| SMSCOM
Project
SMSCOM
Self-Managing Situated Computing
  • Funder: European Commission (EC)
  • Project Code: 227977
  • Funding stream: FP7 | SP2 | ERC
Download from
27 references, page 1 of 2

[1] V. De Antonellis, M. Melchiori, L. De Santis, M. Mecella, E. Mussi, B. Pernici, and P. Plebani, “A layered architecture for flexible web service invocation,” Softw. Pract. Exper., vol. 36, no. 2, pp. 191-223, 2006.

[2] K. Verma, K. Gomadam, A. Sheth, J. Miller, and Z. Wu, “The METEOR-S approach for configuring and executing dynamic web processes,” LSDIS Lab, University of Georgia, Athens, Georgia, Tech. Rep. LSDIS Technical Report 05-001, 2005.

[3] L. Cavallaro, E. Di Nitto, and M. Pradella, “An automatic approach to enable replacement of conversational services,” in ICSOC/ServiceWave, 2009, pp. 159-174. [OpenAIRE]

[4] L. Cavallaro, E. Di Nitto, P. Pelliccione, M. Pradella, and M. Tivoli, “Synthesizing adapters for conversational webservices from their WSDL interface,” in SEAMS '10. ACM, 2010. [OpenAIRE]

[5] S. Ranise and C. Tinelli, standard: Version 1.2,” Tech. http://combination.cs.uiowa.edu/smtlib/.

[6] L. Cavallaro, G. Ripa, and M. Zuccala`, “Adapting service requests to actual service interfaces through semantic annotations,” in Proceedings of PESOS, 2009. [OpenAIRE]

[7] M. M. Bersani, A. Frigeri, M. Pradella, M. Rossi, A. Morzenti, and P. San Pietro, “SMT-based Bounded Model Checking with Difference Logic Constraints,” http://arXiv:submit/0018237, Politecnico di Milano, Tech. Rep., 2010.

[8] H. Comon and V. Cortier, “Flatness Is Not a Weakness,” in CSL, 2000, pp. 262-276.

[9] A. Biere, A. Cimatti, E. M. Clarke, O. Strichman, and Y. Zhu, “Bounded model checking,” Advances in Computers, vol. 58, pp. 118-149, 2003.

[10] A. Biere, K. Heljanko, T. A. Junttila, T. Latvala, and V. Schuppan, “Linear encodings of bounded ltl model checking,” Logical Methods in Computer Science, vol. 2, no. 5, 2006. [OpenAIRE]

[11] M. Pradella, A. Morzenti, and P. San Pietro, “The symmetry of the past and of the future: bi-infinite time in the verification of temporal properties,” in ESEC/SIGSOFT FSE, 2007, pp. 312-320. [OpenAIRE]

[12] M. Pradella, A. Morzenti and P. San Pietro, “A metric encoding for bounded model checking,” in FM 2009: Formal Methods, ser. Lecture Notes in Computer Science, A. Cavalcanti and D. Dams, Eds., vol. 5850. Springer, 2009, pp. 741-756. [OpenAIRE]

[13] C. Drumm, “Improving schema mapping by exploiting domain knowledge,” Ph.D. dissertation, Universitat Karlsruhe, Fakultat fur Informatik, 2008. [OpenAIRE]

[14] M. Fredj, N. Georgantas, V. Issarny, and A. Zarras, “Dynamic service substitution in service-oriented architectures,” in Proceedings of SERVICES, 2008. [OpenAIRE]

[15] T. Schaeck and R. Thompson, “WS-ResourceProperties,” http://docs.oasis-open.org/wsrp/Misc/, 2003.

27 references, page 1 of 2
Powered by OpenAIRE Research Graph
Any information missing or wrong?Report an Issue