Abstract
Recent accounts of accidents draw attention to "automation surprises" that arise in safety critical systems. An automation surprise can occur when a system behaves differently from the expectations of the operator. Interface mode changes are one class of such surprises that have significant impact on the safety of a dynamic interactive system. They may take place implicitly as a result of other system action. Formal specifications of interactive systems provide an opportunity to analyse problems that arise in such systems. In this paper we consider the role that an interactor based specification has as a partial model of an interactive system so that mode consequences can be checked early in the design process. We show how interactor specifications can be translated into the SMV model checker input language and how we can use such specifications in conjunction with the model checker to analyse potential for mode confusion in a realistic case. Our final aim is to develop a general purpose methodology for the automated analysis of interactive systems. This verification process can be useful in raising questions that have to be addressed in a broader context of analysis.

Abstract
This paper sketches a discipline for reverse engineering which combines formal and semi-formal methods. Among the former is the algebra of programming, which we apply in "reverse order" so as to reconstruct formal specifications of legacy code. The latter includes code slicing, used as a means of trimming down the complexity of handling the formal semantics of all program variables at the same time. A strong point of the approach is its constructive style. Reverse calculations go as far as imploding auxiliary variables, introducing mutual recursion (if applicable) and transforming semantic functions into standard generic programming schemata such as cata/paramorphisms. We illustrate the approach by reversing a piece of code (from C to HASKELL) already studied in the codeslicing literature: the word-count (wc) program.

Abstract
This paper sketches a reverse engineering discipline which combines formal and semi-formal methods. Central to the former is denotational semantics, expressed in the ISO/IEC 13817-1 standard specification language (VDM-SL). This is strengthened with algebra of programming, which is applied in "reverse order" so as to reconstruct formal specifications from legacy code. The latter include code slicing, a "shortcut" which trims down the complexity of handling the formal semantics of all program variables at the same time. A key point of the approach is its constructive style. Reverse calculations go as far as absorbing auxiliary variables, introducing mutual recursion (if applicable) and reversing semantic denotations into standard generic programming schemata such as cata/paramorphisms. The approach is illustrated for a small piece of code already studied in the code-slicing literature: Kernighan and Richtie's word count C programming "bagatelle".

Abstract
This paper is an attempt to apply the reasoning principles and calculational style underlying the so-called Bird-Meertens formalism to the design of process calculi, parametrized by a behaviour model. In particular, basically equational and pointfree proofs of process properties are given, relying on the universal characterisation of anamorphisms and therefore avoiding the explicit construction of bisimulations. The developed calculi can be directly implemented on a functional language supporting coinductive types, which provides a convenient way to prototype processes and assess alternative design decisions. ©2001 Published by Elsevier Science B.V.

Abstract
In this paper we address the problem of organized collective agency, and propose a deontic/action modal logic for that purpose. We argue that once we want to attribute obligations (permissions or other deontic notions) to a set of agents, we need to consider a new agent-that we called institutionalized agent, and specify how he interacts with the external world: how the obligations flow from the institutionalized agent to the real agents that support him, and how the actions of the latter count as actions of the former. But an agent may act in many qualities (roles), and it is essential to know in which quality an agent has acted, or intends to act, for three main reasons: to know the effects of the act, its deontic qualification, and authentication issues. Thus, we extend the "sees to it" action operator with an explicit index that states the quality (role) in which the agent has acted. We also show how to associate obligations to roles, and illustrate flow this can be used to express the desired flow of obligations.

Abstract
Emerging technologies that allow a two-way communication between companies, or among companies and their customers, are changing the rules of the market, facilitating the emergence of virtual entities that have to be supported by some kind of platform. Making it is the main objective of this work, materialized in a Mobile Agent Architecture (MAA) which supports the emerging world of the m-Commerce (mobile-Commerce): the MAgnUM architecture, The MAA's development was based on the principles of process and knowledge abstraction, compositionality, reuse, formal semantics, formal evaluation, and security.