Abstract
The dynamic logic with binders D? was recently introduced as a suitable formalism to support a rigorous stepwise development method for reactive software. The commitment of this logic concerning bisimulation equivalence is, however, not satisfactory: the model class semantics of specifications in D? is not closed under bisimulation equivalence; there are D?-sentences that distinguish bisimulation equivalent models, i.e., D? does not enjoy the modal invariance property. This paper improves on these limitations by providing an observational semantics for dynamic logic with binders. This involves the definition of a new model category and of a more relaxed satisfaction relation. We show that the new logic D? ~ enjoys modal invariance and even the Hennessy-Milner property. Moreover, the new model category provides a categorical characterisation of bisimulation equivalence by observational isomorphism. Finally, we consider abstractor semantics obtained by closing the model class of a specification SP in D? under bisimulation equivalence. We show that, under mild conditions, abstractor semantics of SP in D? is the same as observational semantics of SP in D? ~.

Abstract
RESUMO - É fundamental conhecer hábitos alimentares e nutricionais de uma população, para poder intervir na promoção da saúde da mesma. Com este estudo epidemiológico transversal representativo da população portuguesa adulta (dados da SPCNA), pretendeu-se conhecer o padrão nutricional de ingestão quer energética quer em macronutrientes. Por entrevista individualizada (domicílio), registaram-se dados sociodemográficos e avaliou-se a ingestão alimentar, por questionário, das 24 h anteriores. Assim, os portugueses ingerem em média: 2.056 kcal/dia, 19,1% de proteínas, 31,3% de gordura, 45,8% de hidratos de carbono e 3,8% de etanol. Estes dados serão válidos para intervenções adequadas na saúde pública portuguesa.;ABSTRACT - Gathering knowledge about food and nutritional habits of a population is of the utmost importance since dietary intervention positively impacts health outcomes across the life span. With this transversal epidemiologic study representative of the adult Portuguese population (data from SPCNA), we tried to know the nutritional intake pattern (energy and macronutrients) of the Portuguese population. In an domiciliary individualized interview sociodemographic data were registered and food intake was evaluated by the 24-hour recall method. Portuguese energy intake, is on average, 2056 kcal/day, distributed by 19.1% of protein, 45.8% of carbohydrates and 31.3% of total fat, and 3.8% of ethanol. These data will be important to Portuguese public health interventions.

Abstract
In order to achieve underwater acoustic high data-rate and real time communications, it is essential to implement a system that operates both at high and wideband frequencies using digital modulations. Therefore, to reduce the time and cost of developing acoustic communications an emulator of a physical layer model was implemented, allowing to test in real time the performance of digital modulations. The model was composed of an emitter transducer, a hydrophone and the subaquatic medium and was integrated in a Field Programmable Gate Array (FPGA) in order to emulate the physical layer in the acoustic modem testing. The emitter transducer and the hydrophone models were designed to meet real prototype characteristics. The system prototype was implemented in order to compare the experimental trials results with those obtained in emulator, emulating the transmission of acoustic signals, using different types of digital modulations. The system was tested using Binary Phase-Shift Keying (BPSK), Binary Frequency Shift keying (BFSK) and Binary Amplitude Shift Keying (BASK) modulations with a 1 MHz carrier frequency resulting in a data rate of 125 kbps. It was verified that the implemented model represents a suitable approximation to the real subaquatic communication channel, allowing the evaluation of digital acoustic communications.

Abstract
Car safety is an essential feature of marketing strategies for automobile companies. In this work, a statistical analysis on crash tests is conducted based on data available from European New Car Assessment Programme (Euro NCAP). The research work developed in this chapter presents a statistical analysis of the information produced by Euro NCAP, using the SPSS and MATLAB software, and seeks to answer the following research questions: - are there statistically significant differences on adult occupant safety in the six years under study? - are there statistically significant differences among the best-selling car classes regarding safety in frontal collisions? - are electric and hybrid automobiles less secure than their traditional counterparts with respect to frontal collisions?

Abstract
IEC 61850 is a communication standard for electrical Substation Automation Systems (SAS). It defines both the information model and services used for communication between Intelligent Electronic Devices (IEDs) in a substation. The adoption of this standard brings several advantages for the design and operation of substations. The abstract data models defined in IEC 61850 can be mapped upon application protocols, such as MMS, GOOSE or SMV. These protocols can run upon TCP/IP networks or upon specific high speed Ethernet LANs, in order to match the timing requirements associated to protective relaying mechanisms. For the specific case of GOOSE messages, the standard specifies the use of VLANs (Virtual LANs) with priority tagging (IEEE 802.1q) to implement separate virtual networks with the appropriate message priority levels, in order to ensure the specified response times. The lack of adequate simulation models that enable the response time assessment of both SMV and GOOSE messages is one of the shortcomings of available simulation tools. In this paper, we propose simulation models for the IEC 61850 communication standard, targeting application that use GOOSE and SMV messages. This simulation models has been built upon OMNeT++/INET. The simulation results obtained from a typical IEC 61850 communication scenario show the effectiveness of the developed models. Some of these results have been experimentally validated.

Abstract
In massive data analysis, data usually come in streams. In the last years, several studies have investigated novelty detection in these data streams. Different approaches have been proposed and validated in many application domains. A review of the main aspects of these studies can provide useful information to improve the performance of existing approaches, allow their adaptation to new applications and help to identify new important issues to be addresses in future studies. This article presents and analyses different aspects of novelty detection in data streams, like the offline and online phases, the number of classes considered at each phase, the use of ensemble versus a single classifier, supervised and unsupervised approaches for the learning task, information used for decision model update, forgetting mechanisms for outdated concepts, concept drift treatment, how to distinguish noise and outliers from novelty concepts, classification strategies for data with unknown label, and how to deal with recurring classes. This article also describes several applications of novelty detection in data streams investigated in the literature and discuss important challenges and future research directions.