Campus Units

Computer Science

Document Type

Conference Proceeding

Conference

European Symposium on Programming (ESOP 2009)

Publication Version

Accepted Manuscript

Link to Published Version

https://doi.org/10.1007/978-3-642-00590-9_24

Publication Date

2009

Journal or Book Title

Programming Languages and Systems. ESOP 2009. Lecture Notes in Computer Science

Volume

5502

First Page

333

Last Page

347

DOI

10.1007/978-3-642-00590-9_24

Conference Date

March 22-29, 2009

City

York, UK

Abstract

Web services are distributed software components, that are decoupled from each other using interfaces with specified functional behaviors. However, such behavioral specifications are insufficient to demonstrate compliance with certain temporal non-functional policies. An example is demonstrating that a patient’s health-related query sent to a health care service is answered only by a doctor (and not by a secretary). Demonstrating compliance with such policies is important for satisfying governmental privacy regulations. It is often necessary to expose the internals of the web service implementation for demonstrating such compliance, which may compromise modularity. In this work, we provide a language design that enables such demonstrations, while hiding majority of the service’s source code. The key idea is to use greybox specifications to allow service providers to selectively hide and expose parts of their implementation. The overall problem of showing compliance is then reduced to two subproblems: whether the desired properties are satisfied by the service’s greybox specification, and whether this greybox specification is satisfied by the service’s implementation. We specify policies using LTL and solve the first problem by model checking. We solve the second problem by refinement techniques.

Comments

The final publication is available at Springer via https://doi.org/10.1007/978-3-642-00590-9_24. Rajan H., Tao J., Shaner S., Leavens G.T. (2009) Tisa: A Language Design and Modular Verification Technique for Temporal Policies in Web Services. In: Castagna G. (eds) Programming Languages and Systems. ESOP 2009. Lecture Notes in Computer Science, vol 5502. doi: 10.1007/978-3-642-00590-9_24. Posted with permission.

Copyright Owner

Springer-Verlag Berlin Heidelberg

Language

en

File Format

application/pdf

Published Version

Share

Article Location

 
COinS