PROCESS algebras are a family of techniques used in formal specification and analysis of computer systems, specially when independent processes that perform and synchronize in parallel are concerned. The so-called concurrent systems. Circus is a process algebra that aggregates the expressiveness power for concurrent behaviors from CSP, along with the predicative data modelling aspects of Z. Recent publications have established a formal exhaustive symbolic testing theory for specifications modelled in Circus. Aiming to improve the feasibility of applying such tests in practical scenarios, it is convenient to look for criteria that reduces the number of test cases which, by the exhaustive nature of the approach, is often infinite. In the light of this, the work we present proposes the application of mutation testing techniques in Circus specifications, targeting the coverage of faults seeded by well-known mutation operators, along with operators designed with the particularities of the language in mind. Some contributions were produced in the pursuit of these goals, such as establishing a formal theory for mutation testing in Circus specifications and the implementation of a symbolic traces generator for the language. / ÁLGEBRAS de processos são uma família de técnicas de especificação e análise formal utilizadas em sistemas computacionais, especialmente em contextos de processos independentes, que atuam paralelamente e efetuam comunicação entre si. São os chamados sistemas concorrentes. Circus é uma álgebra de processos que agrega a capacidade de expressão de comportamentos concorrentes do CSP com a modelagem predicativa de dados da notação Z. Trabalhos recentes vêm estabelecer uma teoria para o teste simbólico exaustivo baseado em especificações modeladas em Circus. Com o objetivo de viabilizar a aplicação prática desses testes, é conveniente estudar critérios que reduzam o conjunto de casos de teste que, pela sua natureza exaustiva, torna-se frequentemente infinito. Neste sentido, o presente trabalho propõe a aplicação de técnicas de teste de mutação à partir de especificações Circus, visando a cobertura de falhas inseridas por meio de operadores de mutação já conhecidos, juntamente com operadores propostos especificamente para a linguagem. Algumas contribuições foram produzidas na busca destes objetivos, como o estabelecimento de uma teoria formal para a aplicação de teste de mutação em especificações Circus e a implementação de um gerador de rastros simbólicos para a mesma linguagem.

TLE proteins are a closely related family of vertebrate corepressors. They have no intrinsic DNA binding ability, but are recruited as transcriptional repressors by other sequence specific proteins. TLE proteins and their homologues in other species have been implicated in many developmental processes including neurogenesis, haematopoiesis and the formation of major organs. They have also been implicated in early lineage specification in vertebrates but a direct role in this has not been found in mammals. The aim of my PhD is therefore to analyse the function of TLE proteins in early lineage specification and cell fate decisions using mouse embryonic stem cells (ESCs) as a model. The investigation of this has previously been complicated, firstly by the large array of transcription factors that TLEs interact with and secondly by redundancy between similar TLE proteins hindering loss of function approaches. To circumvent these problems, I have used two complementary experimental strategies. The first was identification of point mutations in TLE1 that affect specific classes of DNA binding. Two of these mutations L743F and R534A were of particular interest and were reversibly overexpressed in ES cells to correlate phenotypes to biochemical activity. The second strategy was the mutation of the two primary TLC genes in ES cells and early mouse embryos, TLE3 and TLE4. Complementary evidence from these approaches revealed a role for TLEs in the promotion of ES cell differentiation by repression of pluripotency/self-renewal associated genes. Additionally, neural specification was increased by TLE1 expression especially by the TLE1 point mutations, highlighting opposing roles for negative effects on mesendodermal differentiation. Early mesoderm/primitive streak was increased by loss of TLE, probably through Wnt antagonism. Anterior endoderm was increased by reduced TLE, but a critical level of TLE was still necessary and TLE1 overexpression also upregulated some anterior endoderm markers suggesting both negative and positive roles for TLE proteins in this process.

O aumento crescente da complexidade dos sistemas computacionais criou a necessidade do uso de técnicas de descrição formal (TDFs) na definição, implementação e manutenção dos sistemas. Contudo, apenas a existência de técnicas de descrição formal não garante o eficiente emprego das mesmas na especificação dos sistemas. É necessária a existência de ferramentas que viabilizem o uso das TDFs de forma que estas possam ser efetivamente úteis no desenvolvimento de projetos. Este trabalho apresenta os resultados obtidos da construção de um ambiente de especificação gráfico, onde a TDF E-LOTOS (Enhancements to LOTOS) fornece os mecanismos que uma técnica de descrição deve possuir para viabilizar a consistência, verificação e validação de sistemas. A TDF é suportada através do emprego de uma nova versão gráfica para a sintaxe textual padrão de E-LOTOS. O principal objetivo deste trabalho é disponibilizar aos projetistas e desenvolvedores um ambiente de especificação onde a criação, implementação, teste e manutenção de sistemas sejam feitos de forma fácil, rápida, intuitiva e consistente. Para tal, uma nova sintaxe gráfica de E-LOTOS foi criada: o E-DART (Enhancements to DART). Foi desenvolvida também uma ferramenta que permite o uso de E-DART, o Editor E-DART. A nova sintaxe abstrai, através de diagramas, as complexidades naturais de E-LOTOS, permitindo uma compreensão mais intuitiva dos sistemas. Com o uso de E-DART as especificações construídas são validadas por uma TDF sem que o processo de criação torne-se complexo. No Editor E-DART, a rapidez na criação das especificações é alcançada com mecanismos de reuso de módulos, e com o emprego de recursos avançados de interação com o usuário. O reuso de módulos diminui o tempo total dispensado na criação de especificações porque as mesmas poderão utilizar partes já homologadas de outros sistemas, sem a necessidade de validação e testes, pois estes são procedimentos realizados anteriormente nas outras especificações. Os recursos avançados de interação, por outro lado, permitem que projetistas não familiarizados com E-LOTOS sejam ainda assim capazes de construir sistemas complexos. Além disso, profissionais que tenham experiência com a TDF têm acesso direto ao código textual E-LOTOS, o que lhes garante uma maior compreensão das especificações. / The increasing complexity of the computational systems has created the necessity of the use of formal description techniques (FDTs) in the systems definition, implementation and maintenance. However, only the existence of formal description techniques does not guarantee their efficient use in the systems specification. The existence of tools is necessary to make the use of the TDFFs possible in a way in which these techniques can be effectively useful in projects development. This work presents the results of the construction of a specification graphical environment, where E-LOTOS FDT (Enhancements to LOTOS) supplies the mechanisms that a description technique must possess to make possible the consistency, verification and validation of systems. The FDT is supported through the use of a new graphical version for the standard textual E-LOTOS syntax. The main goal of this work is to provide to designers and developers a specification environment where the creation, implementation, test and maintenance of systems are made in a easy form, fast, intuitive and consistent way. For such, a new graphical syntax of E-LOTOS was created: the E-DART (Enhancements to DART). A tool that allows the E-DART use was also developed, the E-DART Editor. The new syntax represents, through diagrams, the natural complexities of E-LOTOS, allowing a intuitive understanding of the systems. With the use of E-DART the specifications are still validated by a FDT, without turning their creation into a complex process. In the E-DART Editor, fast creation of the specifications is achieved with mechanisms of module reuse, and with the use of advanced user interaction resources. The reuse of module diminishes the total time used in the specifications creation because it will be possible to use parts already validated of other systems. The advanced interaction resources, on the other hand, allow that designers not familiarized with E-LOTOS to be able to construct complex systems. Moreover, professionals who have experience with the FDT have direct access to textual ELOTOS code, which guarantees an easier understanding of the specifications.

This diploma thesis deals with the areas of requirements management in large organizations, especially banks. Bank projects have their own characteristics, as well as the banking environment as such. The paper will analyze the problem of requirements management in general and during description of best practices and methodological procedures attention will be drawn to the peculiar characteristics of the banking environment. This thesis focuses mainly on methodological and personal aspects of requirements management - the role of the analyst and the requirements management methodology. One of the main goals is selection of requiremets management methodology suitable for use in banks. Other important objectives are the description of best practices and mapping of the description of requirements management in the most widely used software development methodologies. The paper can serve as a textbook for junior analysts and other team members, or as a reference guide. Well-educated analyst and knowledgeable project team members enhance probability of a successful completion of the project and objectives achievement within set deadlines, budget and to everyone's satisfaction.

The aim of the thesis entitled "Analysis of the quality management system and preparing the organization Parker Hannifin, Ltd. for certification according to ISO/TS 16949 " is an analysis of the current state of quality management system in an organization Parker Hannifin Ltd. in readiness for certification according to technical specification ISO/TS 16949. This thesis consists of two parts. The theoretical part is a comparison of ISO 9001, which already is in an organization, and ISO/TS 16949 the organization wants to implement. The practical part is focused on analyzing the current state of quality management system and comparing it with the requirements of ISO/TS 16949 to know how is organization prepared for certification. There are also recomendations how to meet this requirements.

La vérification automatique est aujourd'hui devenue un domaine central de recherche en informatique. Depuis plus de 25 ans, une riche théorie a été développée menant à de nombreux outils, à la fois académiques et industriels, permettant la vérification de propriétés booléennes - celles qui peuvent être soit vraies soit fausses. Les besoins actuels évoluent vers une analyse plus fine, c'est-à-dire plus quantitative. L'extension des techniques de vérification aux domaines quantitatifs a débuté depuis 15 ans avec les systèmes probabilistes. Cependant, de nombreuses autres propriétés quantitatives existent, telles que la durée de vie d'un équipement, la consommation énergétique d'une application, la fiabilité d'un programme, ou le nombre de résultats d'une requête dans une base de données. Exprimer ces propriétés requiert de nouveaux langages de spécification, ainsi que des algorithmes vérifiant ces propriétés sur une structure donnée. Cette thèse a pour objectif l'étude de plusieurs formalismes permettant de spécifier de telles propriétés, qu'ils soient dénotationnels - expressions régulières, logiques monadiques ou logiques temporelles - ou davantage opérationnels, comme des automates pondérés, éventuellement étendus avec des jetons. Un premier objectif de ce manuscript est l'étude de résultats d'expressivité comparant ces formalismes. En particulier, on donne des traductions efficaces des formalismes dénotationnels vers celui opérationnel. Ces objets, ainsi que les résultats associés, sont présentés dans un cadre unifié de structures de graphes. Ils peuvent, entre autres, s'appliquer aux mots et arbres finis, aux mots emboîtés (nested words), aux images ou aux traces de Mazurkiewicz. Par conséquent, la vérification de propriétés quantitatives de traces de programmes (potentiellement récursifs, ou concurrents), les requêtes sur des documents XML (modélisant par exemple des bases de données), ou le traitement des langues naturelles sont des applications possibles. On s'intéresse ensuite aux questions algorithmiques que soulèvent naturellement ces résultats, tels que l'évaluation, la satisfaction et le model checking. En particulier, on étudie la décidabilité et la complexité de certains de ces problèmes, en fonction du semi-anneau sous-jacent et des structures considérées (mots, arbres...). Finalement, on considère des restrictions intéressantes des formalismes précédents. Certaines permettent d'étendre l'ensemble des semi-anneau sur lesquels on peut spécifier des propriétés quantitatives. Une autre est dédiée à l'étude du cas spécial de spécifications probabilistes : on étudie en particulier des fragments syntaxiques de nos formalismes génériques de spécification générant uniquement des comportements probabilistes. / Automatic verification has nowadays become a central domain of investigation in computer science. Over 25 years, a rich theory has been developed leading to numerous tools, both in academics and industry, allowing the verification of Boolean properties - those that can be either true or false. Current needs evolve to a finer analysis, a more quantitative one. Extension of verification techniques to quantitative domains has begun 15 years ago with probabilistic systems. However, many other quantitative properties are of interest, such as the lifespan of an equipment, energy consumption of an application, the reliability of a program, or the number of results matching a database query. Expressing these properties requires new specification languages, as well as algorithms checking these properties over a given structure. This thesis aims at investigating several formalisms, equipped with weights, able to specify such properties: denotational ones - like regular expressions, first-order logic with transitive closure, or temporal logics - or more operational ones, like navigating automata, possibly extended with pebbles. A first objective of this thesis is to study expressiveness results comparing these formalisms. In particular, we give efficient translations from denotational formalisms to the operational one. These objects, and the associated results, are presented in a unified framework of graph structures. This permits to handle finite words and trees, nested words, pictures or Mazurkiewicz traces, as special cases. Therefore, possible applications are the verification of quantitative properties of traces of programs (possibly recursive, or concurrent), querying of XML documents (modeling databases for example), or natural language processing. Second, we tackle some of the algorithmic questions that naturally arise in this context, like evaluation, satisfiability and model checking. In particular, we study some decidability and complexity results of these problems depending on the underlying semiring and the structures under consideration (words, trees...). Finally, we consider some interesting restrictions of the previous formalisms. Some permit to extend the class of semirings on which we may specify quantitative properties. Another is dedicated to the special case of probabilistic specifications: in particular, we study syntactic fragments of our generic specification formalisms generating only probabilistic behaviors.

Com a presença cada vez maior de sistemas computacionais e novas tecnologias no cotidiano das pessoas, garantir que eles não falhem e funcionem corretamente tornou-se algo de extrema importância. Além de indicar a qualidade do sistema, assegurar seu bom funcionamento é essencial para se evitar perdas, desde financeiras até de vidas. Uma das técnicas utilizadas para esta finalidade é a chamada verificação formal de programas. A partir da especificação do sistema, descrita numa linguagem formal, são definidas propriedades a serem satisfeitas e que certificariam a qualidade do software. Estas propriedades devem então ser implementadas para uso num verificador, que é a ferramenta responsável por executar a verificação e informar quais propriedades foram satisfeitas e quais não foram; no caso das propriedades terem sido violadas, o verificador deve indicar aos desenvolvedores os possíveis locais com código incorreto no sistema. A desvantagem do uso da verificação formal é, além do seu alto custo, a necessidade de haver pessoas com experiência em métodos formais para definir propriedades a partir da especificação formal do sistema, e convertê-las numa representação que possa ser entendida pelo verificador. Este processo de definição de propriedades é particularmente complexo, demorado e suscetível a erros, por ser feito em sua maior parte de forma manual. Para auxiliar os desenvolvedores na utilização da verificação formal em programas escritos em Java, propomos neste trabalho a geração de representação de propriedades para uso direto num verificador. As propriedades a serem geradas são objetivos de teste derivados da especificação formal do sistema. Estes objetivos de teste descrevem o comportamento esperado do sistema que deve ser observado durante sua execução. Ao estabelecer que o universo de propriedades corresponde ao universo de objetivos de teste do programa, garantimos que as propriedades geradas em nosso trabalho descrevem o comportamento esperado do programa por meio de caminhos de execução que levam a um estado de aceitação da propriedade, ou a um estado de violação. Assim, quando o verificador checa o objetivo de teste, ele consegue dar como resultado o veredicto de sucesso ou falha para a propriedade verificada, além de dados da cobertura dos caminhos de execução do programa que podem ser usados para análise do comportamento do programa que levou ao sucesso ou falha da propriedade verificada. / The task of guaranteeing that computational systems do not fail and work correctly has become extremely important with the growing presence of new technologies in people\'s lives. Therefore, it is essential to ensure that such systems work properly to confirm their high-quality and to avoid financial and even life losses. One of the techniques used to this purpose is called formal verification of programs. From the system specification, which should be described in a formal language, we define properties that must be satisfied during system execution to guarantee the software quality. Then, these properties are checked using a verifier, which is the tool responsible for running the verification and for notifying whether the property was satisfied by the program; if the property was violated, it indicates to software developers the possible location of faults in the system. The disadvantages of using formal verification are the high cost to apply this technique in practice, and the necessity of having people with experience in formal methods to derive the properties from system specification and define them in a formal representation that can be read by a program verifier. This particular task of deriving a property from system specification and defining it to be checked by a verifier is complex, time-consuming and error-prone, since it is usually done by hand. To help software developers in the application of formal verification in Java programs, we propose in this work the generation of properties formal representation for direct use in a verifier. The generated properties are test purposes, which are derived from system formal specification and present the desirable system behavior that must be observed during the system execution. Establishing that the universe of properties correspond to the universe of test purposes of a program, we guarantee that the generated properties describe the expected program behavior through execution traces that lead to either an accept state or a refuse state. Thus, when the verifier checks the test purpose, it can give a success/fail verdict for the property, and provide traces coverage data that can be used to analyze the program behavior that led to that verdict.

Made available in DSpace on 2016-04-29T14:23:40Z (GMT). No. of bitstreams: 1 Jose Valdvogel de Almeida Junior.pdf: 1664725 bytes, checksum: b5162f7ac0d53d0a3c9e995e1e643e18 (MD5) Previous issue date: 2015-11-19 / The component-based software development has proven effective for implementation in various fields of application, but still insufficient to create reusable and flexible parts. Processes and methods have been developed in order to address special care in this context. However, none of the proposed methods shows a simple specification of building blocks. To address this limitation we propose in this research work a split between the static and dynamic elements that make up the nature of an assembled component in a set of steps with application techniques using the best practices of software engineering. As a result, we reach the Component Specification method capable of generating well-designed models for building reusable and flexible software parts. A case study helps to illustrate the application of the method in an application context / O desenvolvimento de software baseado em componentes tem se provado efetivo para a implementação em diversos domínios de aplicação, mas ainda insuficiente para a criação de peças reusáveis e flexíveis. Processos e métodos foram desenvolvidos no intuito de endereçar cuidados especiais nesse contexto. No entanto, nenhum dos métodos propostos demonstra uma forma simples de especificação dos blocos construtores. Para tratar essa limitação propomos nesse trabalho de pesquisa uma divisão entre os elementos estáticos e dinâmicos que compõem a natureza de um componente reunidos em um conjunto de passos com aplicação de técnicas que utilizam as boas práticas da engenharia de software. Como resultado, chega-se ao Método de Especificação de Componentes capaz de gerar modelos bem elaborados para construção de peças de software reusáveis e flexíveis. Um estudo de caso ajuda a ilustrar a aplicação do método em um contexto de aplicação

Tese de mestrado integrado. Engenharia Electrónica e de Computadores. Faculdade de Engenharia. Universidade do Porto. 2012

The determination of economic control charts and the determination of specification limits with minimum cost are two different research topics. In this study, we first combine the design of economic control charts and the determination of specification limits to maximize the expected profit per unit time for the smaller the better quality variable following the gamma distribution. Because of the asymmetric distribution, we design the EWMA control chart with asymmetric control limits. We simultaneously determine the economic EWMA control chart and upper specification limit with maximum expected profit per unit time. Then, extend the approach to determine the economic variable sampling interval EWMA control chart and upper specification limit with maximum expected profit per unit time. In all our numerical examples of the two profit models, the optimum expected profit per unit time under inspection is higher than that of no inspection. The detection ability of the EWMA chart with an appropriate weight is always better than the X-bar probability chart. The detection ability of the VSI EWMA chart is also superior to that of the fixed sampling interval EWMA chart. Sensitivity analyses are provided to determine the significant parameters for the optimal design parameters and the optimal expected profit per unit time.