Catálogo de publicaciones - libros

Formal methods constitute a means of developing reliable and correctly behaving software based on a specification. In scenarios where information technology is used as a foundation to enable human communication, this is, however, not always enough. Successful interaction between humans often depends on the concept of trust, which is different from program correctness. In this paper, we present a framework for integrating trust into a formal development process, allowing for the construction of formally correct programs for communication, embracing trust as a central concept. We present a coordination language for use with action systems, taking a modular approach of separating trust aspects from other functionality. We also believe that our work can be adapted to modelling other aspects beside trust. Throughout the paper, we employ a case study as a testbed for our concepts.

We generalize the CRWL to the setting of the simply typed -calculus, where theories are presented by conditional overlapping fully extended pattern rewrite systems. We claim that this logic is useful for higher-order functional-logic programming, and propose a HOLN for answering joinability and reducibility queries, in which a variant of is used to efficiently control the demand-driven narrowing strategy. The calculus HOLN is shown to be sound and strongly complete with respect to this higher-order conditional rewriting logic.

We show that the class of distributed time-asynchronous automata is more expressive than timed automata, has a decidable emptiness problem, is closed under union, concatenation, star, shuffle and renaming, but not under intersection. The closure results are obtained by showing that distributed time-asynchronous automata are equivalent with a subclass of shuffle regular expressions and its related class of stopwatch automata.

Inspired by the wonderful design and implementation of the Prolog language afforded by the Warren Abstract Machine (WAM), this paper describes an extended logical language which can compute larger realms of first-order logic, based upon theories for finitary . The paper describes a language for expressing first-order geometric logic in tidy closed form, a mathematical that computes the language, and an implementation prototype that intimately mimics the abstract machine, and which also reformulates inference into inference. There are promising for geometric logic systems, collected on the website [5]. The emphasis of this paper is theory, abstract machine design and direct implementation of the abstract machine.

A logic calculus is presented that is a conservative extension of linear logic. The motivation beneath this work concerns lazy evaluation, true concurrency and interferences in proof search. The calculus includes two new connectives to deal with multisequent structures and has the cut-elimination property. Extensions are proposed that give first results concerning our objectives.

Our objective is to extend the standard results of preservation and reflection of properties by bisimulations to the coalgebraic setting, as well as to study under what conditions these results hold for simulations. The notion of bisimulation is the classical one, while for simulations we use that proposed by Hughes and Jacobs. As for properties, we start by using a generalization of linear temporal logic to arbitrary coalgebras suggested by Jacobs, and then an extension by Kurtz which includes atomic propositions too.

A variant of -calculus which can flexibly and dynamically control process modularity is presented. The calculus is equipped with a two level structure to represent process distribution and mobility over flat locations. It provides a suitable model for modular programming in concurrent and mobile computing. Several bisimulation relations are discussed, and a notion of bisimulation-preorder is proposed to reflect some aspects of mobile distributed computing such as interaction costs.

This paper introduces the concept of a ‘structured occurrence net’, which as its name indicates is based on that of an ‘occurrence net’, a well-established formalism for an abstract record that represents causality and concurrency information concerning a single execution of a system. Structured occurrence nets consist of multiple occurrence nets, associated together by means of various types of relationship, and are intended for recording either the actual behaviour of complex systems as they interact and evolve, or evidence that is being gathered and analyzed concerning their alleged past behaviour. We provide a formal basis for the new formalism and show how it can be used to gain better understanding of complex fault-error-failure chains (i) among co-existing interacting systems, (ii) between systems and their sub-systems, and (iii) involving systems that are controlling, supporting, creating or modifying other systems. We then go on to discuss how, perhaps using extended versions of existing tools, structured occurrence nets could form a basis for improved techniques of system failure prevention and analysis.

() is a foundational language for Service Oriented Computing that combines in an original way a number of ingredients borrowed from well-known process calculi, e.g. asynchronous communication, polyadic synchronization, pattern matching, protection, delimited receiving and killing activities, while resulting different from any of them. In this paper, we extend with timed orchestration constructs, this way we obtain a language capable of completely formalizing the semantics of , the ‘de facto’ standard language for orchestration of web services. We present the semantics of the extended language and illustrate its peculiarities and expressiveness by means of several examples.

We present regular linear temporal logic (RLTL), a logic that generalizes linear temporal logic with the ability to use regular expressions arbitrarily as sub-expressions. Every LTL operator can be defined as a context in regular linear temporal logic. This implies that there is a (linear) translation from LTL to RLTL.

Unlike LTL, regular linear temporal logic can define all -regular languages, while still keeping the satisfiability problem in PSPACE. Unlike the extended temporal logics , RLTL is defined with an algebraic signature. In contrast to the linear time -calculus, RLTL does not depend on fix-points in its syntax.