Recent Publications

Campos JC.  1999.  Automated Deduction and Usability Reasoning. Abstractycst-2000-09.pdf

Reasoning about the usability of a given interactive system's design is a difficult task. However it is one task that must be performed if downstream costs with extensive redesign are to be avoided. Traditional usability testing alone cannot avoid these costs since it too often is performed late in development life cycle. In recent years approaches have been put forward that attempt to reason about the usability of a design from early in development. Mainstream approaches are based on some kind of (more or less structured) inspection of a design by usability experts. This type of approach breaks down for systems with large and complex user interfaces, and again extensive testing is required. In an attempt to deal with these issues there have been attempts to apply software engineering reasoning tools to the development of interactive systems. The article reviews this work and puts forward some ideas for the future.

Pereira JO.  1998.  Comunicação Fiável em Sistemas Distribuídos em Grande Escala. Abstracttese.pdf

Protocolos de difusão fiável em grupos de processo são uma ferramenta de programação utilizada em sistemas distribuídos e confiáveis para isolar cada aplicação da complexidade decorrente da comunicação e das diversas faltas que podem ocorrer no sistema. Isto é conseguido oferecendo às aplicações uma abstração de um canal de difusão que oferece garantias muito fortes quanto à qualidade de serviço, o que é suficiente para garantir a correção de um largo espectro de aplicações com um esforço mínimo por parte do programador.
A concretização de protocolos de difusão fiável sobre redes em grande escala introduz um nível adicional de complexidade, pois as características destas redes dificultam a concretização correta e eficiente de serviços que oferecem garantias muito fortes.
Diversas propostas procuram ultrapassar este problema disponibilizando serviços que oferecem menos garantias de qualidade de serviço, mas que apresentam desempenho superior nas situações em que são utilizáveis. No entanto, quanto menos garantias se oferecerem, menos aplicações podem ser correctamente suportadas, uma vez que diferentes aplicações toleram diferentes relaxamentos da qualidade de serviço.
Nesta tese propõe-se um protocolo de difusão fiável que possa ser configurado para cada aplicação, de modo a poder ser simultaneamente eficiente e correcto porque adequado à aplicação em causa.
Para o efeito, começa-se por decompor a especificação de protocolos de difusão segundo um conjunto de parâmetros aplicáveis em separado a cada uma das mensagens de uma sessão, que podem ser combinados em especificações de protocolos adequados a cada aplicação.
Propõe-se então uma estratégia de concretização aberta orientada por objetos, que permite compor protocolos a partir de módulos independentes para cada mensagem, correspondentes aos parâmetros de especificação.

Almeida PS.  1998.  Control of object sharing in programming languages. Abstractpsa-phd-thesis.pdf

Current data abstraction mechanisms are not adequate to control sharing of state in the general case involving objects in linked structures. They only prevent the direct access to the state variables of single objects, as opposed to considering the state reachable by an object and the inter-object references, neglecting the fact that an object is not, in general, self-contained. The pervading possibility of sharing is a source of errors and an obstacle both to reasoning about programs and to language implementation techniques.
This thesis presents balloon types, a general extension to programming languages which makes the ability to share state a first class property of a data type, resolving a long-standing flaw in existing data abstraction mechanisms. Balloon types provide the balloon invariant, which expresses a strong form of encapsulation of state: it is guaranteed that no state reachable (directly or transitively) by an object of a balloon type is referenced by any `external' object.
The mechanism is syntactically very simple, relying on a non-trivial static analysis to perform checking. The static analysis is presented as an abstract interpretation based on a denotational semantics of a simple imperative first-order language with constructs for creating and manipulating objects.
Balloon types are applicable in a wide range of areas such as program transformation, memory management and distributed systems. They are the key to obtaining self-contained composite objects, truly opaque data abstractions and value types---important concepts for the development of large scale, provably correct programs.

Frade MJ.  1995.  Comportamento e Estado. Abstractcompest.pdf

In this work we introduce a formalism for specifying the behaviour of computational systems, based on logic.
Our basic unit of software specification is called agent and is nothing more than a particular logical system. The agent logical language allow us to express the relationship between the occurrence of events and the properties an agent exhibits. The events are seen as logical connectives and the logical assertions reflect the causality between events and properties - the essential cause of a property in face of an event.
Because we are interested in knowing which sequence of events “justify” a property, we have traces coming from the past to the present. Our perspective is that of knowing which behaviour could justify the characteristics of au agent in some instant. Obviously, these characteristics will condition the future behaviour of the agent. This dependency is expressed in a deduction system that reflects the notion of causality.
For the purpose of characterizing the agents semantically a connection is made between the logical system and its topological models. The Stone duality provides a junction between the logical system and its semantics and it provides two alternative perspectives:
the algebraic or logical perspective and the topological perspective.
We present two types of models for the agents: the trace model, a denotational model intimately connected to the notion of event and trace, and the state model, au operational model based on the notions of state and state transitions.
We establish a relation between these two types of models: we see how a state model may be obtained from a trace model. The states arise as equivalence classes of past behaviours. We also study the properties of the state models which result from the conversion of trace models. We see how topological properties — such as separation conditions, soberty and coherence — characterize the state space of these modeis, and how from behaviour we can generate a minimal state space.

Campos JC.  1993.  GAMA- X - Geração Semi-Automática de Interfaces Sensíveis ao Contexto. Abstractmestrado.pdf

A separação dos sistemas interactivos em componente computacional e componente de diálogo, veio possibilitar o aparecimento de tecnologia, específica para a implementação de interfaces com o utilizador. No entanto, apesar da grande quantidade de tecnologia disponível, a construção de uma interface é ainda um processo difícil e demorado. Tal situação, deu origem ao estudo e desenvolvimento de metodologias que permitam especificar formalmente o diálogo humano-computador, tendo em vista um desenvolvimento mais rápido e seguro da referida camada. A interface de um sistema interactivo não deve ser apenas um meio de transmissão passivo entre o utilizador e a aplicação, mas um reflexo da aplicação, permitindo ao utilizador saber o estado actual da mesma facilitando-lhe, assim, o diálogo com ela. A separação demasiado rígida, proposta por muitos modelos, entre camada computacional e camada de diálogo não permite o desenvolvimento de interfaces deste tipo, uma vez que a informação semântica se encontra encapsulada na componente computacional. Com base nestas constatações, foi estudado e implementado um formalismo de especificação de diálogo - Guiões de Interacção - que permite a inclusão de condições semãnticas na especificação, possibilitando expressar claramente e diferenciar as componentes dinâmicas do diálogo, em particular “o diálogo sensível ao con da aplicação”. A utilização de uma notação a la CCS permite a especificação de diálogos concorrentes, tendo-se utilizado Petri Nets para lhes dar semântica e como modelo de implementação dos Guiões de Interacção. É ainda apresentada a arquitectura do sistema GAMA-X - um UIMS para a linguagem CAMILA baseado em Guiões de Interacção - e feita a implementação da componente de runtime do mesmo, provando, deste modo, a validade dos Guiões de Interacção enquanto formalismo para a especificação de diálogo.

Estevez E, Cledou MG, Janowski T.  2013.  Electronic Participation - Framework.
Estevez E, Cledou MG, Janowski T.  2013.  Electronic Participation - Toolkit.