This paper presents a new approach in plant modeling for the formal verification of real time systems. A system composed by two tanks is used, where all its components are modeled by simple modules and all the interdependences of the system?s modular models are presented. As innovating parameters in the plant modeling, having as purpose its use on formal verification tasks, the plant is modeled using Dymola software and Modelica programming language. The results obtained in simulation are used to define the plant models that are used for the formal verification tasks, using the model-checker UPPAAL. The paper presents, in a more detailed way, the part of this work that is related to formal verification, being pointing out the used plant modeling approach.

Software Engineering (SE) and HCI (Human Computer Interaction) are not the same age, do not have the same history, background or foundations, and did never share design principles and design models. The separation principle, by encouraging separate concerns and techniques to design the interactive and the computational layers of a software system - despite being absolutely correct from several SE crucial design principles, like modularity, separation of concerns, encapsulation, context independence and so on -, has sometimes been misjudged and mistakenly used. Therefore, instead of bridging the gap between the two separate de- signs, it helped widening that gap. However, the principle does not mention and does not impose any restrictions on how the integration should be done. In the context of a software engineering course the authors have been involved with for some years, the need has arisen to provide students with HCI skills. Several attempts at integrating HCI into software engineering can be found in the literature. However, none seemed amenable to application in the context of the course, basically because none of them could be taught and learnt in such a way (methodology) that could easily be blent into the software engineering design process. We present a methodological process that we have been teaching that aims at shortening the gap that software engineering students face when trying to adapt SE techniques to the interactive layer.

Graphical user interfaces (GUIs) make software easy to use by providing the user with visual controls. Therefore, correctness of GUI’s code is essential to the correct execution of the overall software. Models can help in the evaluation of interactive applications by allowing designers to concentrate on its more important aspects. This paper describes our approach to reverse engineer an abstract model of a user interface directly from the GUI’s legacy code. We also present results from a case study. These results are encouraging and give evidence that the goal of reverse engineering user interfaces can be met with more work on this technique.

We extend the generic framework of reproducibility for reuse of randomness in multi-recipient encryption schemes as proposed by Bellare et al. (PKC 2003). A new notion of weak reproducibility captures not only encryption schemes which are (fully) reproducible under the criteria given in the previous work, but also a class of efficient schemes which can only be used in the single message setting. In particular, we are able to capture the single message schemes suggested by Kurosawa (PKC 2002), which are more efficient than the direct adaptation of the multiple message schemes studied by Bellare et al. Our study of randomness reuse in key encapsulation mechanisms provides an additional argument for the relevance of these results: by taking advantage of our weak reproducibility notion, we are able to generalise and improve multi-recipient KEM constructions found in literature. We also propose an efficient multi-recipient KEM provably secure in the standard model and conclude the paper by proposing a notion of direct reproducibility which enables tighter security reductions.

There is an inherent trade-off between epidemic and deterministic tree-based broadcast primitives. Tree-based approaches have a small message complexity in steady-state but are very fragile in the presence of faults. Gossip, or epidemic, protocols have a higher message complexity but also offer much higher resilience. This paper proposes an integrated broadcast scheme that combines both approaches. We use a low cost scheme to build and maintain broadcast trees embedded on a gossip-based overlay. The protocol sends the message payload preferably via tree branches but uses the remaining links of the gossip overlay for fast recovery and expedite tree healing. Experimental evaluation presented in the paper shows that our new strategy has a low overhead and that is able to support large number of faults while maintaining a high reliability.

A two-level data transformation consists of a type-level transformation of a data format coupled with value-level transformations of data instances corresponding to that format. We have implemented a system for performing two-level transformations on XML schemas and their corresponding documents, and on SQL schemas and the databases that they describe. The core of the system consists of a combinator library for composing type-changing rewrite rules that preserve structural information and referential constraints. We discuss the implementation of the system’s core library, and of its SQL and XML front-ends in the functional language Haskell. We show how the system can be used to tackle various two-level transformation scenarios, such as XML schema evolution coupled with document migration, and hierarchical-relational data mappings that convert between XML documents and SQL databases.

Various programming languages allow the construction of structureshy programs. Such programs are defined generically for many different datatypes and only specify specific behavior for a few relevant subtypes. Typical examples are XML query languages that allow selection of subdocuments without exhaustively specifying intermediate element tags. Other examples are languages and libraries for polytypic or strategic functional programming and for adaptive object-oriented programming. In this paper, we present an algebraic approach to transformation of declarative structure-shy programs, in particular for strategic functions and XML queries. We formulate a rich set of algebraic laws, not just for transformation of structure-shy programs, but also for their conversion into structure-sensitive programs and vice versa. We show how subsets of these laws can be used to construct effective rewrite systems for specialization, generalization, and optimization of structure-shy programs. We present a typesafe encoding of these rewrite systems in Haskell which itself uses strategic functional programming techniques.