| Joël Ouaknine. Some Recent Results in Metric Temporal Logic |
| Abstract: Metric Temporal Logic (MTL) is a widely-studied real-time extension of Linear Temporal Logic. In this paper we survey results about the complexity of the satisfiability and model checking problems for fragments of MTL with respect to different semantic models. We show that these fragments have widely differing complexities: from polynomial space to non-primitive recursive and even undecidable. However we show that the most commonly occurring real-time properties, such as invariance and bounded response, can be expressed in fragments of MTL for which model checking, if not satisfiability, can be decided in polynomial or exponential space. |
| Albert Benveniste. Composing Web Services in an open world: Issues of Quality of Service |
| Abstract: Orchestrating Web
services has become the method of choice for building new services on
top of existing ones. One area of interest for this technology is
business processes. Languages and methods have been developed and are
now getting widely used, BPEL being the typical instance. When
exposing the profile of a Web service, Quality of Service (QoS) must be
specified. Besides security aspects, QoS involves a variety of
parameters related to performance, query throughput, as well as
quality of the returned data. How should QoS be handled in this
context of Web Services Orchestrations? A number of novel and not so
well identified issues occur that make this topic deviating from QoS
for networks in a substantial way.
Firstly, since Web services aim at hiding details for the external world, no information regarding the infrastructure or resources supporting a Web service is generally exposed. This prevents from using classical resource based performance models. Contracts are preferred instead. Contracts expose what a service offers, in terms of both function and QoS; in turn, contracts may or may not assume certain constraints on how the service should be invoked. A second important feature is that, unlike in networks, the control in orches- trations may depend on the carried data. Consequently performance and data interfere, which can cause orchestrations to become non-monotonic with respect to QoS—improving the QoS of some called service may degrade the overall QoS of the orchestration. Unfortunately, relying on QoS contracts implicitly assumes monotonicity. In a contract-based framework, a central question is to relate the contract that the orchestration can offer to its customers, to the contracts it has established with its subcontractors regarding the called services. This is not so simple when dealing with Web Services Orchestrations because actual QoS parameters vary a lot for different calls and are better described by means of a probability distribution. I shall discuss probabilistic soft contracts and how to compose them. Such contracts must be monitored by the orchestration for possible violations. I shall advocate using testing techniques from statistics for this purpose. Orchestration reconfiguration (e.g., to cope with breaching) is another important issue that is beyond the scope of my presentation, however. |
| Jiri Srba. Comparing the Expressiveness of Timed Automata and Timed Extensions of Petri Nets |
| Abstract: Time dependant models have been intensively studied for many reasons, among others because of their applications in software verification and due to the development of embedded platforms where reliability and safety depend to a large extent on the time features. Many of the time dependant models were suggested as real-time extensions of several well-known untimed models. The most studied formalisms include Networks of Timed Automata which extend the model of communicat- ing finite-state machines with a finite number of real-valued clocks, and timed extensions of Petri nets where the added time constructs include e.g. time intervals that are assigned to the transitions (Time Petri Nets) or to the arcs (Timed-Arc Petri Nets). In this paper, we shall semi-formally introduce these models, discuss their strengths and weaknesses, and provide an overview of the known results about the relationships among the models. |