Catálogo de publicaciones - libros

During Web service discovery, capabilities of Web services are of major concern. This paper proposes an environment ontology based approach for specifying Web service capability semantically. First, a meta-level environment ontology is adopted in the proposed approach to provide formal and sharable specifications of environment resources in a particular domain. For each environment resource, we build a corresponding hierarchical state machine specifying its dynamic characteristics. Second, we propose to use the effect of a Web service on its environment resources for specifying the Web service capability and to designate the effect as the traces of the state transitions the Web service can impose on its environment resources. Finally, we give the mechanism to match service query with service capability description.

The reusability of components affects how much benefit we can get from the component based software development (CBSD). For enhancing the reuse of components, we propose an approach to derive the desired behavior from a component in terms of the user’s requirement given by a scenario specification. In our proposal, a special environment, i.e., sup-inclusive environment (SIE), is automatically constructed to adjust the component’s behavior based on the scenario specification. All behavior of a component that is specified by the scenario specification can be preserved in the composition of the component and its SIE, and other behavior of the component is discarded to the most extent. We use interface automata to model the behavior of components and a set of action sequences to abstract the scenario specification in Message Sequence Charts (MSCs). The composition of components is modelled by the product of interface automata. We give the algorithm for constructing SIE and illustrate our approach by an example.

Recently, a promising programming model called Orc has been proposed to support a structured way of orchestrating distributed web services. Orc is intuitive because it offers concise constructors to manage concurrent communication, time-outs, priorities, failure of sites or communication and so forth. The semantics of Orc is also precisely defined. However, there is no verification tool available to verify critical properties against Orc models. Instead of building one from scratch, we believe the existing mature model-checkers can be reused. In this work, we first define a Timed Automata semantics for the Orc language, which we prove is semantically equivalent to the original operational semantics of Orc . Consequently, Timed Automata models are systematically constructed from Orc models. The practical implication of the construction is that tool supports for Timed Automata, e.g., Uppaal , can be used to model check Orc models. An experimental tool is implemented to automate our approach.

A choreography is a multi-part contract which describes peer to peer collaboration of services regardless of any specific programming language or supporting platform. WS-CDL, issued from W3C, is the first language for describing choreography. In this paper, we propose a language CDL _0 to capture the important features of WS-CDL, including choreography composition, compensation and exception handling. An adjunctive concept role reference is introduced with the aim of distinguishing multiple participants which provide the same kind of service within a choreography model. The semantics is given by an operational approach to provide a formal base for the choreography language. We believe this formalism work helps to clear ambiguous points in the WS-CDL specification and promote the usage of choreography languages.

The Web Services Choreography Description Language (WS-CDL) is a W3C specification developed for the description of peer-to-peer collaborations of participants from a global viewpoint. Currently WS-CDL has no rigorous static type checking. We believe that introducing a type system will exclude many design and description errors, and ensure desirable properties of the choreography specifications. In this paper, we took a core language CDL, which covers most of the important features of the WS-CDL, and is more convenient for the study. We developed the abstract syntax and operational semantics of CDL, and defined a collection of rules which can be used to check if choreography is well-typed. Moreover, we also proved some type safety theorems for CDL in the sense that well-typed choreography cannot get stuck. We show how the use of type information can allow us to gain confidence in the correctness of choreography.

A non-blocking program is one that uses non-blocking primitives, such as load-linked/store-conditional and compare-and-swap, for synchronisation instead of locks so that no process is ever blocked. According to their progress properties, non-blocking programs may be classified as wait-free, lock-free or obstruction-free. However, a precise description of these properties does not exist and it is not unusual to find a definition that is ambiguous or even incorrect. We present a formal definition of the progress properties so that any confusion is removed. The formalisation also allows one to prove the widely believed presumption that wait-freedom is a special case of lock-freedom, which in turn is a special case of obstruction-freedom.

Modern software systems place a large emphasis on heterogeneous communication. For disparate applications to communicate effectively, a generic theory of data is required that works at the inter-application level. The key feature of such a theory is full generality , where the data model of an application is not restricted to any particular modeling formalism. Existing solutions do not have this property: while any data can be encoded in terms of XML or using the Semantic Web, such representations provide only basic generality , whereby to reason about an arbitrary application’s data model it must be re-expressed using the formalism in question. In this paper we present a theory of data which is fully generic and utilizes an extensible design to allow the underlying formalisms to be incorporated into a specification only when necessary. We then show how this theory can be used to investigate two common data equivalence problems — canonicalization and transformation — independently of the datatypes involved.

We propose a framework for the verification of statecharts. We use the CSP/FDR framework to model complex systems designed in statecharts, and check for system consistency or verify special properties within the specification. We have developed an automated translation from statecharts into CSP and exploited it in both theoretical and practical senses.

Timed CSP extends CSP by introducing a capability to quantify temporal aspects of sequencing and synchronization. It is a powerful language to model real time reactive systems. However, there is no verification tool support for proving critical properties over systems modelled using Timed CSP. In this work, we construct a reasoning method using Constraint Logic Programming (CLP) as an underlying reasoning mechanism for Timed CSP. We start with encoding the semantics of Timed CSP in CLP, which allows a systematic translation of Timed CSP to CLP. Powerful constraint solver like CLP( $\mathcal{R}$ ) is then used to prove traditional safety properties and beyond, e.g., reachability, deadlock-freeness, timewise refinement relationship, lower or upper bound of a time interval, etc. Counter-examples are generated when properties are not satisfied. Moreover, our method also handles useful extensions to Timed CSP. Finally, we demonstrate the effectiveness of our approach through case study of standard real time systems.

RT-LOTOS is a timed process algebra which enables compact and abstract specification of real-time systems. This paper proposes and illustrates a structural translation of RT-LOTOS terms into behaviorally equivalent (timed bisimilar) finite Time Petri nets. It is therefore possible to apply Time Petri nets verification techniques to the profit of RT-LOTOS. Our approach has been implemented in RTL2TPN, a prototype tool which takes as input an RT-LOTOS specification and outputs a TPN. The latter is verified using TINA, a TPN analyzer developed by LAAS-CNRS. The toolkit made of RTL2TPN and TINA has been positively benchmarked against previously developed RT-LOTOS verification tool.