04/30/2010, 2pm, GHC-6501
For a system of distributed processes, correctness can be ensured by (statically) checking whether their composition satisfies properties of interest. However, web services are distributed processes that dynamically discover properties of other web services. Since the overall system may not be available statically and since each business process is supposed to be relatively simple, we propose to use (on-line) runtime monitoring of conversations between partners as a means of checking behavioral correctness of the entire web service system. Our system allows users to specify behavioral correctness properties. By transforming these properties to finite-state automata, we enable conformance checking of finite execution traces of web services described in BPEL against the specification.
Moreover, when the violations are discovered at runtime, we automatically propose and rank recovery plans which users can then select for execution. For some of the violations, such plans essentially involve ``going back'' ---compensating the occurred actions until an alternative behavior of the application is possible.
For other violations, such plans include both ``going back'' and ``re-planning'' -- guiding the application towards a desired behavior. In this talk, we describe how to express recovery as a planning problem and report on results of implementing this approach using the SAT-based plan encoding.
Joint work with:
E. Lai (Cambridge), N. Oury (Edinburgh, CSBE) and J. Ollivier (Edinburgh, CSBE and McGill)
Marsha Chechik is Professor and Vice Chair in the Department of Computer Science at the University of Toronto. She received her Ph.D. from the University of Maryland in 1996. Prof. Chechik's research interests are in the application of formal methods to improve the quality of software. She has authored over 80 papers in formal methods, software specification and verification, computer security and requirements engineering. In 2002-2003, Prof. Chechik was a visiting scientist at Lucent Technologies in Murray Hill, NY and at Imperial College, London UK. She is an associate editor of IEEE Transactions on Software Engineering 2003-2007, 2010-present. She is a member of IFIP WG 2.9 on Requirements Engineering and an Associate Editor of Journal on Software and Systems Modeling. She regularly serves on program committees of international conferences in the areas of software engineering and automated verification. Marsha Chechik was a Co-Chair of the 2008 International Conference on Concurrency Theory (CONCUR), Program Committee Co-Chair of the 2008 International Conference on Computer Science and Software Engineering (CASCON), and Program Committee Co-Chair of the 2009 International Conference on Formal Aspects of Software Engineering (FASE).