Specification, refinement and verification of concurrent systems - An integration of Object-Z and CSP

This paper presents a method of formally specifying, refining and verifying concurrent systems which uses the object-oriented state-based specification language Object-Z together with the process algebra CSP. Object-Z provides a convenient way of modelling complex data structures needed to define the component processes of such systems, and CSP enables the concise specification of process interactions. The basis of the integration is a semantics of Object-Z classes identical to that of CSP processes. This allows classes specified in Object-Z to he used directly within the CSP part of the specification. In addition to specification, we also discuss refinement and verification in this model. The common semantic basis enables a unified method of refinement to be used, based upon CSP refinement. To enable state-based techniques to be used fur the Object-Z components of a specification we develop state-based refinement relations which are sound and complete with respect to CSP refinement. In addition, a verification method for static and dynamic properties is presented. The method allows us to verify properties of the CSP system specification in terms of its component Object-Z classes by using the laws of the the CSP operators together with the logic for Object-Z.

The anammox case - A new experimental manifesto for microbiological eco-physiology

The anaerobic ammonium oxidation process is a new process for ammonia removal from wastewater. It is also a new microbial physiology that was previously believed to be impossible. The identification of Candidatus Brocadia anammoxidans and its relatives as the responsible bacteria was only possible with the development of a new experimental approach. That approach is the focus of this paper. The approach is a modernisation of the Winogradsky/Beyerinck strategy of selective enrichment and is based on the introduction of the molecular toolbox and modern bioreactor engineering to microbial ecology. It consists of five steps: (1) postulation of an ecological niche based on thermodynamic considerations and macro-ecological field data; (2) engineering of this niche into a laboratory bioreactor for enrichment culture; (3) black-box physiological characterisation of the enrichment culture as a whole; (4) phylogenetic characterisation of the enriched community using molecular tools; (5) physical separation of the dominant members of the enrichment culture using gradient centrifugation and the identification of the species of interest in accordance with Koch's postulates; (6) verification of the in situ importance of these species in the actual ecosystems. The power of this approach is illustrated with a case study: the identification of the planctomycetes responsible for anaerobic ammonium oxidation. We argue that this was impossible using molecular ecology or conventional 'cultivation based techniques' alone. We suggest that the approach might also be used for the microbiological study of many interesting microbes such as anaerobic methane oxidisers.

Cue competition between elementary trained stimuli: US miscuing, interference, and US omission

The present series of experiments was designed to assess whether rule-based accounts of Pavlovian learning can account for cue competition effects observed after elemental training. All experiments involved initial differential conditioning training with A-US and B alone presentations. Miscuing refers to the fact that responding to A is impaired after one B-US presentation whereas interference is the impairment of responding to A after presentation of C-US pairings. Omission refers to the effects on B of A alone presentations. Experiments 1-2a provided clear evidence for miscuing whereas interference was not found after 1, 5 or 10 C-US pairings. Moreover, Experiments 3 and 3a found only weak evidence for interference in an A-US, B I C-US, D I A design used previously to show the effect. Experiments 4 and 5 failed to find any effect of US omission after one or five omission trials. The present results indicate that miscuing is more robust than is the interference effect. Moreover, the asymmetrical effects of US miscuing and US omission are difficult to accommodate within rule-based accounts of Pavlovian conditioning. (C) 2002 Elsevier Science (USA). All rights reserved.

Medicis: a personal health care assistant

The relation between patient and physician in most modern Health Care Systems is sparse, limited in time and very inflexible. On the other hand, and in contradiction with several recent studies, most physicians do not rely their patient diagnostics evaluations on intertwined psychological and social nature factors. Facing these problems and trying to improve the patient/physician relation we present a mobile health care solution to improve the interaction between the physician and his patients. The solution serves not only as a privileged mean of communication between physicians and patients but also as an evolutionary intelligent platform delivering a mobile rule based system.

Rastreio neonatal dos défices do ciclo da ureia em Portugal

Os défices do ciclo da ureia são um grupo de doenças hereditárias do metabolismo caracterizadas fundamentalmente por uma acumulação de amónia. Clinicamente o espectro é muito alargado, com formas de apresentação no período neonatal até situações mais moderadas de apresentação tardia em adultos. O tratamento é fundamentalmente de base nutricional e traduz-se numa redução significativa da mortalidade e morbilidade. Com a introdução da espectrometria de massa nos laboratórios de rastreio neonatal em meados dos anos 90, passou a ser possível quantificar alguns intermediários do ciclo, o que associado à existência de um intervalo livre e um tratamento eficaz, permitiu o rastreio de algumas das doenças deste grupo. Em 2004 iniciou-se em Portugal o rastreio dos défices do ciclo da ureia, tendo-se rastreado até ao presente, 988 687 recém-nascidos e identificado 19 casos positivos. Recentes desenvolvimentos técnicos vieram possibilitar a quantificação de novos marcadores, mais concretamente do ácido orótico, o que abre a possibilidade de rastrear o défice em ornitina transcarbamilase, o défice do ciclo da ureia mais frequente. Os autores apresentam a situação atual do rastreio dos défices do ciclo da ureia e as perspetivas em virtude dos novos desenvolvimentos técnicos.

Fungal and microbial volatile organic compounds exposure assessment in a waste sorting plant

In the management of solid waste, pollutants over a wide range are released with different routes of exposure for workers. The potential for synergism among the pollutants raises concerns about potential adverse health effects, and there are still many uncertainties involved in exposure assessment. In this study, conventional (culture-based) and molecular real-time polymerase chain reaction (RTPCR) methodologies were used to assess fungal air contamination in a waste-sorting plant which focused on the presence of three potential pathogenic/toxigenic fungal species: Aspergillus flavus, A. fumigatus, and Stachybotrys chartarum. In addition, microbial volatile organic compounds (MVOC) were measured by photoionization detection. For all analysis, samplings were performed at five different workstations inside the facilities and also outdoors as a reference. Penicillium sp. were the most common species found at all plant locations. Pathogenic/toxigenic species (A. fumigatus and S. chartarum) were detected at two different workstations by RTPCR but not by culture-based techniques. MVOC concentration indoors ranged between 0 and 8.9 ppm (average 5.3 ± 3.16 ppm). Our results illustrated the advantage of combining both conventional and molecular methodologies in fungal exposure assessment. Together with MVOC analyses in indoor air, data obtained allow for a more precise evaluation of potential health risks associated with bioaerosol exposure. Consequently, with this knowledge, strategies may be developed for effective protection of the workers.

Direct multisearch for multiobjective optimization

In practical applications of optimization it is common to have several conflicting objective functions to optimize. Frequently, these functions are subject to noise or can be of black-box type, preventing the use of derivative-based techniques. We propose a novel multiobjective derivative-free methodology, calling it direct multisearch (DMS), which does not aggregate any of the objective functions. Our framework is inspired by the search/poll paradigm of direct-search methods of directional type and uses the concept of Pareto dominance to maintain a list of nondominated points (from which the new iterates or poll centers are chosen). The aim of our method is to generate as many points in the Pareto front as possible from the polling procedure itself, while keeping the whole framework general enough to accommodate other disseminating strategies, in particular, when using the (here also) optional search step. DMS generalizes to multiobjective optimization (MOO) all direct-search methods of directional type. We prove under the common assumptions used in direct search for single objective optimization that at least one limit point of the sequence of iterates generated by DMS lies in (a stationary form of) the Pareto front. However, extensive computational experience has shown that our methodology has an impressive capability of generating the whole Pareto front, even without using a search step. Two by-products of this paper are (i) the development of a collection of test problems for MOO and (ii) the extension of performance and data profiles to MOO, allowing a comparison of several solvers on a large set of test problems, in terms of their efficiency and robustness to determine Pareto fronts.

Decision support system with incomplete and domain incoherent information management

Many of the most common human functions such as temporal and non-monotonic reasoning have not yet been fully mapped in developed systems, even though some theoretical breakthroughs have already been accomplished. This is mainly due to the inherent computational complexity of the theoretical approaches. In the particular area of fault diagnosis in power systems however, some systems which tried to solve the problem, have been deployed using methodologies such as production rule based expert systems, neural networks, recognition of chronicles, fuzzy expert systems, etc. SPARSE (from the Portuguese acronym, which means expert system for incident analysis and restoration support) was one of the developed systems and, in the sequence of its development, came the need to cope with incomplete and/or incorrect information as well as the traditional problems for power systems fault diagnosis based on SCADA (supervisory control and data acquisition) information retrieval, namely real-time operation, huge amounts of information, etc. This paper presents an architecture for a decision support system, which can solve the presented problems, using a symbiosis of the event calculus and the default reasoning rule based system paradigms, insuring soft real-time operation with incomplete, incorrect or domain incoherent information handling ability. A prototype implementation of this system is already at work in the control centre of the Portuguese Transmission Network.

Long-term modifications of coastal defences enhance marine biodiversity

Realization that hard coastal infrastructures support lower biodiversity than natural habitats has prompted a wealth of research seeking to identify design enhancements offering ecological benefits. Some studies showed that artificial structures could be modified to increase levels of diversity. Most studies, however, only considered the short-term ecological effects of such modifications, even though reliance on results from short-term studies may lead to serious misjudgements in conservation. In this study, a sevenyear experiment examined how the addition of small pits to otherwise featureless seawalls may enhance the stocks of a highly-exploited limpet. Modified areas of the seawall supported enhanced stocks of limpets seven years after the addition of pits. Modified areas of the seawall also supported a community that differed in the abundance of littorinids, barnacles andmacroalgae compared to the controls. Responses to different treatments (numbers and size of pits) were speciesspecific and, while some species responded directly to differences among treatments, others might have responded indirectly via changes in the distribution of competing species. This type of habitat enhancement can have positive long-lasting effects on the ecology of urban seascapes.Understanding of species interactions could be used to develop a rule-based approach to enhance biodiversity.

True and fair view: um conceito de geometria variável

De acordo com o parágrafo 46 da estrutura concetual do SNC as demonstrações financeiras devem mostrar uma imagem verdadeira e apropriada, ou apresentar apropriadamente, a posição financeira, o desempenho e as alterações da posição financeira de uma entidade. Todavia, a estrutura concetual do SNC não interpreta diretamente tais conceitos, situação que se pode refletir na qualidade do reporting financeiro apresentado e divulgado. O referencial contabilístico português apresenta, como equivalentes, as noções de true and fair view, presentfairly, fairly reflect ou fair reflection, e silenciando toda a polémica envolvente às expressões apresentadas. Com efeito, a primeira expressão é identificada, com a União Europeia, onde a apresentação e divulgação da informação financeira é baseada num conjunto de princípios — principies — based standards — e pressupõe o exercício de um julgamento, enquanto que as três expressões seguintes traduzem o standard de reporting financeiro, para os Estados Unidos, tendo subjacente a abordagem designado por — rule based standards — A não abordagem do SNC levou-nos a refletir sobre o assunto apresentado, apresentando uma análise multifacetada do conceito.

A influência dos jogos matemáticos na predisposição dos alunos para a matemática e na sua aprendizagem

Relatório de estágio apresentado à Escola Superior de Educação de Lisboa para obtenção de grau de mestre em Ensino do 1.º e do 2.º Ciclo do Ensino Básico

Algorithms and methodologies for decision support in energy efficiency on buildings

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 Electrotécnica e de Computadores

Multiple sequence alignment correction using constraints

Trabalho apresentado no âmbito do European Master in Computational Logics, como requisito parcial para obtenção do grau de Mestre em Computational Logics

New analytical methodologies for doping control – detection of anabolic androgenic steroids in human urine

Dissertation submitted to Faculdade de Ciências e Tecnologia - Universidade Nova de Lisboa in fulfilment of the requirements for the degree of Doctor of Philosophy (Biochemistry - Biotechnology)

Combining open and closed world reasoning for the semantic web

Dissertação para obtenção do Grau de Doutor em Informática