CaberNet members involved on the project: Technische Universität Hamburg-Harburg, Germany.
Other Partners:
The Project: The autonomous development of components in service-oriented computing requires emphasising on interface specifications. The goal of the project is to investigate the automatic validation for Web Services. By automatic validation we mean the process of checking if occurring message flows conform the their specifications. It is performed by a general-purpose validator, which observes messages exchanged by communication partners and analyses the conformance to the previously read specification. This allows non-conformance to be immediately detected and corrective actions to be taken before putting risk on the systems dependability. The automatic validation can be applied to a single interface between a pair of communication partners or to the choreography of messages exchanged between several communication partners that can be part of a composite web service. Since available specification techniques for Web Services are either too restricted in their expressiveness or not well-suited for the automatic validation, a new specification technique “Specifications using XQuery expressions on Traces” (SXQT) is developed in the project. Extending the W3C’s Web Services Description Language (WSDL) message-flows are constrained in a temporal and structural manner with expressions of first order logic.
List of relevant chapters:
Service-oriented Computing
Three publications reporting outcomes from the project:
M. Venzke. Automatic Validation of Web Services. In: Proceedings of the 8th CaberNet Radicals Workshop. Hotel Eden Roc, Ajaccio, Corsica, October 5th - 8th , 2003.
M. Venzke, S. Pitzek. Accessing Fieldbus Systems via Web Services. In: Proceedings of the First Workshop on Intelligent Solutions in Embedded Systems (WISES), Vienna University of Technology, Austria, June 27th, 2003.
Network of Excellence in Distributed and Dependable Computing Systems
Acronym:
Project Title: Automatic Verification of Randomized Distributed Algorithms
Start Date: 1998
End Date: 2001
URL: http://www.cs.bham.ac.uk/~mzk/rando/
CaberNet members involved on the project: University of Birmingham, UK
Other Partners:
The Project:
This EPSRC-funded project (grant GR/M04617) is concerned with extending conventional model checking techniques to the case of randomized distributed algorithms. These are algorithms which are designed to run on hardware consisting of many interconnected processors (and often geographically `distributed', as in the case of a network of processors), and which use randomization, that is, make choices at random, using electronic coin flipping. It turns out that randomized algorithms are much faster than their deterministic counter- parts, but verifying their correctness against the specification is much more involved because of the need for sophisticated probabilistic analysis.
List of relevant chapters:
Distributed Systems Security, Rigorous Design
Three publications reporting outcomes from the project
M. Kwiatkowska, G. Norman. Verifying Randomized Byzantine Agreement. In Proc. Formal Techniques for Networked and Distributed Systems (FORTE'02), volume 2529 of LNCS, pp. 194-209, Springer-Verlag 2002
M. Kwiatkowska, G. Norman, R. Segala. Automated Verification of a Randomised Distributed Consensus Protocol Using Cadence SMV and PRISM In Proc. CAV'01, volume 2102 of LNCS, pp. 194-206, Springer-Verlag 2001
L. de Alfaro, M. Kwiatkowska, G. Norman, D. Parker, R. Segala. Symbolic Model Checking of Concurrent Probabilistic Processes using MTBDDs and the Kronecker Representation In Proc. TACAS 2000, volume 1785 of LNCS, pp. 395-410, Springer-Verlag 2000
Network of Excellence in Distributed and Dependable Computing Systems
Acronym:
Project Title: Aware Goods
Start Date: ongoing
End Date:
URL: http://www.teco.edu/~albrecht/
CaberNet members involved on the project: Universität Karlsruhe, Germany
Other Partners:
The Project:
In order to supervise goods during transport from the supplier to the consumer we are trying to introduce a small digital device with a CPU, memory and sensors on it. This device has to control the goods and the resulting measuring values are stored in the device's memory. Once arrived at the product's final destination the device will be automatically read out via infrared or any other possibly wireless communication and the data will be transferred into the consumer's backend system (quality management system/ERP system). The backend system can then check the recorded data and determine the state of the goods. If certain limits are exceeded, an alarm can be invoked and the damaged goods can instantly be returned to the supplier. This system shall offer a continuous control over the goods and a seamless integration into the existing backend systems of the suppliers as well as the consumers, following the concepts of electronic commerce. The advantage is that the error rate is much lower as no manual transferring of data is needed any more. The goods supervise themselves, which results in the term "aware goods". The measurements of digital devices are also much more accurate than those of analogous ones. This offers better control and accuracy of values to present in insurance matters. The transferring of the values is accelerated and thus costs can be reduced.
The list of relevant chapters:
Mobile Systems
Three publications reporting outcomes from the project
Network of Excellence in Distributed and Dependable Computing Systems
Acronym:
Project Title: BAE SYSTEMS Systems Integration Consortium
Start Date: 1999
End Date: ongoing
URL: http://www.baesystems.com
CaberNet members involved on the project: University of York, UK; University of Newcastle, UK
Other Partners: University of Loughborough
The Project:
This project involves collaboration between the Universities of York, Newcastle and Loughborough with BAE SYSTEMS. The work at York is targeted at software productivity improvement. This is divided into the following areas:
Automatic Software Production - This focuses upon the trusted automatic generation of high-level language from models (e.g. UML).
Object-Oriented Modelling - This focuses upon the use of UML within a systems and software engineering context. This involves meta-modelling with UML and investigation of product line architectures.
List of relevant chapters:
Dependable Systems, Real Time Systems
Three publications reporting outcomes from the project
Network of Excellence in Distributed and Dependable Computing Systems
Acronym:
Project Title: BMAN
Start Date: ongoing
End Date:
URL:
CaberNet members involved on the project: Imperial College, UK
Other Partners:
The Project:
BMAN investigates the application of mobile computation models in business processes to the configuration, management and execution of distributed workflow systems for inter-enterprise B2B e-business; new business models and best business practices, exploiting mobile systems and software for business process modelling, are under development.
List of relevant chapters:
Network and Distributed System Management
Three publications reporting outcomes from the project
Network of Excellence in Distributed and Dependable Computing Systems
Acronym:
Project Title: Deriving Authority from Security Policy
Start Date: 2002
End Date: 2003
URL: http://www.jisc.ac.uk/index.cfm?name=project_aaa_kent
CaberNet members involved on the project: University of Kent, UK
Other Partners:
Share with your friends: |