Modular Verification of Asynchronous Service Interactions Using Behavioral Interfaces

Download

index.pdf

Date

2013-04-01

Author

Betin Can, Aysu
Bultan, Tevfik

Metadata

Show full item record

This work is licensed under a Creative Commons Attribution-NonCommercial-NoDerivatives 4.0 International License.

Item Usage Stats

194
views

0
downloads

A crucial problem in service oriented computing is the specification and analysis of interactions among multiple peers that communicate via messages. We propose a design pattern that enables the specification of behavioral interfaces acting as communication contracts between peers. This “peer controller pattern” provides a modular, assume-guarantee style verification strategy that consists of three phases. 1) Each individual peer is statically verified for conformance to its part of the contract, using software model checking. 2) Alternately, a runtime enforcement mechanism blocks the communication events that violate the interface specification at runtime. 3) Using either of these two mechanisms, it can be assumed that the participating peers behave according to their interfaces and safety and liveness properties about the global behavior of the composite web service can then be verified directly on the communication contract. The interface verification of each peer and the behavior verification are hence handled in separate steps. A Java implementation of this pattern is developed and tested on a series of examples; we show that by working in such a modular fashion, it is possible to automatically and efficiently verify properties about service interactions that would otherwise be impossible to verify.

Subject Keywords

Web services, Automated verification, Runtime enforcement, Asynchronous communication, Design patterns

URI

https://hdl.handle.net/11511/31336

Journal

IEEE Transactions on Services Computing

DOI

https://doi.org/10.1109/tsc.2011.55

Collections

Graduate School of Informatics, Article

Suggestions

OpenMETU
Core

Simulation and performance evaluation of a distributed real-time communication protocol for industrial embedded systems Aybar, Güray; Schmidt, Şenan Ece; Department of Electrical and Electronics Engineering (2011) The Dynamic Distributed Dependable Real-Time Industrial communication Protocol (D3RIP) provides service guarantees for Real-Time traffic and integrates the dynamically changing requirements of automation applications in their operation to efficiently utilize the resources. The protocol dynamically allocates the network resources according to the respective system state. To this end, the protocol architecture consists of an Interface Layer that provides time-slotted operation and a Coordination Layer that as...
Semantic interoperability of the un/cefact ccts based electronic business document standards Kabak, Yıldıray; Doğaç, Asuman; Department of Computer Engineering (2009) The interoperability of the electronic documents exchanged in eBusiness applications is an important problem in industry. Currently, this problem is handled by the mapping experts who understand the meaning of every element in the involved document schemas and define the mappings among them which is a very costly and tedious process. In order to improve electronic document interoperability, the UN/CEFACT produced the Core Components Technical Specification (CCTS) which defines a common structure and semanti...
Automatic quality of service (QOS) evaluation for domain specific web service discovery framework Aşkaroğlu, Emra; Karagöz, Pınar; Department of Computer Engineering (2011) Web Service technology is one of the most rapidly developing contemporary technologies. Nowadays, Web Services are being used by a large number of projects and academic studies all over the world. As the use of Web service technology is increasing, it becomes harder to find the most suitable web service which meets the Quality of Service (QoS) as well as functional requirements of the user. In addition, quality of the web services (QoS) that take part in the software system becomes very important. In this t...
Flexible querying in an intelligent object-oriented database environment Koyuncu, M; Yazıcı, Adnan; George, R (2000-10-28) Many new-generation database applications demand intelligent information management necessitating efficient interactions between database gr. knowledge bases and the users. In this study we discuss evaluation of imprecise queries in an intelligent object-oriented database environment, IFOOD. A flexible query evaluation mechanism, capable of handling different data types including complex and imprecise data and knowledge is presented and key language issues are addressed.
Implementation and evaluation of a synchronous time-slotted medium access protocol for networked industrial embedded systems Gözcü, Ahmet Korhan; Schmidt, Şenan Ece; Department of Electrical and Electronics Engineering (2011) Dynamic Distributed Dependable Real-time Industrial communication Protocol family (D3RIP), has been proposed in the literature considering the periodic or event-based traffic characteristics of the industrial communication networks. D3RIP framework consists of two protocol families: Interface Layer (IL) protocol family, which is responsible for providing the accurate time-division multiple access (TDMA) on top of a shared-medium broadcast channel, and Coordination Layer (CL), which is defined to fulfill the...

Citation Formats

A. Betin Can and T. Bultan, “Modular Verification of Asynchronous Service Interactions Using Behavioral Interfaces,” IEEE Transactions on Services Computing, pp. 262–275, 2013, Accessed: 00, 2020. [Online]. Available: https://hdl.handle.net/11511/31336.