Publikationen

Abstract: We describe a use of formal methods to specify and check a Web Services protocol. The Web Services Atomic Transaction protocol was specified in TLA+ and checked with the TLC model checker. A modest effort revealed oversights that caused unanticipated behaviors of the protocol; these were corrected by clarifications and changes to the protocol.

Abstract: Business data is one of the most critical components of the IT portfolio of any enterprise. However enterprises are facing a major challenge of providing a holistic view of it when the data spans across multiple heterogeneous systems with different data models embedded in them. To achieve maximum benefits from the SOA, it is crucial to create a common data management approach that handles all aspects of integrating information exposed through different autonomous services in an enterprise. We present an approach by which it becomes possible to provide the holistic view of business data by actively driving simplicity and SOA project acceleration. It allows us to integrate the supply chain applications of an enterprise and hence building a competitively differentiated supply chain for the future.

Abstract: In this paper we show an approach to business activity modelling, with emphasis on identification of Services, messages being exchanged between them, collaboration scenarios and coordination protocols to be considered for the fulfilment of those scenarios. The modelling technique has been developed during business process analysis at Lufthansa Technik AG. An airframe related components overhaul process has been researched, in order to advise the concerned department, on application of loosely coupled systems. The analysis provides a basis for the inception of a SOA-based system, for the handling of airframe related components. The presented technique is not limited to the aerospace industry, but constitutes a generic approach to Service-Oriented Modelling. The main focus of this technique is the transformation from traditional, activity-based model, towards a model based upon message exchange between the participating Services. Further transition leads to the identification of collaboration patterns involved in the business activity. Given those patterns it is possible, to prove the applicability of standardized coordination protocols to the particular collaboration. We derive a methodology for structural approach to the management of business activities in SOA context, based on our experience gathered during the described analysis.

Abstract: This contribution proposes an approach that is necessary to model cross enterprise business processes using Service Oriented Modeling and its realization by leveraging standard Web Services protocols. It stresses the need for validation of produced models at every step of development which is essential to reduce the mistakes at early stages and raise the level of confidence. It also assures that all important aspects are considered at the right level of abstraction whereas programmatic support allows reducing project completion time.

Abstract: Creation of formal specifications is being considered a relief for the difficulties of inception and construction of distributed systems. Numerous formal methods exist for the purpose of description of distributed systems and protocols. The creation of formal specifications for these systems lacks the extensive support by tools vendors. This results in lack of sophisticated tools, which help the developer to overcome the initial training investment, shallowing the learning curve. Thus, the development of formal specification for the systems under construction stays an expensive undertaking, which lacks the immediate results, important for the overall acceptance of formal methods by the industry. In this paper we describe a plugin for the Eclipse IDE, developed to simplify the task of authoring formal specifications in the TLA+ environment. This plugin provides features, expected from an IDE for a common programming language, such as syntax highlighting, autocompletion and execution assistance.

Abstract: Web Service protocol standards should be unambiguous and provide a complete description of the allowed behavior of the protocols_ participants. Implementation of such protocols is an error-prone process, firstly because of the lack of precision and completeness of the standards, and secondly because of erroneous transformation of semantics from the specification to the final implementation. Applying the TLA+ paradigm we first consider the protocol on an abstract level. Safety properties taken from real world scenarios are compared to the facilities of the protocol. As result, we identified some limitation of applicability of the WS-BA protocol to abstract application use cases, modelled from the real world scenarios. These limitations are an omission of possible activities seen in the real world. Further, WS-C and WS-BA make assumptions about the internal structures of the participants, violating SOA paradigm. The former error could be detected by the use of formal methods. The latter can be circumvented by a sophisticated implementation strategy. The proposed strategy of implementing WS-Coordination and WS-BusinessActivity allows non-intrusive integration of the transactional framework, considering SOA requirements. This paper describes the results of analysis and some design decisions taken during the proof-of-concept implementation of WS-C and WS-BA frameworks.

Abstract: This paper proposes the sequence of steps that are necessary to produce efficiently working Service Oriented Architecture for cross enterprise business processes and stresses the need for verification and programmatic support at every step of development. Verification of produced models at early stages allows the reduction of mistakes and assures that all important aspects have been included whereas programmatic support reduces the 'double' work and allows reducing project completion time.

Abstract: We describe a use of formal methods to specify and check a Web Services protocol. The Web Services Atomic Transaction protocol was specified in TLA+ and checked with the TLC model checker. A modest effort revealed oversights that caused unanticipated behaviors of the protocol; these were corrected by clarifications and changes to the protocol.