Software integration needs to face various kinds of incompatibilities that unavoidably arise when composing services developed by different parties. To overcome signature, behaviour, or security mismatches, various techniques supporting flexible and non-intrusive service adaptation have been developed. In this talk, we will first exemplify the problems and the potential of behaviour adaptation, also when in adverse conditions. We will then try to discuss some of the general issues involved in service adaptation, such as dynamicity, correctness, cross-layerness, and cost.
Short Biography: Antonio Brogi, Ph.D., is full professor at the Department of Computer Science of the University of Pisa. His research interests include service-oriented computing, coordination and adaptation of software elements, formal methods and design of programming languages. He has published the results of his research in over 140 papers in international journals and conferences. He is currently member of the editorial board of the journals "Advances in Computer Science and Engineering", "Computer Languages, Systems and Structures", and "International Journal of Web Science", of the steering committee of the CIbSE, ESOCC, FLACOS, and FOCLASA conference series, and he has participated in the program committee of various international conferences in his areas of research. He has been participating as project or site leader in various international research projects. He spent one year as visiting professor at UCLA (USA) and he has spent invited research stays in Spain, Portugal and Peru.
Many efforts have been devoted in the computer science community to "a priori" verifications of properties of IT systems. In many situations however, properties cannot be controlled or imposed a priori. This can be the case for a variety of reasons: certain actions can be out of control of a given system (they may depend on other systems or on human beings), the compliance property itself may be impossible to check on the fly (it can depend on contextual information or on future events) or it may just be too cumbersome to impose a priori verifications in practice. Typical illustrations of this situation are the compliance with privacy or intellectual property protection rules, or the verification of Service Level Agreement commitments for on-line services. Accountability is an attractive alternative that relies on "a posteriori" controls to check that a system has complied with the rules. Accountability has been studied in a variety of contexts such as politics, sociology, ethics, law and also computer science, sometimes with slightly different meanings. But accountability also raises challenges that should not be underestimated. In this talk, we will review the definitions of accountability and their relationships with the notions of responsibility and liability. We will identify the main challenges raised by accountability and argue that it should not be taken for granted but should result from a deliberate "accountability by design approach".
C-O Diagrams have been introduced as a means to have a visual representation of normative texts and electronic contracts, where it is possible to represent the obligations, permissions and prohibitions of the different signatories, as well as what are the penalties in case of not fulfillment of their obligations and prohibitions. In such diagrams we are also able to represent absolute and relative timing constrains. In this paper we consider a formal semantics for C-O Diagrams based on a network of time automata and we present several relations to check the consistency of a contract in terms of realizability, to analyze whether an implementation satisfies the requirements defined on its contract, and to compare several implementations using the executed permissions as criteria.
This article deals with the interrelation of deontic operators in contracts – an aspect often neglected when considering only one of the involved parties. On top of an automata-based semantics we formalise the onuses that obligations, permissions and prohibitions on one party impose on the other. Such formalisation allows for a clean notion of contract strictness and a derived notion of contract conflict that is enriched with issues arising from party interdependence.
We develop a theory of contracting systems, where behavioural contracts may be violated by dishonest participants after they have been agreed upon - unlike in traditional approaches based on behavioural types.
We consider a generic contract model, and we embed it in a calculus that allows distributed participants to advertise contracts, reach agreements, and realise them (or choose not to). We highlight some research directions about the problem of determining the honesty of participants.
Contract conformance is hard to determine statically, prior to the deployment of large pieces of software. A scalable alternative is to monitor for contract violations post-deployment: once a violation is detected, the trace characterising the offending execution is analysed to pinpoint the source of the offense. A major drawback with this technique is that, often, contract violations take time to surface, resulting in long traces that are hard to analyse. In this paper proposes a methodology and presents an accompanying tool for simplifying traces thus assisting contract-violation debugging.
The approaches based on the notions of a contract and contract-based development (e.g., design-by-contract programming) are steadily gaining popularity in software engineering. Traditionally, contracts are used as static formal annotations of a particular component that can be referred while validating or verifying the design and functionality of the overall system. In this presentation, we will offer a slightly different take on the notion of contracts, making them a part of the dynamic system state. In our representation of a component system, components can dynamically engage into and disengage from different contracts, each of which defines possible activities of several involved components. Moreover, since active contracts are a part of the dynamic system state, contract definitions can directly refer to other contracts a particular contract component may be required to be involved in. The presentation will briefly describe a formalisation of dynamic contracts as well as give some examples of such contracts.
This paper describes a way to formally specify the behaviour of concurrent data structures. When specifying concurrent data structures, the main challenge is to make specifications stable, i.e., to ensure that they cannot be invalidated by other threads. To this end, we propose to use history-based specifications: instead of describing method behaviour in terms of the object’s state, we specify it in terms of the object’s state history. A history is defined as a list of state updates, which at all points can be related to the actual object’s state.
We illustrate the approach on the BlockingQueue hierarchy from the java.util.concurrent library. We show how the behaviour of the interface BlockingQueue is specified, leaving a few decisions open to descendant classes. The classes implementing the interface correctly inherit the specifications. As a specification language, we use a combination of JML and permission-based separation logic, including abstract predicates. This results in an abstract, modular and natural way to specify the behaviour of concurrent queues. The specifications can be used to derive high-level properties about queues, for example to show that the order of elements is preserved. Moreover, the approach can be easily adapted to other concurrent data structures.
Our aim is to detect whether texts written in natural language contain normative conflicts (i.e., whether there are conflicting obligations, permissions and prohibitions). We present AnaCon, a framework where such texts are written in a Controlled Natural Language (CNL) and automatically translated into the formal language CL using the Grammatical Framework (GF). In AnaCon such CL expressions are analyzed for normative conflicts by the tool CLAN which gives a counter-example in case a conflict is found. We also discuss the practicality of the approach, and give a short overview on the research challenges and future directions in the area.
Web services managing distributed resources is a technology that allows the user to have an easier and cheaper mechanism to access and manage distributed resources. The formal modeling of web services with distributed resources thus becomes very important in order to understand accuratelytheir behavior. In this paper, we present a framework to model web services with distributed resources by using a widely adopted standard (UML 2.0), enriched with resource management capabilities, on the basis on a standard for the management of distributed resources, WSRF.
The talk takes outset in and discuss how to combine work presented as a poster at DEBS 2012 joint with Zanitti in the Genie project and work presented in a paper at FHIES 2012 joint with Henriksen, Nielsen, Yoshida and Henglein in the Trustworthy Pervasive Healthcare Services (TrustCare) project.
In the DEBS 2012 poster we propose a declarative, Process-oriented Event-based Programming Language (PEPL) aimed at pervasive, context-sensitive workflow management and process-oriented systems.
In the FHIES 2012 paper we propose a new theory of multiparty session types extended with propositional assertions and symmetric sum types for modeling collaborative distributed workflows. Multiparty session types statically guarantee that workflows are type-safe and deadlock-free, facilitate automatic generation of participant-specific (local) workflow protocols from global descriptions, and support flexible implementation of local workflows guaranteed to be compliant with the (global) workflow protocols. The extensions with assertions and symmetric sum types support expressing state-based (pre)conditions and consensual multiparty synchronisation, which are common in complex distributed workflows.
We have demonstrated in the FHIES 2012 paper the theory's applicability to clinical practice guidelines (CPGs) by a prototype implementation targeting mobile healthcare applications. The prototype compiles declarative healthcare workflows specified in a flexible spreadsheet-formatted process matrix into type-checked multiparty processes, which are subsequently interpreted on a server. The interpreter provides interface hooks for access by mobile clients. For demonstration purposes we have implemented a role-tailored graphical user interface (GUI) running on Android tablet computers, which reflects the pervasiveness requirements common to clinical and home healthcare scenarios. A physician has, with little prior training, successfully used the prototype to design her own healthcare workflow as a process matrix, employing instantaneous test and usage feedback from the automatically generated client.
In the talk we discuss the possibilities of using the PEPL language as source language in place of the spreadsheet-formattet process matrix.