|
|
|
FLACOS 2009 Third Workshop on Formal Languages and Analysis of Contract-Oriented Software Toledo, Spain, September 24-25, 2009 University of Castilla-La Mancha, Department of Computer Science Real-Time and Concurrent Systems Research Group  |
|
Invited Talks
Accepted Papers
Other Talks
Abstracts
Evolution of contracts Any formalism to describe contracts must be able to capture evolvability over time, and also to correlate such evolutions to changes in the environment or in the behavior of the parties involved in contracts. Yet, few works have focused on the general problem of verifying evolvable contracts. The talk will show that verification techniques for static contracts naturally extend to evolvable contracts. Starting from a very general view of contracts as syntactic entities that characterize sets of traces, we show how to accomodate two essential ingredients of dynamic contracts: spillover, which characterizes the remains of a clause when it is withdrawn from a contract, and power, which characterizes when a principal is entitled to perform a change in a contract. Then, we show that standard definitions of offline and online monitoring extend to dynamic contracts, and we prove that the standard criteria of soundness and completeness of online monitoring wrt offline monitoring remain applicable for dynamic contracts. One useful consequence of our results is the possibility of relying on online methods to ensure that power is used correctly. Although the technical development is carried in an abstract setting, we illustrate our definitions and results using contract languages for rights and obligations; these languages, despite their simplicity, share many essential features with other formalisms for digital right management and access control, and are therefore representative of the potential interest of our approach.
Automated Service Creation The talk covers what we are doing at SICS in the project 'Goal-oriented policies for self-management' (GOPS), which is about bridging the gap between business level goals and network configuration policies that currently impedes the creation of complex telecom services. I'll focus on our first paper (DAMNS 2008) which outlines the architecture of a new type of network elements (Autonomic Entities) that are supposed to be able both to refine and combine goals and to orchestrate complex services. I'll also present some of the more recent developments in GOPS, including the communication between autonomic entities, goal refinement, and goal composition.
On Behavioural Interfaces and Contracts for Software Adaptation Software Adaptation aims at composing in a non-intrusive way black-box components or services, even if they present some mismatches in their interfaces. Adaptation is a complex issue especially when behavioural descriptions of services are taken into account in their interfaces. In this paper, we first present our abstract notations used to specify behavioural interfaces and adaptation contracts, and propose some solutions to support the specification of these contracts. Then, we overview our techniques for the generation of centralized or distributed adaptor protocols and code based on the aforementioned contracts.
Runtime monitoring of contract regulated web services We investigate the problem of locally monitoring contract reg- ulated behaviours in web services. We encode contract clauses in service specifications by using extended timed automata. We propose a non intrusive local monitoring framework along with an API to monitor the fulfilment (or violation) of contractual obligations. A key feature of the framework is that it is logic-based and fully symbolic thereby providing a scalable solution to monitoring. At runtime execution steps generated by the service are passed as input to the runtime monitor. In our imple- mentation snapshots are taken from runtime execution traces generated by services and are passed as input to the runtime monitoring framework. Conformance of the execution against the service specification is checked using a symbolically represented extended timed automaton. This allows us to monitor service behaviours over large state spaces generated by mul- tiple, long running contracts. We illustrate our methodology by monitoring a service composition scenario from the vehicle repair domain, and report on the experimental results.
Towards a Rigorous IT Security Engineering Discipline Current practices for developing secure systems are still closer to art than to an engineering discipline. Security is still treated too frequently as an add-on and is therefore not integrated into IT systems development practices and tools. Experienced security artisans continue to be the key for achieving acceptable levels of security in IT systems. In this situation we could safely state that security engineering is a hype. In fact, the term security engineering has been used to denote partial approaches that cover only small parts of the processes that are required in order to create a secure system, like modelling, verification, programming, etc. Moreover, one finds in the literature that the main books about security engineering describe threat-based engineering approaches. The main drawbacks of these approaches is that they fail to provide a reasonable level of support for systematic engineering since the identification, characterization and specification of the requirements (frequently based on avoiding threats) as well as the selection of appropriate mechanisms and countermeasures depends on the experience of the engineers. Consequently, these approaches are inherently opposed to what an engineering discipline should be and represent only minor improvements over the security art. This paper discusses this vision and advocates a change of paradigm based on rigour and precision. In particular, the paper presents an approach based on the precise and formal specification of both security requirements and security solutions as the basis for the engineering of secure systems and discusses the role of contracts in security engineering.
Visual Specification of Timed Contracts In the Web Services context, a contract specifies not only how services should behave, but also the restrictions that these services must fulfill, such as time constraints. We describe a visual model that allows users to model formal contracts in a user friendly way, by means of a two-layer structure: the goal model layer, whose goals represent the contract clauses, and the formal model layer, that formally specifies the behavior corresponding to the goal model, including the restrictions defined.
Models for Open Transactions Loosely coupled interactions permeate modern distributed systems, where autonomous applications need to collaborate by dynamical assembly. We can single out three different phases occurring in every collaboration: 1) negotiation of some sort of contracts, mediating the needs of prospective participants; 2) acceptance or rejection of the contract; 3) contract-guarantee execution. The above scheme, called NCE for short (Negotiation, Commit, Execution), covers a wide range of situations, ranging from sessions and transactions to proof-carrying code. In the paper we concentrate on the notion of open transaction and on Zero-Safe Nets, a model developed by the authors for modelling long transactions. We extend the latter to cover the three-phase process above.
Analyzing Service Contract with Model Checking This presentation gives an overview of an ongoing work which investigates tool support for analysis of SOA-based service contracts using Model Checking. The specification language for the contract is Business Process Execution Language (BPEL). It captures the behavior of services and allows developers to compose services without dependence on any particular implementation technology. A behavior specification is extracted from a BPEL program for formal analysis. One of the key conditions is that the extracted behavior should reflect the intended semantics for BPEL, and in order to make it comprehensible, it is specified in a functional language. The resulting tool suite will be hosted on an Eclipse platform.
From Orchestration to Choreography: Memoryless and Distributed Orchestrators In the context of Web services, making client and service interact so as to satisfy the client, that is, making the service compliant with the client, can be done using either orchestration or choreography. In this paper we propose to build, whenever possible, memoryless orchestrators, and then distribute them using protocols so as to obtain choreographies. When necessary for guaranteeing compliance, we infer from the initial (sequential) transition system possible concurrency between certain interactions, whose validity must be checked by the designer. Our approach allows for a clear distinction between the design phase and the implementation phase while being, in the general case, more efficient than orchestration. An example dealing with resource management illustrates the usefulness of memoryless orchestrators. We also discuss a methodology allowing contract-based design and verification of Web services at a higher level of abstraction.
COSoDIS as it is A summary of what we have accomplished during the three years of the project: An investigation of high level contract specification with deontic modalities, some steps towards analysing protocols for service programming languages WS-BPEL and WS-CDL. And the open questions which needs further thought: What are the overall healthiness conditions for a service - or what is the beauty of a service? Is compensation just going to be the well-known transaction mechanism in a distributed setting? Are services components in the Cloud?
Passages retrieval and intellectual property in legal texts. Question answering (QA) can be viewed as a particular form of information retrieval (IR), in which the amount of information you want to find is the minimum amount information required to satisfy the user needs expressed by a specific question. A passage retrieval system (PR) is an IR system which returns part of texts (passages) that are relevant to the user needs. JIRS is a free use PR system developed at the Universidad Politécnica de Valencia. The PR system is independent of the language, as it is based on n-grams structure. This paper shows the experiments made in the ambit of passage retrieval and the intellectual property on the legal text, in the collaboration framework of the Natural Language Engineering Lab. Of the Universidad Politécnica de Valencia with the Maat Knowlegde Company; it is based on JIRS tool for the ResPubliQA and IP tracks at the ClEF-2009.
Service Inter-Dependency in the Action System Formalism With the ubiquity of computing devices, information sources become increasingly distributed and is provided by scattered independent entities. Commonly, the providing entities can be called services. A service might collect several sources’ information and deduce new information out of these. Whether being an intermediate service or elementary source of information, the service provided need to be considered as a black-box from the utilising system’s point of view, i.e. as components. Moreover, the utilising system might depend on this information and halt until it is available. In order to master the distribution of information sources, we long a method to integrate the services to the utilising specification and a means to in a systematic way formally model the dependencies of these services. In order to achieve this, we need to define a formal construct for dependency. We have chosen to model the dependency in the action system formalism framework. We use reactive action systems as they provide means for reasoning about the information in a service-like distributed manner. The focus is on examining the consequences to the action system when applying uni- and bidirectional dependencies. Refining the systems will also be considered. However, as refinement is about preserving correctness on mathematical foundations, it is restricted to the algorithmic part and thereby, refinement is not directly applicable on physical or logical dependencies. This talk will introduce the methods and operators needed to describe dependencies. Initially, they are implemented on one system for sheer comprehensibility, and only later shown how they can be applied on several possibly inter-dependent action systems.
A Contract-Based Approach to Adaptability in User-Centric Pervasive Applications Pervasive user-centric applications operate in highly dynamic and uncertain environments. Designing such applications as one monolithic component taking all possible environments into account inevitably leads to bad system design. We instead propose constructing partial solutions handling only a subset of all possible environments, and changing the system as the environment evolves. We use an assume-guarantee contract framework to infer the conditions under which configurations exhibit the desired functionality. Furthermore, we show how a system undergoing reconfigurations can be shown to satisfy a global assume-guarantee contract. |