Abstract
Many errors in spreadsheet formulas can be avoided if spreadsheets are built automatically from higher-level models that can encode and enforce consistency constraints. However, designing such models is time consuming and requires expertise beyond the knowledge to work with spreadsheets. Legacy spreadsheets pose a particular challenge to the approach of controlling spreadsheet evolution through higher-level models, because the need for a model might be overshadowed by two problems: (A) The benefit of creating a spreadsheet is lacking since the legacy spreadsheet already exists, and (B) existing data must be transferred into the new model-generated spreadsheet. To address these problems and to support the model-driven spreadsheet engineering approach, we have developed a tool that can automatically infer ClassSheet models from spreadsheets. To this end, we have adapted a method to infer entity/relationship models from relational database to the spreadsheets/ClassSheets realm. We have implemented our techniques in the HAEXCEL framework and integrated it with the ViTSL/Gencel spreadsheet generator, which allows the automatic generation of refactored spreadsheets from the inferred ClassSheet model. The resulting spreadsheet guides further changes and provably safeguards the spreadsheet against a large class of formula errors. The developed tool is a significant contribution to spreadsheet (reverse) engineering, because it fills an important gap and allows a promising design method (ClassSheets) to be applied to a huge collection of legacy spreadsheets with minimal effort. © 2010 IEEE.

Abstract
Zero-knowledge proofs of knowledge (ZK-PoK) are important building blocks for numerous cryptographic applications. Although ZK-PoK have a high potential impact, their real world deployment is typically hindered by their significant complexity compared to other (non-interactive) crypto primitives. Moreover, their design and implementation are time-consuming and error-prone. We contribute to overcoming these challenges as follows: We present a comprehensive specification language and a compiler for ZK-PoK protocols based on Sigma-protocols. The compiler allows the fully automatic translation of an abstract description of a proof goal into an executable implementation. Moreover, the compiler overcomes various restrictions of previous approaches, e.g., it supports the important class of exponentiation homomorphisms with hidden-order co-domain, needed for privacy-preserving applications such as DAA. Finally, our compiler is certifying, in the sense that it automatically produces a formal proof of the soundness of the compiled protocol for a large class of protocols using the Isabelle/HOL theorem prover.

Abstract
The user experience of ubiquitous environments is a determining factor in their success. The characteristics of such systems must be explored as early as possible to anticipate potential user problems, and to reduce the cost of redesign. However, the development of early prototypes to be evaluated in the target environment can be disruptive to the ongoing system and therefore unacceptable. This paper reports on an ongoing effort to explore how model-based rapid prototyping of ubiquitous environments might be used to avoid actual deployment while still enabling users to interact with a representation of the system. The paper describes APEX, a framework that brings together an existing 3D Application Server with CPN Tools. APEX-based prototypes enable users to navigate a virtual world simulation of the envisaged ubiquitous environment. The APEX architecture and the proposed CPN-based modelling approach are described. An example illustrates their use.

Abstract
Although presented with a variety of 'flavours', the notion of an interactor, as an abstract characterisation of an interactive component, is well-known in the area of formal modelling techniques for interactive systems. Tins paper replaces traditional, hierarchical, 'tree-like' composition of interactors in the specification of complex interactive systems, by their exogenous coordination through general-purpose software connectors which assure the flow of data and the meet of synchronisation constraints. The paper's technical contribution is twofold. First a modal logic is defined to express behavioural properties of both interactors and connectors. The logic is new in the sense that its modalities are indexed by fragments of sets of actions to cater for action co-occurrence. Then, tins logic is used in the specification of both interactors and coordination layers which orchestrate their interconnection.

Abstract
Aerospace systems software is developed taking into account some precautions to avoid dangerous situations. Usually the controllers of these systems are critical embedded real-time controllers and the respective software programs are developed in the C programming language. This paper is developed on the context of developing embedded critical real-time systems software, for aerospace systems applications, based on formalisms commonly used in the industrial automation field. More precisely, the approach proposed, in this paper, consists in translating a SFC specification to C programming language code considering also the behaviour of the controller device, where the specification will be implemented. An illustrative case study is presented in the end of the paper in order to facilitate the understanding of the proposed approach.

Abstract
This article's main goal is to present a review on the principles of ergonomics applied to tools used for e-learning. It is known that the errors in the application of these principles entail cognitive overload on users of these platforms, so the article tries to address the issue comprehensively. Thus, in the first section presents the most notable ergonomic principles as the foundations of Cognitive and Informational Ergonomics and then presents guidelines for the usability of information systems that can serve as support for academic interactions. In the second part, there will be a discussion about some aspects from collaborative learning experiences among teachers and students in research projects and extension. The methodology of this paper points to a research of qualitative nature, where the aim was to understand the interactions virtually experienced by users of systems whose goal is to encourage the construction of the academic knowledge. The results of this research appear as an additional form of analysis of issues related to ergonomics, so that the information systems always prioritize the different profiles of its users.