Catálogo de publicaciones - libros

By a domain we mean a universe of discourse.

Typical examples are (partially) man-made universes of discourse - such as Air Traffic, Airports, Financial Services (banks, insurance companies, securities trading [brokers, traders, stock exchanges]), Health Care (hospitals etc.), Secure IT Systems (according to Intl. ISO/IEC Standard 17799), The Market (consumers, retailers, wholesalers, producers, “the supply chain”), Transportation (road, air, sea and/or rail transport), etc.

We shall outline how one might describe such (infrastructure component) domains, informally and formally - what the current descriptional limitations appear to be, and, hence, the prospects for future research as well as practice.

The current paper is based on Part IV, Chaps. 8-16 of [3]. The volume is one of [1,2,3].

The aim of this paper is to suggest a number of areas of domain theory and methodology research.

A theory of programming is intended to help in the construction of programs that provably meet their specifications. It starts with a complete lattice of specifications, used as a domain for the semantics of the programming language. The operators of the language are defined as monotonic functions over this domain. This paper presents a method which enables us to derive an enriched semantics for the imperative languages. We show that the new definition of the primitive commands can be recast as the weakest solution of the embedding equation, and demonstrate how the operators of the programming language are redefined from the homomorphic property of the embedding and the healthiness conditions imposed on “real” programs.

Differing from [6] this paper reduces non-linear ranking function discovering for polynomial programs to semi-algebraic system solving, and demonstrates how to apply the symbolic computation tools, DISCOVERER and QEPCAD, to some interesting examples.

Mobile ambients calculus is a formalism for mobile computing able to express local communications inside ambients. Ambients mobility is controlled by capabilities: , and . We add timers to communication channels, capabilities and ambients, and use a typing system for communication. The passage of time is given by a discrete global time progress function. We prove that structural congruence and passage of time do not interfere with the typing system. Moreover, once well-typed, an ambient remains well-typed. A timed extension of the cab protocol illustrates how the new formalism is working.

Binary semaphores can be used to implement conditional critical regions by using the split binary semaphore (SBS) technique. Given a specification of a conditional critical regions problem, the SBS technique provides not only the resulting programs but also some invariants which ensure the correctness of the solution. The programs obtained in this way are generally not efficient. However, they can be optimized by strengthening these invariants and using them to eliminate unnecessary tests.

We present a mechanical method to perform these optimizations. The idea is to use the backward propagation technique over a guarded transition system that models the behavior of the programs generated by the SBS. This process needs proving heavy implications and simplifying growing invariants. Our method automatically entrusts these tasks to the Isabelle theorem prover and the CVC Lite validity checker. We have tested our method on a number of classical examples from concurrent programming.

Simulink is a popular tool for model-based development of control systems. However, due to the complexity caused by the increasing demand for sophisticated controllers, validation of Simulink models is becoming a more difficult task. To ensure correctness and reliability of large models, it is important to be able to reason about model parts and their interactions. This paper provides a definition of contracts and refinement using the action system formalism. Contracts enable abstract specifications of model parts, while refinement offers a framework to reason about correctness of implementation of contracts, as well as composition of model parts. An example is provided to illustrate system development using contracts and refinement.

In this paper we design a distributed variant of higher order -calculus which takes distributed location into account. Furthermore, we present three bisimulations for such a distributed higher order -calculus, called distributed context bisimulation, distributed normal bisimulation and distributed reduction bisimulation respectively. We prove that the three distributed bisimulations are equivalent.

In this paper we present a propositional deontic logic, with the goal of using it to specify fault-tolerant systems, and an axiomatization of it. We prove several results about this logic: completeness, soundness, compactness and decidability. The main technique used during the completeness proof is based on standard techniques for modal logics, but it has some new characteristics introduced for dealing with this logic. In addition, the logic provides several operators which appear useful for use in practice, in particular to model fault-tolerant systems and to reason about their fault tolerance properties.

Lock-free algorithms are designed to improve the performance of concurrent programs by maximising the potential for processes to operate in parallel. Lock-free algorithms guarantee that within the system as a whole, process will eventually complete its operation (as opposed to guaranteeing that operations will eventully complete). Since lock-free algorithms potentially allow a high degree of interference between concurrent processes, and because their progress property is non-trivial, it is difficult to be assured of their correctness without a formal, machine-checked verification. In this paper we describe a method for proving the lock-free progress property. The approach is based on the construction of a well-founded ordering on the set of processes. The method is demonstrated using a well-known lock-free stack algorithm as an example, and we describe how the proof was checked using a theorem prover.

We present a new programming approach based on a contextual component specification. The language we propose integrates XML and functional aspects in a coherent and homogeneous framework. This enables us to fully have static typing and to specify formal properties with respect to interactions.

Our language FICX, Functional Interactive and Compositional XML, defines a new kind of data structure called Xobjects and relies on a statically typed functional language (currently OCaml). An Xobject is an abstract structure made in two parts: the Xdata part is an XML structure extended by means of triggers dedicated to interactions, the reaction part gives the code associated to triggers that is evaluated on demand. The modularity is ensured by a parameterization of Xobjects: compound Xobjects form a tree structure, rendering a complex XML tree together with appropriate reactions for triggers. A program is a set of structures, each structure being a tree of Xobjects.