Publications in Specification

Articles in Refereed Journals:

1. L. Baresi, D. Bianculli, C. Ghezzi, S. Guinea, P. Spoletini. Validation of web service compositions. IET Software, Vol. 1, Num. 6, pages 219-232, December 2007.
   Abstract: Web services support software architectures that can evolve dynamically. In particular, in this paper the focus is on architectures where services are composed (orchestrated) through a workflow described in the business process execution language (BPEL). It is assumed that the resulting composite service refers to external services through assertions that specify their expected functional and non-functional properties. On the basis of these assertions, the composite service may be verified at design time by checking that it ensures certain relevant properties. Because of the dynamic nature of web services and the multiple stakeholders involved in their provision, however, the external services may evolve dynamically, and even unexpectedly. They may become inconsistent with respect to the assertions against which the workflow was verified during development. As a consequence, validation of the composition must extend to run time. In this work, an assertion language, called assertion language for BPEL process interactions (ALBERT), is introduced; it can be used to specify both functional and non-functional properties. An environment which supports design-time verification of ALBERT assertions for BPEL workflows via model checking is also described. At run time, the assertions can be turned into checks that a software monitor performs on the composite system to verify that it continues to guarantee its required properties. A TeleAssistance application is provided as a running example to illustrate our validation framework.

Articles in Refereed Conferences:

1. Wei-Tek Tsai, Yinong Chen, Raymond A. Paul. Specification-Based Verification and Validation of Web Services and Service-Oriented Operating Systems. WORDS, pages 139-147, 2005.
   Abstract: Service-Oriented Architecture (SOA) and Web Services (WS) have received significant attention recently. Even though WS are based on open standards and support software interoperability, but the trustworthy issues of WS has actually limited the growth of WS applications as organizations do not trust those WS developed by other vendors and at the same time they do not have access to the source code. This paper addressed this issue by proposing several solutions including specification-based verification and validation, collaborative testing, and group testing. The key concept is that it is possible to provide a comprehensive evaluation of WS even if their source code is not available.

Technical Reports and Manuals:

1. The OMG Group. UML$^\mathrm{TM}$ Profile for Modeling Quality of Service and Fault Tolerance Characteristics and Mechanisms. Num. ptc/2005-05-02, The OMG Group, May 2005.

2. Akhil Sahai, Anna Durante, Vijay Machiraju. Towards Automated SLA Management for Web Services. Num. HPL-2001-310, HP Laboratories, July 2002.
   Abstract: In order to automate SLA management it is essential to specify SLAs in precise and unambiguous manner as well as keep the specification flexible. While precision will help automate the process of monitoring and metric collection, flexibility will enable extending it to unforeseen service level agreement specifications.

3. Svend Frolund, Jari Koistinen. QML: A Language for Quality of Service Specification. Num. HPL-98-10, 63 pages, HP Laboratories, 1998.
   Abstract: To be competitive, future software system must provide not only the correct functionality, but also an adequate level of quality of service (QoS). By QoS, we refer to non-functional properties, such as reliability, performance, timing, and security. To provide an adequate level of QoS, software systems need to include capabilities such as QoS negotiation, monitoring, and adaptation. These capabilities all require the expected and the provided QoS levels to be explicitly specified. QoS can be specified statically at the time of implementation, design, or dynamically at deployment or runtime. To facilitate QoS specification, we present a general Quality of service Modeling Language (QML) for defining multi-category QoS specifications for components in distributed object systems. QML is designed to support QoS in general, encompassing QoS categories such as reliability, performance, security, and timing. QoS specification in QML facilitate the static decomposition of a software system into components with precisely specified QoS boundaries. They also facilitate dynamic QoS functions, such as negotiations, monitoring, and adaptation. QML is designed for a good fit with object-oriented distributed architectures and concepts such as interfaces and inheritance. It also allows specification at a fine-grained level for operations, operation arguments, and attributes. QML enables user- defined QoS categories, and allows specifications within those categories to be associated with component interface definitions. In addition, checks can be made dynamically to determine whether one QML specification satisfies another. This mechanism allows us to dynamically match QoS requirements and offers