Catálogo de publicaciones - libros

In this paper we propose a formal language for writing electronic contracts, based on the deontic notions of obligation, permission, and prohibition. We take an ought-to-do approach, where deontic operators are applied to actions instead of state-of-affairs. We propose an extension of the -calculus in order to capture the intuitive meaning of the deontic notions and to express concurrent actions. We provide a translation of the contract language into the logic, the semantics of which faithfully captures the meaning of obligation, permission and prohibition. We also show how our language captures most of the intuitive desirable properties of electronic contracts, as well as how it avoids most of the classical paradoxes of deontic logic. We finally show its applicability on a contract example.

In this paper we present a formalization of Abadi’s and Cardelli’s theory of objects in the interactive theorem prover Isabelle/ HOL. Our motivation is to build a mechanized HOL-framework for the analysis of a functional calculus for distributed objects. In particular, we present (a) a formal model of objects and its operational semantics based on de Bruijn indices (b) a parallel reduction relation for objects (c) the proof of confluence for the theory of objects reusing Nipkow’s HOL-framework for the lambda calculus. We expect this framework to be highly reusable and allow further development and mechanized proofs of various aspects of object theory, e.g., distribution, aspect orientation, typing.

The Pict programming language is an implementation of the -calculus in which executions of -calculus terms are specified via an abstract machine. An important property of any concurrent programming language implementation is the fair execution of threads. After defining fairness for the -calculus, we show that Pict abstract machine executions implement fair -calculus executions. We also give new proofs of soundness and liveness for the Pict abstract machine.

We present a refinement method for Java programs which is motivated by the challenge of verifying security protocol implementations. The method can be used for stepwise refinement of abstract specifications down to the level of code running in the real application. The approach is based on a calculus for the verification of Java programs for the concrete level and Abstract State Machines for the abstract level. In this paper we illustrate our method by the verification of a M-Commerce application for buying movie tickets using a mobile phone written in J2ME. For verification we use KIV, our interactive theorem prover [1].

Refactoring is a method for improving the structure of programs/specifications as to enhance readability, modularity and reusability. Refactorings are required to be in that – to an external observer – no difference between the program before and after refactoring is visible. In this paper, we develop refactorings for an object-oriented specification formalism combining a state-based language (Object-Z) with a process algebra (CSP). In contrast to OO-programming languages, refactorings moving methods or attributes up and down the class hierarchy, in addition, need to change . We formally prove behaviour preservation with respect to the failures-divergences model of CSP.

In this paper we discuss an assertional proof method for multi-threaded Java programs. The method extends the proof theory for sequential Java programs with a generalization of the Owicki/Gries interference freedom test to threads in Java.

The behavior of a Web service can be described by means of a contract, which is a specification of the legal interactions with the service. Given a repository of Web services, from the client viewpoint a proper service selection should be based on functional as well as non-functional aspects of the interactions. In this paper we provide a technique that enables a client both to discover compatible services and to compare them on the basis of specific performance requirements. Our technique, which is illustrated on a simple probabilistic calculus, relies on two families of client-specific probabilistic testing preorders. These are shown to be precongruences with respect to the operators of the language and not to collapse into equivalences unlike some more general probabilistic testing preorders appeared in the literature.

We present a novel approach, based on probabilistic formal methods, to developing cross-layer resource optimization policies for resource limited distributed systems. One objective of this approach is to enable system designers to analyze designs in order to study design tradeoffs and predict the possible property violations as the system evolves dynamically over time. Specifically, an executable formal specification is developed for each layer under consideration (for example, application, middleware, operating system). The formal specification is then analyzed using statistical model checking and statistical quantitative analysis, to determine the impact of various resource management policies for achieving desired end-to-end QoS properties. We describe how existing statistical approaches have been adapted and improved to provide analyses of given cross-layered optimization policies with quantifiable confidence. The ideas are tested in a multi-mode multi-media case study. Experiments from both theoretical analysis and Monte-Carlo simulation followed by statistical analyses demonstrate the applicability of this approach to the design of resource-limited distributed systems.

In this paper we introduce a formal model for reasoning about resource sensitive timed component connectors. We extended the constraint automata model, which is used as the semantic model for the exogenous channel-based coordination language Reo, through integrating both resource and time information. This model allows to specify both the interactions that take time to be performed and timeouts. Moreover, the model reflects resource issues, such as bandwidth or allocated memory, that may affect the time needed for interactions when specifying the timed behavior of connectors. The time duration that an interaction takes is represented by a function on the available resources. In addition to the formalism, we also discuss compositional reasoning and present two notions of simulation to relate different connectors from functional and resource-sensitive temporal perspectives respectively.