Publications
Journal Articles | Conference Contributions
Journal Articles
James E. Johnson, David E. Langworthy, Leslie Lamport and Friedrich H. Vogt. Formal Specification of a Web Services Protocol. Journal of Logic and Algebraic Programming, 70(1):34–52, 2007.
@Article{Telematik_JLLV_2007_Formal,
author = {James E. Johnson and David E. Langworthy and Leslie Lamport and Friedrich H. Vogt},
title = {Formal Specification of a Web Services Protocol},
pages = {34-52},
journal = {Journal of Logic and Algebraic Programming},
volume = {70},
number = {1},
year = 2007,
}
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.
Conference Contributions
Arsalan Minhas and Friedrich H. Vogt. Service Orientation for Dynamic Enterprises. In Proceedings of the International Conference on
Logistics and Supply Chain Management (LSCM'06), January 2006. Hong Kong.
@InProceedings{Telematik_AV_2006_ServiceOrientationDynamicEnterprises,
author = {Arsalan Minhas and Friedrich H. Vogt},
title = {Service Orientation for Dynamic Enterprises},
booktitle = {Proceedings of the International Conference on
Logistics and Supply Chain Management (LSCM'06)},
day = {5-7},
month = jan,
year = 2006,
location = {Hong Kong},
}
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.
Boris Gruschko, Friedrich H. Vogt and Simon Zambrovski. Business Activities in an Industrial Context. In Proceedings of the International Conference on
Logistics and Supply Chain Management (LSCM'06), January 2006. Hong Kong.
@InProceedings{Telematik_GVZ_2006_BusinessActivity,
author = {Boris Gruschko and Friedrich H. Vogt and Simon Zambrovski},
title = {Business Activities in an Industrial Context},
booktitle = {Proceedings of the International Conference on
Logistics and Supply Chain Management (LSCM'06)},
day = {5-7},
month = jan,
year = 2006,
location = {Hong Kong},
}
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.
Friedrich H. Vogt and Arsalan Minhas. Using Service Orientation to Drive Business Processes. In Proceedings of the 9th IEEE International Multi
Topic Conference (MTC'05), December 2005. Karachi, Pakistan.
@InProceedings{Telematik_VOGTM_2005_SOABP,
author = {Friedrich H. Vogt and Arsalan Minhas},
title = {Using Service Orientation to Drive Business Processes},
booktitle = {Proceedings of the 9th IEEE International Multi
Topic Conference (MTC'05)},
day = {13-25},
month = dec,
year = 2005,
location = {Karachi, Pakistan},
}
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.
Boris Gruschko, Friedrich H. Vogt and Simon Zambrovski. Enabling the usage of formal methods by creation of
convenient tools. In Proceedings of the 2nd International Workshop on
Web Services and Formal Methods (WSFM'05), September 2005. Versailles, France.
@InProceedings{Telematik_GVZ_2005_TLAEclipse,
author = {Boris Gruschko and Friedrich H. Vogt and Simon Zambrovski},
title = {Enabling the usage of formal methods by creation of
convenient tools},
booktitle = {Proceedings of the 2nd International Workshop on
Web Services and Formal Methods (WSFM'05)},
day = {1-3},
month = sep,
year = 2005,
location = {Versailles, France},
}
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.
Friedrich H. Vogt, Simon Zambrovski, Boris Gruschko, Peter Furness and Alastair Green. Implementing Web Service Protocols in SOA:
WS-Coordination and WS-Business Activity. In Proceedings of the 7th IEEE International
Conference on E-Commerce Technology Workshops (CEC'05), July 2005. München.
@InProceedings{Telematik_VZGFG_2005_WSCWSA,
author = {Friedrich H. Vogt and Simon Zambrovski and Boris Gruschko and Peter Furness and Alastair Green},
title = {Implementing Web Service Protocols in SOA:
WS-Coordination and WS-Business Activity},
booktitle = {Proceedings of the 7th IEEE International
Conference on E-Commerce Technology Workshops (CEC'05)},
day = {19-22},
month = jul,
year = 2005,
location = {München},
}
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.
Jurga Kazlauskaite, Arsalan Minhas and Friedrich H. Vogt. Applying Service Oriented Architecture in the Aerospace
Industry. In Proceedings of the International Mass Customization
Meeting (IMCM'05), GITO-Verlag, Berlin, June 2005. Klagenfurt, Austria.
@InProceedings{Telematik_KMV_2005_SOA,
author = {Jurga Kazlauskaite and Arsalan Minhas and Friedrich H. Vogt},
title = {Applying Service Oriented Architecture in the Aerospace
Industry},
booktitle = {Proceedings of the International Mass Customization
Meeting (IMCM'05)},
publisher = {GITO-Verlag, Berlin},
day = {2-3},
month = jun,
year = 2005,
location = {Klagenfurt, Austria},
}
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.
James E. Johnson, David E. Langworthy, Leslie Lamport and Friedrich H. Vogt. Formal Specification of a Web Services Protocol. In Proceedings of the First International Workshop on
Web Services and Formal Methods (WS-FM'04), December 2004. Pisa, Italy. Published in: Electronic Notes in Theoretical Computer
Science, Volume 105, p. 147-158, 10 December 2004.
@InProceedings{Telematik_JLLV_2004_TLA,
author = {James E. Johnson and David E. Langworthy and Leslie Lamport and Friedrich H. Vogt},
editor = {Mario Bravetti and Gianluigi Zavattaro},
title = {Formal Specification of a Web Services Protocol},
booktitle = {Proceedings of the First International Workshop on
Web Services and Formal Methods (WS-FM'04)},
month = dec,
year = 2004,
location = {Pisa, Italy},
note = {Published in: Electronic Notes in Theoretical Computer
Science, Volume 105, p. 147-158, 10 December 2004},
}
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.
U. Gröning and Friedrich H. Vogt. ZULIS - Zulieferlogistik-Informationssystem für KMU im
Flugzeugbau. In Proceedings of the 12th Hamburger
Logistik-Kolloquium, March 2003. Hamburg, Germany.
@InProceedings{Telematik_GV_2003_ZULIS,
author = {U. Gröning and Friedrich H. Vogt},
title = {ZULIS - Zulieferlogistik-Informationssystem für KMU im
Flugzeugbau},
booktitle = {Proceedings of the 12th Hamburger
Logistik-Kolloquium},
month = mar,
year = 2003,
location = {Hamburg, Germany},
}