The real-time refinement calculus: A foundation for machine-independent real-time programming

The real-time refinement calculus is an extension of the standard refinement calculus in which programs are developed from a precondition plus post-condition style of specification. In addition to adapting standard refinement rules to be valid in the real-time context, specific rules are required for the timing constructs such as delays and deadlines. Because many real-time programs may be nonterminating, a further extension is to allow nonterminating repetitions. A real-time specification constrains not only what values should be output, but when they should be output. Hence for a program to implement such a specification, it must guarantee to output values by the specified times. With standard programming languages such guarantees cannot be made without taking into account the timing characteristics of the implementation of the program on a particular machine. To avoid having to consider such details during the refinement process, we have extended our real-time programming language with a deadline command. The deadline command takes no time to execute and always guarantees to meet the specified time; if the deadline has already passed the deadline command is infeasible (miraculous in Dijkstra's terminology). When such a realtime program is compiled for a particular machine, one needs to ensure that all execution paths leading to a deadline are guaranteed to reach it by the specified time. We consider this checking as part of an extended compilation phase. The addition of the deadline command restores for the real-time language the advantage of machine independence enjoyed by non-real-time programming languages.

Language-based Techniques for Practical and Trustworthy Secure Multi-party Computations

Secure Multi-party Computation (MPC) enables a set of parties to collaboratively compute, using cryptographic protocols, a function over their private data in a way that the participants do not see each other's data, they only see the final output. Typical MPC examples include statistical computations over joint private data, private set intersection, and auctions. While these applications are examples of monolithic MPC, richer MPC applications move between "normal" (i.e., per-party local) and "secure" (i.e., joint, multi-party secure) modes repeatedly, resulting overall in mixed-mode computations. For example, we might use MPC to implement the role of the dealer in a game of mental poker -- the game will be divided into rounds of local decision-making (e.g. bidding) and joint interaction (e.g. dealing). Mixed-mode computations are also used to improve performance over monolithic secure computations. Starting with the Fairplay project, several MPC frameworks have been proposed in the last decade to help programmers write MPC applications in a high-level language, while the toolchain manages the low-level details. However, these frameworks are either not expressive enough to allow writing mixed-mode applications or lack formal specification, and reasoning capabilities, thereby diminishing the parties' trust in such tools, and the programs written using them. Furthermore, none of the frameworks provides a verified toolchain to run the MPC programs, leaving the potential of security holes that can compromise the privacy of parties' data. This dissertation presents language-based techniques to make MPC more practical and trustworthy. First, it presents the design and implementation of a new MPC Domain Specific Language, called Wysteria, for writing rich mixed-mode MPC applications. Wysteria provides several benefits over previous languages, including a conceptual single thread of control, generic support for more than two parties, high-level abstractions for secret shares, and a fully formalized type system and operational semantics. Using Wysteria, we have implemented several MPC applications, including, for the first time, a card dealing application. The dissertation next presents Wys*, an embedding of Wysteria in F*, a full-featured verification oriented programming language. Wys* improves on Wysteria along three lines: (a) It enables programmers to formally verify the correctness and security properties of their programs. As far as we know, Wys* is the first language to provide verification capabilities for MPC programs. (b) It provides a partially verified toolchain to run MPC programs, and finally (c) It enables the MPC programs to use, with no extra effort, standard language constructs from the host language F*, thereby making it more usable and scalable. Finally, the dissertation develops static analyses that help optimize monolithic MPC programs into mixed-mode MPC programs, while providing similar privacy guarantees as the monolithic versions.

Developing and implementing an open and non-proprietary device description for FOUNDATION fieldbus based on software standards

Support for interoperability and interchangeability of software components which are part of a fieldbus automation system relies on the definition of open architectures, most of them involving proprietary technologies. Concurrently, standard, open and non-proprietary technologies, such as XML, SOAP, Web Services and the like, have greatly evolved and been diffused in the computing area. This article presents a FOUNDATION fieldbus (TM) device description technology named Open-EDD, based on XML and other related technologies (XLST, DOM using Xerces implementation, OO, XMIL Schema), proposing an open and nonproprietary alternative to the EDD (Electronic Device Description). This initial proposal includes defining Open-EDDML as the programming language of the technology in the FOUNDATION fieldbus (TM) protocol, implementing a compiler and a parser, and finally, integrating and testing the new technology using field devices and a commercial fieldbus configurator. This study attests that this new technology is feasible and can be applied to other configurators or HMI applications used in fieldbus automation systems. (c) 2008 Elsevier B.V. All rights reserved.

Proposal of a High-Level Language for Writing Self Modifying Programs

This paper proposes a simple high-level programming language, endowed with resources that help encoding self-modifying programs. With this purpose, a conventional imperative language syntax (not explicitly stated in this paper) is incremented with special commands and statements forming an adaptive layer specially designed with focus on the dynamical changes to be applied to the code at run-time. The resulting language allows programmers to easily specify dynamic changes to their own program`s code. Such a language succeeds to allow programmers to effortless describe the dynamic logic of their adaptive applications. In this paper, we describe the most important aspects of the design and implementation of such a language. A small example is finally presented for illustration purposes.

An L-system-based plant modeling language

Cpfg is a program for simulating and visualizing plant development, based on the theory of L-systems. A special-purpose programming language, used to specify plant models, is an essential feature of cpfg. We review postulates of L-system theory that have influenced the design of this language. We then present the main constructs of this language, and evaluate it from a user's perspective.

Concep����o de uma pequena turbina e��lica destinada ao segmento dom��stico (simplifica����o e an��lise aerodin��mica das p��s)

O trabalho que se apresenta incide sobre o estudo aerodin��mico das p��s de uma turbina e��lica de pequeno porte, com vista �� simplifica����o geom��trica, de forma a que estas sejam baratas e de f��cil concep����o. A teoria da quantidade de movimento do elemento de p�� (BEMT), que �� o modelo de refer��ncia para o projecto e an��lise aerodin��mica das p��s das turbinas e��licas, foi utilizada neste trabalho de forma a projectar e analisar aerodinamicamente as p��s da turbina. Sendo assim, desenvolveu-se um programa computacional em MATLAB, denominado de ���Turbina���, de forma a implementar a teoria BEM. Introduzindo os dados dos par��metros de projecto no programa (pot��ncia requerida, o n��mero de p��s, velocidade do vento, a TSR e o tipo de perfil alar), obt��m-se os par��metros geom��tricos das p��s (distribui����o da corda ao longo da envergadura, o raio da p�� e a distribui����o da tor����o da p��), os par��metros aerodin��micos e de desempenho. Uma p�� ideal foi calculada e de seguida foi modificada de forma a obter-se uma p�� simples e menos carregada aerodinamicamente. Introduzidas as modifica����es na geometria da p�� ideal, obtiveram-se duas configura����es distintas. Uma configura����o linear, onde a distribui����o da corda e do ��ngulo de tor����o se tornam lineares, e outra configura����o bi-linear, onde a distribui����o da corda continua linear mas o ��ngulo de tor����o se torna bi-linear, isto ��, a p�� �� composta por dois tro��os onde cada tro��o apresenta uma distribui����o linear do ��ngulo de tor����o geom��trica. As conclus��es demonstram que a configura����o bi-linear �� uma boa alternativa a configura����o ideal, apresentando uma redu����o do desempenho do rotor de 2.8% para um aumento do raio da p�� em 1.41%, para se obter a mesma pot��ncia da configura����o ideal. A an��lise aos perfis alares, utilizados neste trabalho, foi efectuada a partir dos programas comerciais ICEM e FLUENT. De forma a automatizar a an��lise de CFD, tr��s programas foram desenvolvidos utilizando a linguagem de programa����o ���C���. Os programas s��o denominados de ���Malha2D���, ���Calcula_Coeficientes��� e ���Plot_Graficos���. Finalmente, um estudo param��trico foi feito de forma a avaliar a influ��ncias das vari��veis de projecto no desempenho geral da turbina.

To Ada or not To Ada: Adaing vs. Javaing in real-time systems

Ada is really an unfortunate Lady. After years fighting against C/C++ villains, her major lift-up (Ada 95) had brought up a promise of fortune. However, a new strong villain (Java) has appeared trying to end her struggle for survival. Ada has now to fight with her own weapons. She will only prosper by her own merits. But two questions emerge. Do they exist? Are they better than Java���s? Our opinion is that they do exist, and are not matched by any other programming language

Design and implementation of a behaviorally typed programming system for web services

Disserta����o apresentada na Faculdade de Ci��ncias e Tecnologia da Universidade Nova de Lisboa para a obten����o do Grau de Mestre em Engenharia Inform��tica.

A type system for access control in an object-oriented language

Trabalho apresentado no ��mbito do Mestrado em Engenharia Inform��tica, como requisito parcial para obten����o do grau de Mestre em Engenharia Inform��tica

Project, modelling and simulation of air stripping columns for the treatment of groundwater contaminated with volatile organic compounds

Volatile organic compounds are a common source of groundwater contamination that can be easily removed by air stripping in columns with random packing and using a counter-current flow between the phases. This work proposes a new methodology for the column design for any particular type of packing and contaminant avoiding the necessity of a pre-defined diameter used in the classical approach. It also renders unnecessary the employment of the graphical Eckert generalized correlation for pressure drop estimates. The hydraulic features are previously chosen as a project criterion and only afterwards the mass transfer phenomena are incorporated, in opposition to conventional approach. The design procedure was translated into a convenient algorithm using C++ as programming language. A column was built in order to test the models used either in the design or in the simulation of the column performance. The experiments were fulfilled using a solution of chloroform in distilled water. Another model was built to simulate the operational performance of the column, both in steady state and in transient conditions. It consists in a system of two partial non linear differential equations (distributed parameters). Nevertheless, when flows are steady, the system became linear, although there is not an evident solution in analytical terms. In steady state the resulting system of ODE can be solved, allowing for the calculation of the concentration profile in both phases inside the column. In transient state the system of PDE was numerically solved by finite differences, after a previous linearization.

Core language for web applications

Trabalho apresentado no ��mbito do Mestrado em Engenharia Inform��tica, como requisito parcial para obten����o do grau de Mestre em Engenharia Inform��tica

Estructura de datos avanzadas : clases disjuntas, mont��culos, ��rboles de b��squeda

En aquest treball s'amplia la implementaci�� en Java de les estructures de dades iniciada per Esteve Marin��, utilitzant el seu disseny b��sic. Concretament, s'ha fet la programaci�� de les estructures de a) classes disjuntes, utilitzant els algorismes de llistes encadenades i amb estructura d'arbre, b) monticles, amb els algorismes binari, binomial i de Fibonacci, i c) arbres de recerca basats en l'algorisme d'arbre binari vermell-negre, el qual complementa els dos ja existents amb algorismes d'encadenaments i AVL. Per a examinar l'evoluci�� de les estructures, s'ha preparat un visualitzador gr��fic interactiu amb l'usuari que permet fer les operacions b��siques de l'estructura. Amb aquest entorn ��s possible desar les estructures, tornar a reproduir-les i desfer i tornar a repetir les operacions fetes sobre l'estructura. Finalment, aporta una metodologia, amb visualitzaci�� mitjan��ant gr��fics, de l'avaluaci�� comparativa dels algorismes implementats, que permet modificar els par��metres d'avaluaci�� com ara nombre d'elements que s'han de tractar, algorismes que s'han de comparar i nombre de repeticions. Les dades obtingudes es poden exportar per a analitzar-les posteriorment.

UOCJOBS - portal de empleo

El proyecto a desarrollar consiste en la construcci��n de un portal de empleo para la gesti��n de ofertas y candidaturas. Esta soluci��n consta de un solo m��dulo web; constituido por una secci��n personal y una secci��n de administraci��n. El desarrollo se ha realizado con la plataforma de Microsoft .NET usando C# como lenguaje de programaci��n.

Using petri nets to specify and execute missions for autonomous underwater vehicles

This paper presents the design and implementation of a mission control system (MCS) for an autonomous underwater vehicle (AUV) based on Petri nets. In the proposed approach the Petri nets are used to specify as well as to execute the desired autonomous vehicle mission. The mission is easily described using an imperative programming language called mission control language (MCL) that formally describes the mission execution thread. A mission control language compiler (MCL-C) able to automatically translate the MCL into a Petri net is described and a real-time Petri net player that allows to execute the resulting Petri net onboard an AUV are also presented

On the origin and scope of the second language speech production disadvatage

Los hablantes biling��es tienen un acceso al l��xico m��s lento y menos robusto que los monoling��es, incluso cuando hablan en su lengua materna y dominante. Este fen��meno, com��nmente llamado ���la desventaja biling��e��� tambi��n se observa en hablantes de una segunda lengua en comparaci��n con hablantes de una primera lengua. Una causa que posiblemente contribuya a estas desventajas es el uso de control inhibitorio durante la producci��n del lenguaje: la inhibici��n de palabras coactivadas de la lengua actualmente no en uso puede prevenir intrusiones de dicha lengua, pero al mismo tiempo ralentizar la producci��n del lenguaje. El primer objetivo de los estudios descritos en este informe era testear esta hip��tesis mediante diferentes predicciones generadas por teor��as de control inhibitorio del lenguaje. Un segundo objetivo era investigar la extensi��n de la desventaja biling��e dentro y fuera de la producci��n de palabras aisladas, as�� como avanzar en el conocimiento de las variables que la modulan. En lo atingente al primer objetivo, la evidencia obtenida es incompatible con un control inhibitorio global, desafiando la idea de mecanismos espec��ficos en el hablante biling��e utilizados para la selecci��n l��xica. Esto implica que una explicaci��n com��n para el control de lenguaje y la desventaja biling��e en el acceso al l��xico es poco plausible. En cuanto al segundo objetivo, los resultados muestran que (a) la desventaja biling��e no tiene un impacto al acceso a la memoria; (b) la desventaja biling��e extiende a la producci��n del habla conectada; y (c) similitudes entre lenguas a diferentes niveles de representaci��n as�� como la frecuencia de uso son factores que modulan la desventaja biling��e. ������