Abstract
It is proposed an approach to integrate formal methods in the software development process, with an emphasis on the user interface development. The approach covers the specification by means of formal models, early model animation and validation, construction and conformity testing of the user interface implementation with respect to the specification. These conformity tests are described in detail through a state transition model with an abstraction function mapping concrete (implementation) to abstract (specification) states and operations. In order to illustrate the approach, it is presented a simple login/password dialog specification in VDM++, using a reusable control specification library, with a straightforward translation to Java or C#.

Abstract
SINUP consists of a geographical information system whose purpose is to store, in a coherent manner, data resulting from key activities of Oporto local authority, allowing to better structure the knowledge about the urban reality. In the possession of such knowledge, and with the revision of Oporto's Municipal Master Plan taking place soon, the municipality is making an effort to develop an electronic citizen service that will allow a large number of citizens to consult it, and more important, participate in its public discussion prior to approval thus creating a major instrument of e-democracy in Oporto's municipality.

Abstract
The emergence of run-time reconfigurable architectures makes feasible the configure-execute paradigm. Compilation of behavioral descriptions (in, e.g., C, Java, etc.), apart from mapping the computational structures onto the available resources on the device, must split the program in temporal sections if it needs more resources than physically available. In addition, since the execution of the computational structures in a configuration needs at least two stages (i.e., configuring and computing), it is important to split the program such that the reconfiguration overheads are minimized, taking advantage of the overlapping of the execution stages on different configurations. This paper presents mapping techniques to cope with those features. The techniques are being researched in the context of a C compiler for the eXtreme Processing Platform (XPP). Temporal partitioning is applied to furnish a set of configurations that reduces the reconfiguration overhead and thus may lead to performance gains. We also show that when applications include a sequence of loops, the use of several configurations may be more beneficial than the mapping of the entire application onto a single configuration. Preliminary results for a number of benchmarks strongly confirm the approach.

Abstract
These techniques for compiling software programs into reconfigurable hardware offer faster and more efficient performance than the complex resource-sharing approaches typical of high-level synthesis systems. The Java-based compiler presented in this article uses intermediate graph representations to embody parallelism at various levels.

Abstract
Resource virtualization on FPGA devices, achievable due to its dynamic reconfiguration capabilities, provides an attractive solution to save silicon area. Architectural synthesis for dynamically reconfigurable FPGA-based digital systems needs to consider the case of reducing the number of temporal partitions (reconfigurations) by enabling sharing of some functional units in the same temporal partition. This paper proposes a novel algorithm for automated datapath design from behavioral input descriptions (represented by an acyclic dataflow graph), which simultaneously performs temporal partitioning and sharing of functional units. The proposed algorithm attempts to minimize both the number of temporal partitions and the execution latency of the generated solution. Temporal partitioning, resource sharing, scheduling, and a simple form of allocation and binding are all integrated in a single task. The algorithm is based on heuristics and on a new concept of construction by gradually enlarging timing slots. Results show the efficiency and effectiveness of the algorithm when compared to existent approaches.

Abstract
An increasing interest in the design of mobile robots has been observed in recent years, which is mainly motivated by technological advances that may allow their application to consumer markets, in addition to industrial areas. Although sophisticated techniques have been developed, choosing the appropriate hardware-software partitioning and programming robot functions are still very complex tasks. Current approaches often involve the design and implementation of hardwired solutions, with the associated problems of a long development cycle and inflexibility. In this paper we present a framework called ARCHITECT-R, which aims to design and program specialized hardware for robots based on FPGAs. We also present the first results obtained using this framework.