An approach for design and analysis of User-centric Communication Middleware

Today, the development of domain-specific communication applications is both time-consuming and error-prone because the low-level communication services provided by the existing systems and networks are primitive and often heterogeneous. Multimedia communication applications are typically built on top of low-level network abstractions such as TCP/UDP socket, SIP (Session Initiation Protocol) and RTP (Real-time Transport Protocol) APIs. The User-centric Communication Middleware (UCM) is proposed to encapsulate the networking complexity and heterogeneity of basic multimedia and multi-party communication for upper-layer communication applications. And UCM provides a unified user-centric communication service to diverse communication applications ranging from a simple phone call and video conferencing to specialized communication applications like disaster management and telemedicine. It makes it easier to the development of domain-specific communication applications. The UCM abstraction and API is proposed to achieve these goals. The dissertation also tries to integrate the formal method into UCM development process. The formal model is created for UCM using SAM methodology. Some design errors are found during model creation because the formal method forces to give the precise description of UCM. By using the SAM tool, formal UCM model is translated to Promela formula model. In the dissertation, some system properties are defined as temporal logic formulas. These temporal logic formulas are manually translated to promela formulas which are individually integrated with promela formula model of UCM and verified using SPIN tool. Formal analysis used here helps verify the system properties (for example multiparty multimedia protocol) and dig out the bugs of systems.

Formal verification and testing of software architectural models

Ensuring the correctness of software has been the major motivation in software research, constituting a Grand Challenge. Due to its impact in the final implementation, one critical aspect of software is its architectural design. By guaranteeing a correct architectural design, major and costly flaws can be caught early on in the development cycle. Software architecture design has received a lot of attention in the past years, with several methods, techniques and tools developed. However, there is still more to be done, such as providing adequate formal analysis of software architectures. On these regards, a framework to ensure system dependability from design to implementation has been developed at FIU (Florida International University). This framework is based on SAM (Software Architecture Model), an ADL (Architecture Description Language), that allows hierarchical compositions of components and connectors, defines an architectural modeling language for the behavior of components and connectors, and provides a specification language for the behavioral properties. The behavioral model of a SAM model is expressed in the form of Petri nets and the properties in first order linear temporal logic.^ This dissertation presents a formal verification and testing approach to guarantee the correctness of Software Architectures. The Software Architectures studied are expressed in SAM. For the formal verification approach, the technique applied was model checking and the model checker of choice was Spin. As part of the approach, a SAM model is formally translated to a model in the input language of Spin and verified for its correctness with respect to temporal properties. In terms of testing, a testing approach for SAM architectures was defined which includes the evaluation of test cases based on Petri net testing theory to be used in the testing process at the design level. Additionally, the information at the design level is used to derive test cases for the implementation level. Finally, a modeling and analysis tool (SAM tool) was implemented to help support the design and analysis of SAM models. The results show the applicability of the approach to testing and verification of SAM models with the aid of the SAM tool.^

Formal verification and testing of software architectural models

Ensuring the correctness of software has been the major motivation in software research, constituting a Grand Challenge. Due to its impact in the final implementation, one critical aspect of software is its architectural design. By guaranteeing a correct architectural design, major and costly flaws can be caught early on in the development cycle. Software architecture design has received a lot of attention in the past years, with several methods, techniques and tools developed. However, there is still more to be done, such as providing adequate formal analysis of software architectures. On these regards, a framework to ensure system dependability from design to implementation has been developed at FIU (Florida International University). This framework is based on SAM (Software Architecture Model), an ADL (Architecture Description Language), that allows hierarchical compositions of components and connectors, defines an architectural modeling language for the behavior of components and connectors, and provides a specification language for the behavioral properties. The behavioral model of a SAM model is expressed in the form of Petri nets and the properties in first order linear temporal logic. This dissertation presents a formal verification and testing approach to guarantee the correctness of Software Architectures. The Software Architectures studied are expressed in SAM. For the formal verification approach, the technique applied was model checking and the model checker of choice was Spin. As part of the approach, a SAM model is formally translated to a model in the input language of Spin and verified for its correctness with respect to temporal properties. In terms of testing, a testing approach for SAM architectures was defined which includes the evaluation of test cases based on Petri net testing theory to be used in the testing process at the design level. Additionally, the information at the design level is used to derive test cases for the implementation level. Finally, a modeling and analysis tool (SAM tool) was implemented to help support the design and analysis of SAM models. The results show the applicability of the approach to testing and verification of SAM models with the aid of the SAM tool.

Embedded DSP-Based Compact Fuzzy System and Its Application for Induction-Motor V/f Speed Control

This paper presents a compact embedded fuzzy system for three-phase induction-motor scalar speed control. The control strategy consists in keeping constant the voltage-frequency ratio of the induction-motor supply source. A fuzzy-control system is built on a digital signal processor, which uses speed error and speed-error variation to change both the fundamental voltage amplitude and frequency of a sinusoidal pulsewidth modulation inverter. An alternative optimized method for embedded fuzzy-system design is also proposed. The controller performance, in relation to reference and load-torque variations, is evaluated by experimental results. A comparative analysis with conventional proportional-integral controller is also achieved.

Evolution of genotypes of Group A streptococci from colonization and infection

Dissertação para obtenção do Grau de Doutor em Biologia

Efficiency of strengthening techniques assessed for existing masonry buildings

The Azores archipelago is a zone with a vast cultural heritage, presenting a building stock mainly constructed in traditional stone masonry. It is known that this type of construction exhibits poor behaviour under seismic excitations; however it is extensively used in seismic prone areas, such as this case. The 9th of July of 1998 earthquake was the last seismic event in the islands, leaving many traditional stone constructions severely damaged or totally destroyed. This scenario led to an effort by the local government of improving the seismic resistance of these constructions, with the application of several reinforcement techniques. This work aims to study some of the most used reinforcement schemes after the 1998 earthquake, and to assess their effectiveness in the mitigation of the construction’s seismic vulnerability. A brief evaluation of the cost versus benefit of these retrofitting techniques is also made, seeking to identify those that are most suitable for each building typology. Thus, it was sought to analyze the case of real structures with different geometrical and physical characteristics, by establishing a comparison between the seismic performance of reinforced and non-reinforced structures. The first section contains the analysis of a total of six reinforcement scenarios for each building chosen. Using the recorded 1998 earthquake accelerograms, a linear time-history analysis was performed for each reinforcement scenario. A comparison was then established between the maximum displacements, inter-storey drift and maximum stress obtained, in order to evaluate the global seismic response of each reinforced structure. In the second part of the work, the examination of the performance obtained in the previous section, in relation to the cost of implementing each reinforcement technique, allowed to draw conclusions concerning the viability of implementing each reinforcement method, based on the book value of the buildings in study.

Approximating subtree distances between Phylogenies

We give a 5-approximation algorithm to the rooted Subtree-Prune-and-Regraft (rSPR) distance between two phylogenies, which was recently shown to be NP-complete by Bordewich and Semple [5]. This paper presents the first approximation result for this important tree distance. The algorithm follows a standard format for tree distances such as Rodrigues et al. [24] and Hein et al. [13]. The novel ideas are in the analysis. In the analysis, the cost of the algorithm uses a \cascading" scheme that accounts for possible wrong moves. This accounting is missing from previous analysis of tree distance approximation algorithms. Further, we show how all algorithms of this type can be implemented in linear time and give experimental results.

Propagation connectivity of random hypergraphs

We study the concept of propagation connectivity on random 3-uniform hypergraphs. This concept is inspired by a simple linear time algorithm for solving instances of certain constraint satisfaction problems. We derive upper and lower bounds for the propagation connectivity threshold, and point out some algorithmic implications.

Modeling of hybrid systems by piecewise decomposition

Piecewise linear models systems arise as mathematical models of systems in many practical applications, often from linearization for nonlinear systems. There are two main approaches of dealing with these systems according to their continuous or discrete-time aspects. We propose an approach which is based on the state transformation, more particularly the partition of the phase portrait in different regions where each subregion is modeled as a two-dimensional linear time invariant system. Then the Takagi-Sugeno model, which is a combination of local model is calculated. The simulation results show that the Alpha partition is well-suited for dealing with such a system

Subsampling the mean of heavy-tailed dependent observations

We establish the validity of subsampling confidence intervals for themean of a dependent series with heavy-tailed marginal distributions.Using point process theory, we study both linear and nonlinear GARCH-liketime series models. We propose a data-dependent method for the optimalblock size selection and investigate its performance by means of asimulation study.

Planning under partial observability by classical replanning: theory and experiments

Planning with partial observability can be formulated as a non-deterministic search problem in belief space. The problem is harder than classical planning as keeping track of beliefs is harder than keeping track of states, and searching for action policies is harder than searching for action sequences. In this work, we develop a framework for partial observability that avoids these limitations and leads to a planner that scales up to larger problems. For this, the class of problems is restricted to those in which 1) the non-unary clauses representing the uncertainty about the initial situation are nvariant, and 2) variables that are hidden in the initial situation do not appear in the body of conditional effects, which are all assumed to be deterministic. We show that such problems can be translated in linear time into equivalent fully observable non-deterministic planning problems, and that an slight extension of this translation renders the problem solvable by means of classical planners. The whole approach is sound and complete provided that in addition, the state-space is connected. Experiments are also reported.

Increasing prehospital emergency medical service interventions for nursing home residents.

QUESTION: In the ageing European population, the proportion of interventions by the emergency medical services (EMS) for elderly patients is increasing, but little is known about the recent trend of EMS interventions in nursing homes. The aim of this analysis was to describe the evolution of the incidence of requests for prehospital EMS interventions for nursing home residents aged 65 years and over between 2004 and 2013. METHODS: A prospective population-based register of routinely collected data for each EMS intervention in the Canton of Vaud. Linear time trends of incidence of requests to the EMS in nursing homes were calculated and stratified by age categories. RESULTS: The number of ambulance interventions in nursing homes for people aged 65 years and over (65+) increased by 68.9% (1124‒1898) between 2004 and 2013. A significant linear increase of the annual incidence of requests to EMS per 1,000 nursing home residents was found for people aged 65-79 (10.2, 95% confidence interval [CI] 6.2-14.2), 80-89 (16.5, 95% CI 14.0-19.0) and over 90 (12.1, 95% CI 5.8-18.4). EMS interventions in nursing home residents who required an emergency physician increased during the same period by 205.6% (from 106 to 324), representing an increase from 2% to 7% of all emergency physician interventions in the Canton. CONCLUSIONS: Our results confirmed an important increase in the incidence of EMS interventions in nursing homes during the last decade, far exceeding the actual increase of the nursing home population during the same period. This evolution represents an important opportunity to reconsider the EMS missions in the context of an ageing society.

A Gradient based algorithm for blind inversion of Wiener System using multi-variate score functions

A Wiener system is a linear time-invariant filter, followed by an invertible nonlinear distortion. Assuming that the input signal is an independent and identically distributed (iid) sequence, we propose an algorithm for estimating the input signal only by observing the output of the Wiener system. The algorithm is based on minimizing the mutual information of the output samples, by means of a steepest descent gradient approach.

Long term trends in prevalence of neural tube defects in Europe: population based study.

STUDY QUESTION: What are the long term trends in the total (live births, fetal deaths, and terminations of pregnancy for fetal anomaly) and live birth prevalence of neural tube defects (NTD) in Europe, where many countries have issued recommendations for folic acid supplementation but a policy for mandatory folic acid fortification of food does not exist? METHODS: This was a population based, observational study using data on 11 353 cases of NTD not associated with chromosomal anomalies, including 4162 cases of anencephaly and 5776 cases of spina bifida from 28 EUROCAT (European Surveillance of Congenital Anomalies) registries covering approximately 12.5 million births in 19 countries between 1991 and 2011. The main outcome measures were total and live birth prevalence of NTD, as well as anencephaly and spina bifida, with time trends analysed using random effects Poisson regression models to account for heterogeneities across registries and splines to model non-linear time trends. SUMMARY ANSWER AND LIMITATIONS: Overall, the pooled total prevalence of NTD during the study period was 9.1 per 10 000 births. Prevalence of NTD fluctuated slightly but without an obvious downward trend, with the final estimate of the pooled total prevalence of NTD in 2011 similar to that in 1991. Estimates from Poisson models that took registry heterogeneities into account showed an annual increase of 4% (prevalence ratio 1.04, 95% confidence interval 1.01 to 1.07) in 1995-99 and a decrease of 3% per year in 1999-2003 (0.97, 0.95 to 0.99), with stable rates thereafter. The trend patterns for anencephaly and spina bifida were similar, but neither anomaly decreased substantially over time. The live birth prevalence of NTD generally decreased, especially for anencephaly. Registration problems or other data artefacts cannot be excluded as a partial explanation of the observed trends (or lack thereof) in the prevalence of NTD. WHAT THIS STUDY ADDS: In the absence of mandatory fortification, the prevalence of NTD has not decreased in Europe despite longstanding recommendations aimed at promoting peri-conceptional folic acid supplementation and existence of voluntary folic acid fortification. FUNDING, COMPETING INTERESTS, DATA SHARING: The study was funded by the European Public Health Commission, EUROCAT Joint Action 2011-2013. HD and ML received support from the European Commission DG Sanco during the conduct of this study. No additional data available.

Distribution and role of macrophytes in coastal lagoons : implications of critical shifts

Crossroads, crucibles and refuges are three words that may describe natural coastal lagoon environments. The words refer to the complex mix of marine and terrestrial influences, prolonged dilution due to the semi-enclosed nature and the function of a habitat for highly diverse plant and animal communities, some of which are endangered. To attain a realistic picture of the present situation, high vulnerability to anthropogenic impact should be added to the description. As the sea floor in coastal lagoons is usually entirely photic, macrophyte primary production is accentuated compared with open sea environments. There is, however, a lack of proper knowledge on the importance of vegetation for the general functioning of coastal lagoon ecosystems. The aim of this thesis is to assess the role of macrophyte diversity, cover and species identity over temporal and spatial scales for lagoon functions, and to determine which steering factors primarily restrict the qualitative and quantitative composition of vegetation in coastal lagoons. The results are linked to patterns of related trophic levels and the indicative potential of vegetation for assessment of general conditions in coastal lagoons is evaluated. This thesis includes five field studies conducted in flads and glo-flads in the brackish water northern Baltic Sea. Flads and glo-flads are defined as a Baltic variety of coastal lagoons, which due to an inlet threshold and post-glacial landuplift slowly will be isolated from the open sea. This process shrinks inlet size, increases exposure and water retention, and is called habitat isolation. The studied coastal lagoons are situated in the archipelago areas of the eastern coast of Sweden, the Åland Islands and the south-west mainland of Finland, where land-uplift amounts to ca. 5 mm/ per year. Out of 400 evaluated sites, a total of 70 lagoons varying in inlet size, archipelago position and anthropogenic influence to cover for essential environmental variation were chosen for further inventory. Vegetation composition, cover and richness were measured together with several hydrographic and morphometric variables in the lagoons both seasonally and inter-annually to cover for general regional, local and temporal patterns influencing lagoon and vegetation development. On smaller species-level scale, the effects of macrophyte species identity and richness for the fish habitat function were studied by examining the influence of plant interaction on juvenile fish diversity. Thus, the active election of plant monoand polycultures by fish and the diversity of fish in the respective culture were examined and related to plant height and water depth. The lagoons and vegetation composition were found to experience a regime shift initiated by increased habitat isolation along with land-uplift. Vegetation composition altered, richness decreased and cover increased forming a less isolated and more isolated regime, named the vascular plant regime and charophyte regime, respectively according to the dominant vegetation. As total phosphorus in the water, turbidity and the impact of regional influences decreased in parallel, the dominance of charophytes and increasing cover seemed to buffer and stabilize conditions in the charophyte regime and indicated an increased functional role of vegetation for the lagoon ecosystem. The regime pattern was unaffected by geographical differences, while strong anthropogenic impact seemed to distort the pattern due to loss of especially Chara tomentosa L. in the charophyte regime. The regimes were further found unperturbed by short-time temporal fluctuations. In fact the seasonal and inter-annual dynamics reinforced the functional difference between the regimes by the increasing role of vegetation along habitat isolation and the resemblance to lake environments for the charophyte regime. For instance, greater total phosphorus and chlorophyll a concentrations in the water in the beginning of the season in the charophyte regime compared with the vascular plant regime presented a steeper reduction to even lower values than in the vascular plant regime along the season. Despite a regional importance and positive relationship of macrophyte diversity in relation to trophic diversity, species identity was underlined in the results of this thesis, especially with decreasing spatial scale. This result was supported partly by the increased role of charophytes in the functioning of the charophyte regime, but even more explicitly by the species-specific preference of juvenile fish for tall macrophyte monocultures. On a smaller species-level scale, tall plant species in monoculture seemed to be able to increase their length, indicating that negative selection forms preferred habitat structures, which increase fish diversity. This negative relationship between plant and fish diversity suggest a shift in diversity patterns among trohic levels on smaller scale. Thus, as diversity patterns seem complex and diverge among spatial scales, it might be ambiguous to extend the understanding of diversity relationships from one trophic level to the other. All together, the regime shift described here presents similarities to the regime development in marine lagoon environments and shallow lakes subjected to nutrient enrichment. However, due to nutrient buffering by vegetation with increased isolation and water retention as a consequence of the inlet threshold, the development seems opposite to the course along an eutrophication gradient described in marine lagoons lacking an inlet threshold, where the role of vegetation decreases. Thus, the results imply devastating consequences of inlet dredging (decreasing isolation) in terms of vegetation loss and nutrient release, and call for increased conservational supervision. Especially the red listed charophytes would suffer negatively from such interference and the consequences are likely to also deteriorate juvenile fish production. The fact that a new species to Finland, Chara connivens Salzm. Ex. Braun 1835 was discovered during this study further indicates a potential of the lagoons serving as refuges for rare species.