Abstract

Abstract
In this paper we argue that using verification in interactive systems development is more than just checking whether the specification of the system has all the required properties; and that changing the focus from a global specification into partial, property oriented, specifications can provide a number of advantages and make verification act as an aid to decision making. We also present a compiler that allows for the verification of interactor specifications to be done in SMV, as well as a simple case study where verification is used to inform a design decision.

Abstract
This paper illustrates the application of formal specification techniques to the experimental development of a CAD tool for building-specification and automatic building-plan plotting. Buildings are specified in an abstract way which records what the architect wants, to build and not how it is actually built in terms of construction materials. Building designs are not recorded in terms of their drawings, but lather in a linguistic way, by structural composition of standard space units according to an abstract syntax equipped with space aggregation constructs, subject to formal properties which check for building well-formedness. A formal model is developed for such an abstract syntax and for its associated functionality which (as later prototyped in a rapid-prototyping shell) has mainly to do with automatically generating building plans from abstract descriptions. At prototype level, this is first achieved by structurally calculating LATEX picture format drawings as a pictorial semantics of the abstract descriptions. In a second phase, the adopted output graphical server is the AUTOCAD(TM) system. Throughout these experiments, not only did formal methods greatly increase confidence on the building-description language correctness, expressive power and conciseness, but also rapid prototyping provided a great deal of insight on the design, at a very low cost. A future implementation is discussed which not only will provide the system as a 'plug-in' extension of AUTOCAD for WINDOWS(TM), but will also connect it to an underlying production database allowing for automatic construction materials planning and budget control.

Abstract
This paper presents a formal framework in which to study the socialization processes evolving among utility-based agents. These agents are self-interested, being their different social attitudes (cooperativeness, competitiveness or indifference) a consequence of this behavior. The dynamics of the socialization process are captured by a relation that measures the similarities between the desires of two groups of agents. This similitude relation is derived from the system's model, defined as a probabilistic transition system and a set of individual preference relations. Game-theoretic concepts are used in order to determine the rational(or expected) transitions of the system. © 1998 IEEE.

Abstract
Today's dynamic industrial process simulation problems require systematically new methodologies and sophisticated computational tools. Such processes involve frequently discontinuities, environment structures changes and entities with high functional levels. Furthermore, there are cases where we must integrate intelligent techniques and negotiation protocols. These characteristics are crucial in distributed problems that require resource balance, low cost distribution plans, and stock optimization. In order to analyse the application of a distributed object-oriented simulation system we selected, as a case study, a gas distribution network in which we find all the referred characteristics. This paper presents a brief description of the simulation scenario, the overall system's structure, the intelligent negotiation protocol used by system's objects and the concurrent programming techniques to implement it.

Abstract
CANopen is a field level communication protocol for industrial automation distributed applications. The acceptance of CANopen is already widespread and continues growing, because it offers not only all the well known features of CAN for real-time communication, but also a powerful set of higher level Application Layer services. These services implement an object-oriented distributed environment for simplified system integration, but still they allow for a very high level of communication efficiency. Often, sensors and actuators have to be placed at geographically remote locations, at considerable distances from the processor(s) running a control application. When this is the case, a possible solution, that is gaining increasing popularity, is to use an autonomous I/O module, located close to the sensors and actuators, that provides the application with an interface to these devices. For this to be possible, the application must be distributed between the remote I/O module and the local processor(s) using a communication network to allow the different parts to cooperate. This work is centred on the development of an I/O module of the type previously described, based on the SAB-C167CR-LM chip from SIEMENS. The device is able, on one hand, to interface with sensors and actuators using digital signals and, on the other hand, to communicate using the CANopen protocol. In other words, the I/O module makes sensors and actuators accessible via the CAN bus, using the CANopen protocol. The objective is to show that CANopen can be implemented over new hardware platforms, in minimum time, with satisfactory results. It is shown that CANopen provides a systems-integrator-friendly object-oriented environment and that for this reason, the CANopen Communication Profile greatly simplifies the implementation of distributed applications in CAN based systems. Furthermore, CANopen also provides flexible realtime data transfer mechanisms that are able to meet time-critical constraints and, therefore,make CANopen a good solution for distributed control environments.