Formal methods for the development and verification of autonomic IT systems

This chapter explores ways in which rigorous mathematical techniques, termed formal methods, can be employed to improve the predictability and dependability of autonomic computing. Model checking, formal specification, and quantitative verification are presented in the contexts of conflict detection in autonomic computing policies, and of implementation of goal and utility-function policies in autonomic IT systems, respectively. Each of these techniques is illustrated using a detailed case study, and analysed to establish its merits and limitations. The analysis is then used as a basis for discussing the challenges and opportunities of this endeavour to transition the development of autonomic IT systems from the current practice of using ad-hoc methods and heuristic towards a more principled approach. © 2012, IGI Global.

A framework for transforming, analyzing, and realizing software designs in unified modeling language

Unified Modeling Language (UML) is the most comprehensive and widely accepted object-oriented modeling language due to its multi-paradigm modeling capabilities and easy to use graphical notations, with strong international organizational support and industrial production quality tool support. However, there is a lack of precise definition of the semantics of individual UML notations as well as the relationships among multiple UML models, which often introduces incomplete and inconsistent problems for software designs in UML, especially for complex systems. Furthermore, there is a lack of methodologies to ensure a correct implementation from a given UML design. The purpose of this investigation is to verify and validate software designs in UML, and to provide dependability assurance for the realization of a UML design.^ In my research, an approach is proposed to transform UML diagrams into a semantic domain, which is a formal component-based framework. The framework I proposed consists of components and interactions through message passing, which are modeled by two-layer algebraic high-level nets and transformation rules respectively. In the transformation approach, class diagrams, state machine diagrams and activity diagrams are transformed into component models, and transformation rules are extracted from interaction diagrams. By applying transformation rules to component models, a (sub)system model of one or more scenarios can be constructed. Various techniques such as model checking, Petri net analysis techniques can be adopted to check if UML designs are complete or consistent. A new component called property parser was developed and merged into the tool SAM Parser, which realize (sub)system models automatically. The property parser generates and weaves runtime monitoring code into system implementations automatically for dependability assurance. The framework in the investigation is creative and flexible since it not only can be explored to verify and validate UML designs, but also provides an approach to build models for various scenarios. As a result of my research, several kinds of previous ignored behavioral inconsistencies can be detected.^

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.

Uma abordagem para avaliação e tratamento de exceções propagadas no uso de serviços Web em .Net

High dependability, availability and fault-tolerance are open problems in Service-Oriented Architecture (SOA). The possibility of generating software applications by integrating services from heterogeneous domains, in a reliable way, makes worthwhile to face the challenges inherent to this paradigm. In order to ensure quality in service compositions, some research efforts propose the adoption of verification techniques to identify and correct errors. In this context, exception handling is a powerful mechanism to increase SOA quality. Several research works are concerned with mechanisms for exception propagation on web services, implemented in many languages and frameworks. However, to the extent of our knowledge, no works found evaluates these mechanisms in SOA with regard to the .NET framework. The main contribution of this paper is to evaluate and to propose exception propagation mechanisms in SOA to applications developed within the .NET framework. In this direction, this work: (i)extends a previous study, showing the need to propose a solution to the exception propagation in SOA to applications developed in .NET, and (ii) show a solution, based in model obtained from the results found in (i) and that will be applied in real cases through of faults injections and AOP techniques.

Metodologia para análise da dependabilidade de Smart Grids

Smart Grids are a new trend of electric power distribution, the future of current systems. These networks are continually being introduced in order to improve the reliability of systems, providing alternatives to energy supply and cost savings. Faced with increasing electric power grids complexity, the energy demand and the introduction of alternative sources to energy generation, all components of system require a fully integration in order to achieve high reliability and availability levels (dependability). The systematization of a Smart Grid from the Fault Tree formalism enable the quantitative evaluation of dependability of a specific scenario. In this work, a methodology for dependability evaluation of Smart Grids is proposed. A study of case is described in order to validate the proposal. With the use of this methodology, it is possible to estimate during the early design phase the reliability, availability of Smart Grid beyond to identify the critical points from the failure and repair distributions of components.

Stopping rules in Bayesian adaptive threshold estimation

Threshold estimation with sequential procedures is justifiable on the surmise that the index used in the so-called dynamic stopping rule has diagnostic value for identifying when an accurate estimate has been obtained. The performance of five types of Bayesian sequential procedure was compared here to that of an analogous fixed-length procedure. Indices for use in sequential procedures were: (1) the width of the Bayesian probability interval, (2) the posterior standard deviation, (3) the absolute change, (4) the average change, and (5) the number of sign fluctuations. A simulation study was carried out to evaluate which index renders estimates with less bias and smaller standard error at lower cost (i.e. lower average number of trials to completion), in both yes–no and two-alternative forced-choice (2AFC) tasks. We also considered the effect of the form and parameters of the psychometric function and its similarity with themodel function assumed in the procedure. Our results show that sequential procedures do not outperform fixed-length procedures in yes–no tasks. However, in 2AFC tasks, sequential procedures not based on sign fluctuations all yield minimally better estimates than fixed-length procedures, although most of the improvement occurs with short runs that render undependable estimates and the differences vanish when the procedures run for a number of trials (around 70) that ensures dependability. Thus, none of the indices considered here (some of which are widespread) has the diagnostic value that would justify its use. In addition, difficulties of implementation make sequential procedures unfit as alternatives to fixed-length procedures.

A guideline to improve qualitative social science publishing in ecology and conservation journals

A rise in qualitative social science manuscripts published in ecology and conservation journals speaks to the growing awareness of the importance of the human dimension in maintaining and improving Earth’s ecosystems. Given the rise in the quantity of qualitative social science research published in ecology and conservation journals, it is worthwhile quantifying the extent to which this research is meeting established criteria for research design, conduct, and interpretation. Through a comprehensive review of this literature, we aimed to gather and assess data on the nature and extent of information presented on research design published qualitative research articles, which could be used to judge research quality. Our review was based on 146 studies from across nine ecology and conservation journals. We reviewed and summarized elements of quality that could be used by reviewers and readers to evaluate qualitative research (dependability, credibility, confirmability, and transferability); assessed the prevalence of these elements in research published in ecology and conservation journals; and explored the implications of sound qualitative research reporting for applying research findings. We found that dependability and credibility were reasonably well reported, albeit poorly evolved in relation to critical aspects of qualitative social science such as methodology and triangulation, including reflexivity. Confirmability was, on average, inadequately accounted for, particularly with respect to researchers’ ontology, epistemology, or philosophical perspective and their choice of methodology. Transferability was often poorly developed in terms of triangulation methods and the suitability of the sample for answering the research question/s. Based on these findings, we provide a guideline that may be used to evaluate qualitative research presented in ecology and conservation journals to help secure the role of qualitative research and its application to decision making.

Genetic manipulation of Anopheles stephensi immunity to increase plasmodium falciparum salivary gland sporozoite infection levels

Human malaria is responsible for over 700,000 deaths a year. To stay abreast of the threat posed by the parasite, a constant stream of new drugs and vector control methods are required. This study focuses on a vaccine that has the potential to protect against parasite infection, but has been hindered by developmental challenges. In malaria prevention, live, attenuated, aseptic, Plasmodium falciparum sporozoites (PfSPZ) can be administered as a highly protective vaccine. PfSPZ are produced using adult female Anopheles stephensi mosquitoes as bioreactors. Production volume and cost of a PfSPZ vaccine for malaria are expected to be directly correlated with Plasmodium falciparum infection intensity in the salivary glands. The sporogonic development of Plasmodium falciparum in A. stephensi to fully infected salivary gland stage sporozoites is dictated by the activities of several known components of the mosquito’s innate immune system. Here I report on the use of genetic technologies that have been rarely, if ever, used in Anopheles stephensi Sda500 to increase the yield of sporozoites per mosquito and enhance vaccine production. By combining the Gal4/UAS bipartite system with in vivo expression of shRNA gene silencing, activity of the IMD signaling pathway downstream effector LRIM1, an antagonist to Plasmodium development, was reduced in the midgut, fat body, and salivary glands of A. stephensi. In infection studies using P. berghei and P. falciparum these transgenic mosquitoes consistently produced significantly more salivary gland stage sporozoites than wildtype controls, with increases in P. falciparum ranging from 2.5 to 10 fold. Using Plasmodium infection assays and qRT-PCR, two novel findings were identified. First, it was shown that 14 days post Plasmodium infection, transcript abundance of the IMD immune effector genes LRIM1, TEP1 and APL1c are elevated, in the salivary glands of A. stephensi, suggesting the salivary glands may play a role in post midgut defense against the parasite. Second, a non-pathogenic IMD signaling pathway response was observed which could suggest an alternative pathway for IMD activation. The information gained from these studies has significantly increased our knowledge of Plasmodium defense in A. stephensi and moreover could significantly improve vaccine production.

Ionospheric Turbulence Near the Upper Hybrid Layer: Theory and Experiment

The thesis presents experimental results, simulations, and theory on turbulence excited in magnetized plasmas near the ionosphere’s upper hybrid layer. The results include: The first experimental observations of super small striations (SSS) excited by the High-Frequency Auroral Research Project (HAARP) The first detection of high-frequency (HF) waves from the HAARP transmitter over a distance of 16x10^3 km The first simulations indicating that upper hybrid (UH) turbulence excites electron Bernstein waves associated with all nearby gyroharmonics Simulation results that indicate that the resulting bulk electron heating near the upper hybrid (UH) resonance is caused primarily by electron Bernstein waves parametrically excited near the first gyroharmonic. On the experimental side we present two sets of experiments performed at the HAARP heating facility in Alaska. In the first set of experiments, we present the first detection of super-small (cm scale) striations (SSS) at the HAARP facility. We detected density structures smaller than 30 cm for the first time through a combination of satellite and ground based measurements. In the second set of experiments, we present the results of a novel diagnostic implemented by the Ukrainian Antarctic Station (UAS) in Verdansky. The technique allowed the detection of the HAARP signal at a distance of nearly 16 Mm, and established that the HAARP signal was injected into the ionospheric waveguide by direct scattering off of dekameter-scale density structures induced by the heater. On the theoretical side, we present results of Vlasov simulations near the upper hybrid layer. These results are consistent with the bulk heating required by previous work on the theory of the formation of descending artificial ionospheric layers (DIALs), and with the new observations of DIALs at HAARP’s upgraded effective radiated power (ERP). The simulations that frequency sweeps, and demonstrate that the heating changes from a bulk heating between gyroharmonics, to a tail acceleration as the pump frequency is swept through the fourth gyroharmonic. These simulations are in good agreement with experiments. We also incorporate test particle simulations that isolate the effects of specific wave modes on heating, and we find important contributions from both electron Bernstein waves and upper hybrid waves, the former of which have not yet been detected by experiments, and have not been previously explored as a driver of heating. In presenting these results, we analyzed data from HAARP diagnostics and assisted in planning the second round of experiments. We integrated the data into a picture of experiments that demonstrated the detection of SSS, hysteresis effects in simulated electromagnetic emission (SEE) features, and the direct scattering of the HF pump into the ionospheric waveguide. We performed simulations and analyzed simulation data to build the understanding of collisionless heating near the upper hybrid layer, and we used these simulations to show that bulk electron heating at the upper hybrid layer is possible, which is required by current theories of DAIL formation. We wrote a test particle simulation to isolate the effects of electron Bernstein waves and upper hybrid layers on collisionless heating, and integrated this code to work with both the output of Vlasov simulations and the input for simulations of DAIL formation.

Early analysis of fault-attack effects for cryptographic hardware

International audience

A path-based framework for analyzing large markov models

Reliability and dependability modeling can be employed during many stages of analysis of a computing system to gain insights into its critical behaviors. To provide useful results, realistic models of systems are often necessarily large and complex. Numerical analysis of these models presents a formidable challenge because the sizes of their state-space descriptions grow exponentially in proportion to the sizes of the models. On the other hand, simulation of the models requires analysis of many trajectories in order to compute statistically correct solutions. This dissertation presents a novel framework for performing both numerical analysis and simulation. The new numerical approach computes bounds on the solutions of transient measures in large continuous-time Markov chains (CTMCs). It extends existing path-based and uniformization-based methods by identifying sets of paths that are equivalent with respect to a reward measure and related to one another via a simple structural relationship. This relationship makes it possible for the approach to explore multiple paths at the same time,· thus significantly increasing the number of paths that can be explored in a given amount of time. Furthermore, the use of a structured representation for the state space and the direct computation of the desired reward measure (without ever storing the solution vector) allow it to analyze very large models using a very small amount of storage. Often, path-based techniques must compute many paths to obtain tight bounds. In addition to presenting the basic path-based approach, we also present algorithms for computing more paths and tighter bounds quickly. One resulting approach is based on the concept of path composition whereby precomputed subpaths are composed to compute the whole paths efficiently. Another approach is based on selecting important paths (among a set of many paths) for evaluation. Many path-based techniques suffer from having to evaluate many (unimportant) paths. Evaluating the important ones helps to compute tight bounds efficiently and quickly.

2C-Cas9: a versatile tool for clonal analysis of gene function.

CRISPR/Cas9-mediated targeted mutagenesis allows efficient generation of loss-of-function alleles in zebrafish. To date, this technology has been primarily used to generate genetic knockout animals. Nevertheless, the study of the function of certain loci might require tight spatiotemporal control of gene inactivation. Here, we show that tissue-specific gene disruption can be achieved by driving Cas9 expression with the Gal4/UAS system. Furthermore, by combining the Gal4/UAS and Cre/loxP systems, we establish a versatile tool to genetically label mutant cell clones, enabling their phenotypic analysis. Our technique has the potential to be applied to diverse model organisms, enabling tissue-specific loss-of-function and phenotypic characterization of live and fixed tissues.

Operacionalização, no contexto da Força Aérea, de um Sistema Aéreo Autónomo Não-Tripulado Classe II para Vigilância Marítima e Busca e Salvamento

Os sistemas de aeronaves não-tripuladas (UAS-Unmanned Aircraft Systems) são uma realidade nos mais distintos cenários, especialmente nos militares. Atualmente, qualquer força armada credível possui sistemas de armas deste tipo ou planeia adquiri-los a curto prazo. Os militares encontram nesta nova valência do poder aéreo uma forma de ultrapassar alguns desafios colocados, essencialmente, por problemas de restrições económicas, humanas e técnicas. O aumento da mobilidade no transporte marítimo e no transporte aéreo, sobre os oceanos leva a que a zona económica exclusiva possa estar ameaçada, especialmente, a costa portuguesa, justificando-se assim, a existência dos meios necessários à sua vigilância de forma eficiente e eficaz. Para isso o país conta com o apoio Força Aérea Portuguesa, que pretende integrar no seu dispositivo nacional UAS Classe II (peso máximo à descolagem entre os 150kg e os 600kg) e desta forma levar a cabo, juntamente com as outras Unidades Aéreas já existentes, missões de Vigilância Marítima e Busca e Salvamento. Não obstante da capacidade já existente, torna-se relevante que sejam estudadas soluções que possam complementar a missão por ela levada a cabo visando, assim, uma otimização de recursos se possível. Tendo em conta esta moldura enquadradora, a presente dissertação, através de um estudo teórico, tem por objetivo geral analisar a potencial operacionalização de um UAS do tipo Classe II, no contexto das missões da Força Aérea. Para a elaboração deste estudo investigou-se e recolheu-se informações sobre a missão VIMAR e SAR. Para a recolha de dados foram elaboradas entrevistas a alguns militares experientes da organização. Os dados recolhidos possibilitaram a criação e respetiva análise de uma matriz SWOT, assim como tipificar missões, no âmbito da Vigilância Marítima e Busca e Salvamento, nas quais a integração do UAS com as aeronaves tripuladas se revelaria fulcral para o sucesso das operações aéreas. Provado o potencial, termina-se com a enumeração de diversas tarefas, sensores, equipamentos e requisitos que poderão servir de referência aos responsáveis pelo desenho e conceção do UAS.

Revolução Tecnológica no séc. XXI: Vulnerabilidades e Potencialidades

Esta dissertação procura analisar o fenómeno da revolução tecnológica no séc. XXI, e as suas vulnerabilidades e potencialidades. Em particular os desafios internacionais associados à crescente utilização de armamento autónomo pelos atores internacionais, tomando como caso de estudo o emprego, por parte dos Estados Unidos da América, de UAS, no combate ao terrorismo no Paquistão. Para isso, numa primeira fase analisou-se a evolução do sistema internacional, da estratégia militar e do poder aéreo, em articulação com a revolução tecnológica, particularizada nos UAS, contextualizando e enquadrando o seu aparecimento e desenvolvimento. Numa segunda fase, buscou-se a caracterização desta tipologia de armamento, analisando-se as principais questões legais e éticas aplicáveis, para aferir as suas vulnerabilidades e potencialidades. Na fase seguinte, procurou refletir-se sobre a relação desta tecnologia com o sistema internacional, com o objetivo de serem tecidas algumas considerações sobre a forma como a sua existência, comercialização e utilização poderá influenciar as relações entre atores internacionais, estatais e não estatais. Numa quarta e última fase, efetuou-se um estudo de caso, para analisar, em termos concretos, a utilização de UAS num cenário real – explorando as causas e consequências resultantes da sua utilização, os resultados obtidos e as tendências futuras – para, deste modo, melhor poder percecionar as suas potencialidades e vulnerabilidades. Com esta investigação chegou-se à conclusão que o percurso evolutivo dos UAS apresenta bastantes semelhanças com o da aviação tripulada. Para além disso constatou-se que, por se constituir numa tecnologia tão disruptiva, a utilização de UAS apresenta desafios éticos e legais, ainda que os mesmos não se apresentem, a priori, como ilegais ou antiéticos. Por fim, chegou-se à conclusão que, pelas suas características, e com o aumentar da sua proliferação, os UAS podem tornar-se num fator potenciador de conflitos, ainda que possam ter um efeito positivo na diminuição da sua dimensão e intensidade.