FLACOS 2007
  First Workshop on Formal Languages and Analysis of Contract-Oriented Software
Oslo, October 9-10, 2007

ABSTRACTS OF INVITED PARTICPANTS' TALKS

• Gilles Barthe (INRIA Sophia-Antipolis, France)
  See the NWPT page
  
  
• Frank S. de Boer (CWI, The Netherlands)
  Task Scheduling for Actors
  Abstract:
      I will show how to use the formalism of task automata for representing both the real-time output behavior of the provided methods of an actor and the real-time behavior of its environment. These task automata are timed automata with labels consisting of a method call and an associated deadline. The incoming methods are stored in the queue of an actor according to a particular scheduling policy (e.g., shortest deadline first). Given a scheduling policy I will show how we can construct again a task automata which represents the real-time interaction between an actor and its environment. This automata serves as the basis for the schedulability analysis and the compatibility check of the environmental assumptions of the different actors in a system.
  
  
• Emilia Cambronero Piqueras (University of Castilla-La Mancha, Spain)
  WST: A Tool for Verifying Web Services systems
  Abstract:
      In this paper we introduce a tool called Web Service Translation tool, WST for short, which we are developing to support a model-driven methodology, intended to the analysis, design, implementation, validation and verification of Web Services with time restrictions, called Correct-WS methodology. This methodology works by making several translations, from phase to phase in the life cycle. An important feature of this methodology is that at each phase the system is represented by XML models. Then, we use XSL Transformations (XSLT), which is a language for transforming XML documents.
      The purpose of these translations is to obtain Web Services description models with Timed Automata for validating and verificating Web Services with time restrictions. For that, we use UPPAAL tool, which is used to simulate and analyse the behavior of Real-Time Systems described by Timed Automata.
  
  
• Giuseppe Castagna (University of Paris 7, France)
  A Theory of Contracts for Web Services
  (by Giuseppe Castagna, Nils Gesbert and Luca Padovani)
  Abstract:
      Contracts are behavioural descriptions of Web services. We devise a theory of contracts that formalises the compatibility of a client to a service, and the safe replacement of a service with another service. The use of contracts statically ensures the successful completion of every possible interaction between compatible clients and services. The technical device that underlies the theory is the definition of "filters", which are explicit coercions that prevent some possible behaviours of services and, in doing so, they make services compatible with different usage scenarios.
      We show that filters can be seen as proofs of a sound and complete subcontracting deduction system which simultaneously refines and extends Hennessy's classical axiomatisation of the must testing preorder. The relation is decidable and the decision algorithm is obtained via a cut-elimination process that proves the coherence of subcontracting as a logical system. Despite the richness of the technical development, the resulting approach is based on simple ideas and basic intuitions. Remarkably, its application is mostly independent of the language used to program the services or the clients. We also outline the possible practical impact of such a work and the perspectives of future research it opens.
  
  
• Jean-Marc Eber (LexiFi, France)
  Applications of a Formal Contract Description Language to the Investment Banking Domain
  Abstract:
      In our presentation, we firstly introduce the audience to the particular domain we are addressing, namely investment banking financial problems. After a quick presentation of the typical problems encountered by this industry when manipulating complex financial contracts, we show the practical benefits of a clearly defined operational semantics. We then give some intuition for understanding the problem of pricing complex contracts, a fundamental problem in this industry. We show that even if many different pricing models appear in the finance theory literature, a unified approach is indeed possible, and can be interpreted as a denotational semantics of our contract description language.
      Our company, LexiFi, has developed an industrial solution around these ideas, mostly implemented as an application around a core library implemented in OCaml. We will present some typical usage examples, showing the combined use of LexiFi's pricing compiler and contract management engine. We emphasize the importance of some implementation details (for instance run-time code generation and partial evaluation) to achieve good run-time efficiency.
      We present some user experience and discuss typical pitfalls to avoid. We also want to discuss with the audience future research and development directions for manipulating contracts.
  
  
• Fritz Henglein (DIKU, Denmark)
  Compositional contract specification for REA
  Abstract:
      We present a declarative language for compositional specification of contracts governing the exchange of resources. It extends Eber and Peyton Jones's declarative language for specifying financial contracts to the exchange of money, goods and services amongst multiple parties, and it complements McCarthy's Resources, Events and Agents (REA) accounting model with a view-independent formal contract model that supports definition of user-defined contracts, automatic monitoring under execution, and user-definable analysis of their state before, during and after execution. A variety of (real) contracts can be expressed in such a fashion as to support their integration, management and analysis in an event-driven architecture. As part of ongoing work the language is expected to evolve into a core component of a process-oriented software architecture for next-generation ERP systems within the 3gERP Project (3gERP.org).
  
  Joint work with Jesper Andersen, Ebbe Elsborg, Jakob Grue Simonsen and
  Christian Stefansen.  (Contract language previously presented at ISoLA
  2004, published in STTT 2006).
  
  
• Martin Leucker (Technische Universitat Munchen, Germany)
  Monitor-based Runtime Reflection
  (by Martin Leucker and Christian Schallhart )
  Abstract:
      In this paper, we give an overview on the concepts of runtime verification, monitor-oriented programming, and monitor-based runtime reflection. Runtime verification is mainly concerned with monitoring a (correctness) property at runtime, i.e. when executing a system. Monitor-oriented programming aims at a programming methodology that allows for the execution of code whenever monitors observe a violation of a given correctness property. Runtime reflection is an architecture pattern that is applicable for systems in which monitors are enriched with a diagnosis and reconfiguration phase. We briefly discuss their use in contract enforcement.
  
  
• Fabio Massacci (University of Trento, Italy)
  A Security-by-Contracts Architecture for Pervasive Services
  Abstract:
      Future pervasive environments will by characterised by pervasive client downloads: new (untrusted) clients will be dynamically downloaded in order to exploit the computational power of the nomadic devices to make a better use of the services available in the environment. To address the challenges of this paradigm we propose the notion of security-by-contract (SxC), as in programming-by-contract, based on the notion of a mobile contract that a pervasive download carries with itself. It describes the relevant security features of the application and the relevant security interactions with its nomadic host. In this paper we describe the layered security architecture of the SxC paradigm for pervasive security, the threats and mitigation strategies of security services and sketch some interaction modalities of the security services layer.
  
  
• John-Jules Ch. Meyer (Utrecht University, The Netherlands)
  Delegation Contracts in Autonomous Robotic Mission Scenarios
  Abstract:
      I'll stetch ongoing work with Patrick Doherty (Linkoeping) on how to employ delegation contracts in the context of scenarios with autonomous robotic missions involving UAVs, where mixed initiative and adjustable autonomy are called for. In this work we start out from theoretical work on delegation by Castelfranchi & Falcone. On the one hand we underpin this semi-formal theory with the formal agent logic KARO, on the other hand we consider how to employ this in agent programming and particularly its use in the very practical context mentioned above.
  
  
• Ralf Reussner (University Karlsruhe, Germany)
  Parametric Contracts for Software Components
  Abstract:
      This talk discusses the role of software components for an engineering approach to software construction. In particular, this talk concentrates on the automated adaptation of software components and predicting extra-functional properties of layered component-based software architectures. The approach presented is based on parametric contracts, a generalisation of design-by-contract. Firstly, the talks discusses the role of component-based software engineering plays for software engineering in general. Secondly, we adresses the meaning of the "contractual use of components", a term sometimes used loosely - or even inconsistently - in current literature. Thirdly, we introduce the abstract concept of parametric contracts. It is shown how parameterised contracts are used to compute quality properties of a component in dependence from its environment.
  
  
• Marek Sergot (Imperial College, UK)
  On the formal representation of contracts: verification and execution monitoring
  Abstract:
      We describe the main elements of a project we have recently started on the formal representation of contracts and the business processes within which they are enacted, outlining the motivation, technical objectives, and preliminary work completed so far. Our aim is to integrate and then build upon three separate strands of previous work: (1) the use of the event calculus for tracking the evolving state of a contract as it is enacted;   (2) executable specifications of `open agent societies', for which we have used both the event calculus as well as action languages from AI (specifically the language C+); and (3) symbolic model checking techniques for the verification of normative and temporal epistemic properties of multi-agent systems, and their application to the formal modelling of web service compositions. We want to support both (1) run-time monitoring of contract execution and implementation of the enabling infrastructure (e.g., web services), and (2) off-line (design-time) verification of contract and system properties. For illustration we will present one of the examples we are using to drive the development.
      It concerns a contract for the production and phased delivery of a complex artefact comprising several components (in the actual example, a large software product commissioned and specified by the client). The contract specifies an agreed schedule of monitoring and progress report points, delivery milestones for the various phases of the project, and mechanisms allowing the parties to request changes to the specification or cancellations and modifications of a complete sub-component. The emphasis in the example (as in many other examples of contracts) is not so much on obligations and sanctions, which are relevant but comparatively peripheral, but rather on detailing the terms under which the delivered product is to be regarded as meeting its specification, and the powers and procedures by means of which changes to the specification are requested, approved, and effected.
  
  
• Isabelle Simplot-Ryl (University of Lille 1, France)
  Contracts as a support to static analysis of open systems
  Authors: Nadia Bel Hadj Aissa, Dorina Ghindici, Gilles Grimaud, Isabelle Simplot-Ryl
  Abstract:
      Static analysis is a powerful tool to establish various properties of programs. The analysis is often directed by the call graph of the programs and thus is not well suited to open object-oriented systems. In this work in progress, we introduce the notion of contract as a support to openness and extensibility: we propose an analysis computing the contract of a method relying on contracts of methods used by it. Thus the analysis is compositional the properties of composed code can be deduced from contract composition.
      We give two examples of applications in the context of open object-oriented systems and dynamical loading of applications: one for a distributed WCET computation method for small embedded systems and one for a dependency calculus on Java programs. These examples allow us to present two types of contracts: the contracts that are introduced by the designer of the system, and the contracts that are automatically computed by the analysis with regard to the first ones.
  
  
• Valentin Valero Ruiz (University of Castilla-La Mancha, Spain)
  Transforming Web Services Choreographies with Priorities and Time Constraints Into Prioritized-Time Petri Nets
  Abstract:
      A Web Service is a self-describing, self-contained modular application that can be published, located, and invoked over a network, e.g. the Internet. Web Services composition provides a way to obtain value-added services by combining several Web Services. Then, the composition of Web Services is suitable to support enterprise application integration. WS-CDL (Web Services Choreography Description Language) is a W3C candidate recommendation for the description of peer-to-peer collaboration for the participants in a Web Services composition. In this paper we focus our attention on the timed aspects of WS-CDL, as well as in the collaborations that require some kind of priorization. Then, our goal is to provide a WS-CDL definition of prioritized collaborations and a semantics for them by means of timed Petri nets.
  
  

---

Last modified, 6 September 2007.