The diversity and range of the biological functions of non-coding RNA molecules (ncRNA) have only recently been realised, and phylogenetic analysis of the RNA genes that define these molecules can provide important insights into the evolutionary pressures acting on RNA genes, and can lead to a better understanding of the structure and function of ncRNA. An appropriate dataset is fundamental to any evolutionary analysis, and because existing RNA alignments are unsuitable, I describe a software pipeline to derive RNA gene datasets from genomic alignments. RNA gene prediction software has not previously been evaluated on such sets of known RNA genes, and I find that two popular methods fail to predict the genes in approximately half of the alignments. In addition, high numbers of predictions are made in flanking regions that lack RNA genes, and these results provide motivation for subsequent phylogenetic analyses, because a better understanding of RNA gene evolution should lead to improved methods of prediction. I analyse the RNA gene alignments with a range of evolutionary models of substitution and examine which models best describe the changes evident in the alignment. The best models are expected to provide more accurate trees, and their properties can also shed light on the evolutionary processes that occur in RNA genes. Comparing DNA and RNA substitution models is non-trivial however, because they describe changes between two different types of state, so I present a proof that allows models with different state spaces to be compared in a statistically valid manner. I find that a large proportion of RNA genes are well described by a single RNA model that includes parameters describing both nucleotides and RNA structure, highlighting the multiple levels of constraint that act on the genes. The choice of model affects the inference of a phylogenetic tree, suggesting that model selection, with RNA models, should be standard practice for analysis of RNA genes.

Doctor of Philosophy / Department of Computing and Information Sciences / Matthew Dwyer / John M. Hatcliff / To analyze an open system, one needs to close it with a definition of its environment, i.e., its execution context. Environment modeling is a significant challenge: environment models should be general enough to permit analysis of large portions of a system's possible behaviors, yet sufficiently precise to enable cost-effective reasoning. This thesis presents the Bandera Environment Generator (BEG), a toolset that automates generation of environment models to provide a restricted form of modular model checking of Java programs, where the module's source code is the subject of analysis along with an abstract model of the environment's behavior. Since the most general environments do not allow for tractable model checking, BEG has support for restricting the environment behavior based on domain-specific knowledge and assumptions about the environment behavior, which can be acquired from a variety of sources. When the environment code is not available, developers can encode their assumptions as an explicit formal specification. When the environment code is available, BEG employs static analyses to extract environment assumptions. Both specifications and static analyses can be tuned to reflect domain-specific knowledge, i.e., to describe domain-specific aspects of the environment behavior. Initially, BEG was implemented to handle general Java applications; later, it was extended to handle two specific domains: Graphical User Interfaces (GUI) implemented using the Swing/AWT libraries and web applications implemented using the J2EE framework. BEG was evaluated on several non-trivial case studies, including industrial applications from NASA, SUN, and Fujitsu. This thesis presents the domain-specific environment generation for GUI and web applications and describes BEG, its extensible architecture, usage, and how it can be extended to handle new domains.

No description available.

The thesis presents xavier, a novel tool-set for model checking of concurrent x86-64 assembly programs, via Partial Order Reduction (POR). xavier{} presents a realistic platform for systematically exploring and analyzing the state-space of concurrent x86 assembly programs, with the aim of detecting bugs via assertion failures in mainstream programs. Recently, a number of state-of-the-art model checking solutions have been introduced to efficiently explore the state-space of concurrent programs, using POR algorithms. However, such solutions are inefficient while analyzing stateful programming languages, such as the x86 assembly language, due to their low level of abstraction. To this end, xavier{} makes two contributions: i) a novel order-sensitivity based POR algorithm, that is applicable to concurrent x86 assembly, ii) an x86 machine-model that can accurately perform relaxed-consistency emulation of concurrent x86 assembly, without the need for any translations. We demonstrate the applicability of xavier{} through an evaluation on several classical mutual-exclusion benchmarks and mainstream benchmarks from the Userspace Read-Copy-Update (URCU) concurrency library, where the benchmarks range from $250-3700$ lines of x86 assembly. The framework is the first that supports systematic model checking of concurrent x86 assembly programs, and the effectiveness of xavier{} is demonstrated by reproducing a concurrency issue of threads accessing intermediate states in the URCU library, which stems from an assumption violation. / Master of Science / Sound verification of multi-threaded programs necessitate a systematic analysis of program state-spaces that result from thread interactions. Consequently, model-checking cite{godefroid1997model, Clarke2018} has been one of the prominent methods used to tackle the verification of multi-threaded programs. However, existing model-checking solutions are inefficient while analyzing stateful programming languages, such as the x86 assembly language, due to the solutions' higher level of abstraction. Therefore, the thesis presents xavier, a novel tool-set and a realistic platform for systematically exploring and analyzing the state-space of mainstream concurrent x86 assembly programs, with the aim of detecting bugs via assertion failures. To this end, xavier{} makes two contributions: i) a novel order-sensitivity based Partial Order Reduction algorithm, which efficiently explores the state space of concurrent x86 assembly, ii) an x86 machine-model that can accurately emulate the execution of concurrent x86 assembly, without the need for any translations. We demonstrate the applicability of xavier{} through an evaluation on several classical mutual-exclusion and mainstream benchmarks from the Userspace Read-Copy-Update (URCU) concurrency library, where the benchmarks range from $250-3700$ lines of x86 assembly. Moreover, we demonstrate the effectiveness of xavier{} by reproducing a concurrency issue in the URCU library, which manifests as a result of an assumption violation.

Model checking is a technique used to verify whether a model meets a given specification by exhaustively and automatically checking each reachable state in the model. It is a well-developed technique, but it suffers from some issues, perhaps most importantly the state space explosion problem. Models may contain so many states that must be checked means that the model checking procedure may be intractable. In this thesis we investigate whether procedure summaries can be used to improve the performance of model checking. Procedure summaries are concise representations of parts of a program, such as a function or method. We present a design and an implementation of dynamically generated summaries as an extension of Java PathFinder, a virtual machine executing Java bytecode that is able to model check programs written in Java by backtracking execution, to explore different schedulings etc. We find that our summaries incur an overhead that outweighs the benefits in most cases, but the approach shows promise in certain cases, in particular when stateless model checking is used. We also provide some statistics related to cases when our summaries are applicable that could provide guidance for future work within this field. / Model checking, eller modellkontroll, är en välkänd teknik inom programverifikation som används för att verifiera att en modell, ofta av ett program, uppfyller en given specifikation genom att undersöka alla nåbara tillstånd i modellen. Det är en välutvecklad teknik som lider av några brister, en av de viktigaste är det så kallade state space explosion-problemet. Modellerna kan bestå av så många olika tillstånd att \textit{model checking} inte går att använda. I den här rapporten undersöker vi om vi kan tillämpa så kallade procedur-sammanfattningar för att förbättra prestandan av model checking. Procedur-sammanfattningar är representationer av delar av program, till exempel metoder eller funktioner. Vi presenterar en design och implementation av dynamiskt genererade sammanfattningar i form av ett tillägg till Java PathFinder, en virtuell maskin som exekverar Java bytecode som kan utföra model checking genom att backa körningar för att till exempel utforska olika schemaläggningar. Våra procedur-sammanfattningar har i många fall en negativ effekt på körtid, men visar på lovande resultat i vissa fall, i synnerhet när så kallad stateless model checking används. Vi presenterar också resultat kopplat till fall när våra sammanfattningar är applicerbara som kan leda vägen för fortsatt arbete inom området.

Rapid prototyping (RP) is a set of fabrication technologies that are used to produce accurate parts directly from computer aided drawing (CAD) data. These technologies are unique in a way that they use an additive fabrication approach in which a three dimensional (3D) object is directly produced. In this thesis study, a RP application with a modular architecture is designed and implemented to satisfy the possible requirements of future rapid prototyping studies. After a functional classification, the developed RP software is divided into View, RP and Slice Modules. In the RP module, the process parameter selection and optimal build orientation determination steps are carried out. In the Slice Module, slicing and tool path generation steps are performed. View Module is used to visualize the inputs and outputs of the RP software. To provide 3D visualization support for View Module, a fully independent, open for development, high level 3D modeling environment and graphics library called Graphics Framework is developed. The resulting RP application is benchmarked with the RP software packages in the market according to their memory usage and process time. As a result of this benchmark, it is observed that the developed RP software has presented an equivalent performance with the other commercial RP applications and has proved its success.

This thesis deals with the design and implementation of Android application development tool based on model driven software development. The first part of the thesis is focused on general software development and next part on software development based on model driven development and executable UML. In next part Android platform, methods of Android application development and existing MDD tools are described. This thesis continues with the design of my own MDD tool for the creation of Android applications. The designed tool is realized like Gradle plugin and independent development environment using thisplugin. The designed tool is based on fUML and ALF language. The features and options of development tool are demonstrated by creation of example application.

L’innovation est un élément efficace pour répondre aux défis et perspectives imposés par les événements contemporains (mondialisation, concurrence, bouleversements politiques…). Des politiques liées aux stratégies d’innovation, des études sur les pratiques et les méthodes pour innover sont conduites par les entreprises et promues par les gouvernements. Afin de consolider la capacité à créer et innover, des recherches sont aujourd’hui axées sur les phases amont du processus d’innovation. Ces phases consistent à générer, évaluer et exploiter très tôt des innovations embryonnaires. Notre problématique de recherche concerne spécifiquement l’évaluation d’idées générées dans les phases amont. Les enjeux de cette action sont d’évaluer des idées très peu finalisées, en grandes quantités. Actuellement, le manque de méthodes adaptées, des restrictions de temps ou encore des budgets limités contraignent cette phase d’évaluation. Afin de pouvoir proposer une méthode d’aide à l’évaluation d’idées, nous réalisons une étude bibliographique puis proposons une démarche et des outils conduisant à une évaluation d’idées formalisée et instrumentée. Notre proposition permet d’appréhender les informations des évaluations réalisées et fournit des éléments de visualisation pour aider notamment les experts lors de cette action. Cette méthode s’est construite à partir d’analyses de situations professionnelles sur le terrain et nous a permis de proposer trois modèles. Ceux-ci ont été testés et expérimentés en milieu académique et industriel. Enfin, cette recherche s’est concrétisée par l’élaboration d’une maquette informatique nommée IdéoVal destinée à aider l’évaluation et la sélection d’idées / Innovation is an effective element to address the challenges and prospects imposed by the contemporary events (globalization, competition, political changes…). Innovation strategies, studies on the practices and methods to innovate are led by several companies and are promoted by the governments. In order to consolidate the capacity to create and innovate, current researches are focused on the early stages of the innovation process. These phases consist of generating, evaluating and exploiting embryonic innovations very early in the process. Our research problematic is specifically related to the evaluation of ideas generated in the early stages. The issues involving this action are to evaluate a large quantity of ideas that are not yet finalized. Currently, the lack of adapted methods, time restrictions or limited budgets constraint this evaluation stage. In order to propose a method for assisting ideas evaluation, we made a bibliographical study, and then we proposed an approach and tools leading to a formalized and instrumented evaluation of ideas. Our proposal enables the capitalization of the information from the evaluations carried out and provides a visualization of elements to, in particular, help the experts carry out this action. This method was built from the analyses of professional situations in the field and allowed us to propose three models. These models were tested in academic and industrial environments. Finally, this research was materialized by the elaboration of a software model called IdéoVal, which purpose is to help evaluate and select ideas

Made available in DSpace on 2016-06-02T19:05:57Z (GMT). No. of bitstreams: 1 4450.pdf: 5302294 bytes, checksum: a12e396d985ac3fe2e63b38cc999decf (MD5) Previous issue date: 2012-07-04 / Universidade Federal de Minas Gerais / Aspect-Oriented programming was created to modularize the so-called crosscutting concerns . Crosscutting concerns have some properties that cannot be fully modularized with the object-oriented paradigm. After that, aspect-oriented frameworks were created in order to make reuse of different concern codes easier. Among these frameworks, Crosscutting Frameworks are aspect-oriented frameworks specifically created for crosscutting concern code modularization, for instance, persistence, distribution, concurrency and business rules. Currently, these frameworks are usually distributed as source code and must be reused by extending classes, aspects and methods. Reusing these frameworks in code-level require application developers to worry about implementation issues, that affects understandability, productivity and quality of final software. In this thesis, the objective is to raise abstraction level by applying a new model-driven approach for crosscutting framework reuse, which also allows reusability during earlier development phases. Experiments were conducted in order to compare the productivity of the proposed process with the conventional reuse technique, which is based on source-code edition. It was identified that the proposed process has advantages during the reuse activity, however, no advantages were detected while maintaining an application coupled to a crosscutting framework. / A programação orientada a aspectos foi criada para permitir a modularização de um tipo de interesse de software denominado de interesse transversal , que não pode ser completamente modularizado com paradigmas como o orientado a objetos. Com o uso do paradigma orientado a aspectos, vários pesquisadores começaram a pesquisar como determinados interesses transversais poderiam ser modularizados de formas genéricas para aumentar suas possibilidades de reúso, fazendo surgir Frameworks Orientados a Aspectos e também o termo Frameworks Transversais. Framework Transversal é um tipo de framework orientado a aspectos que tem o objetivo de permitir o reúso de código de interesses transversais, como persistência, distribuição, concorrência ou regras de negócio. Em geral, esses frameworks são disponibilizados na forma de código-fonte e devem ser reusados por meio da edição de código. Realizar o reúso neste nível faz com que engenheiros de aplicação tenham que se preocupar com detalhes da implementação do framework, afetando o entendimento, a produtividade e a qualidade do software final. Neste trabalho, o objetivo é elevar o nível de abstração do processo de reúso de frameworks transversais, propondo um processo dirigido por modelos que permite iniciar o processo de reúso nas fases antecedentes à implementação. Experimentos foram realizados para comparar o tempo de aplicar no novo processo com o processo de edição de código-fonte. Foi identificado que o novo processo possui vantagens em diminuir o tempo para reusar os frameworks, porém, não foram encontradas vantagens durante a manutenção de aplicações acopladas a frameworks transversais.

When developing three phase motor drives, the best way to validate the desiredfunctionality is to connect the inverter to an actual electrical motor. However, when developingfunctions which are not directly involved in controlling the motor, it could bemore efficient to use a real-time software model of the motor. In this master thesis, the developmentand implementation of a software model of a permanent magnet synchronousmotor (PMSM) is presented. This model was based on general dynamic equations forPMSM in a rotating reference frame (dq-frame). The model was simulated and convertedto C code using model based software development in Mathworks Simulink. To providemore realistic performance of the model, a finite element analysis (FEA) was done of anactual PMSM using the software tool FEMM. This analysis resulted in data describingthe relation between flux linkage and current which, when added into to software model,limits the produced torque due to magnetic saturation. Both the FEMM model and thefinal software model was compared to a corresponding actual motor for validation andperformance testing. All this resulted in a fully functional software model which was executableon the inverter. In the comparison of FEMM model to the real motor, a deviationin produced torque was discovered. This led to the conclusion that the model needed to beimproved to perform more alike the real motor. However, for this application the modelwas considered good enough to be used in future software development projects. / N¨ar kontrollsystem till trefasmotorer utvecklas s°a ¨ar det mest vanliga och troligendet b¨asta s¨attet f¨or funktionsvalidering att k¨ora drivenheten kopplad mot en riktig elektriskmotor. D¨aremot, om funktioner som ej ¨ar direkt kopplade till sj¨alva drivningen av motornutvecklas, s°a kan det vara mer effektivt att ist¨allet anv¨anda en mjukvarumodell. I det h¨arexamensarbetet s°a presenteras en mjukvarumodell av en permanentmagnetiserad synkronmotor(PMSM). Modellen baserades p°a de generella ekvationerna f¨or PMSM och simuleradessamt kodgenererades i Mathworks verktyg Simulink. F¨or att g¨ora modellen mer realistisks°a kompletterades den med data som beskriver relationen mellan det l¨ankade fl¨odetoch str¨om f¨or att ¨aven ta h¨ansyn till magnetisk m¨attnad. Den informationen simuleradesfram i verktyget FEMMgenom fl¨odesber¨akningar p°a en specifik motor typ. Samma motortyp har ocks°a j¨amf¨orts med den slutgiltiga mjukvarumodellen med avseende p°a utvecklatvridmoment vilket resulterade i n°agot st¨orre skillnader ¨an f¨orv¨antat. Slutsatsen blevs°aledes att modellen beh¨over f¨orb¨attras f¨or att p°a ett b¨attre s¨att st¨amma ¨overens med verklighetenmen att den fungerar tillr¨ackligt bra f¨or den ¨amnade applikationen.