Spelling suggestions: "subject:"modelbased ingesting"" "subject:"modelbased andtesting""
41 |
Automated state model extraction, testing and change detection through graphical user interfaceAho, P. (Pekka) 01 November 2019 (has links)
Abstract
Testing is an important part of quality assurance, and the use of agile processes, continuous integration and DevOps is increasing the pressure for automating all aspects of testing. Testing through graphical user interfaces (GUIs) is commonly automated by scripts that are captured or manually created with a script editor, automating the execution of test cases. A major challenge with script-based GUI test automation is the manual effort required for maintaining the scripts when the GUI changes. Model-based testing (MBT) is an approach for automating also the design of test cases. Traditionally, models for MBT are designed manually with a modelling tool, and an MBT tool is used for generating abstract test cases from the model. Then, an adapter is implemented to translate the abstract test cases into concrete test cases that can be executed on system under test (SUT). When the GUI changes, the model has to be updated and the test cases can be generated from the updated model, reducing the maintenance effort. However, designing models and implementing adapters requires effort and specialized expertise.
The main research questions of this thesis are 1) how to automatically extract state-based models of software systems with GUI, and 2) how to use the extracted models to automate testing. Our focus is on using dynamic analysis through the GUI during automated exploration of the system, and we concentrate on desktop applications. Our results show that extracting state models through GUI is possible and the models can be used to generate regression test cases, but a more promising approach is to use model comparison on extracted models of consequent system versions to automatically detect changes between the versions. / Tiivistelmä
Testaaminen on tärkeä osa laadun varmistusta. Ketterät kehitysprosessit ja jatkuva integrointi lisäävät tarvetta automatisoida kaikki testauksen osa-alueet. Testaus graafisten käyttöliittymien kautta automatisoidaan yleensä skripteinä, jotka luodaan joko tallentamalla manuaalista testausta tai kirjoittamalla käyttäen skriptieditoria. Tällöin scriptit automatisoivat testitapausten suorittamista. Muutokset graafisessa käyttöliittymässä vaativat scriptien päivittämistä ja scriptien ylläpitoon kuluva työmäärä on iso ongelma. Mallipohjaisessa testauksessa automatisoidaan testien suorittamisen lisäksi myös testitapausten suunnittelu. Perinteisesti mallipohjaisessa testauksessa mallit suunnitellaan manuaalisesti käyttämällä mallinnustyökalua, ja mallista luodaan abstrakteja testitapauksia automaattisesti mallipohjaisen testauksen työkalun avulla. Sen jälkeen implementoidaan adapteri, joka muuttaa abstraktit testitapaukset konkreettisiksi, jotta ne voidaan suorittaa testattavassa järjestelmässä. Kun testattava graafinen käyttöliittymä muuttuu, vain mallia täytyy päivittää ja testitapaukset voidaan luoda automaattisesti uudelleen, vähentäen ylläpitoon käytettävää työmäärää. Mallien suunnittelu ja adapterien implementointi vaatii kuitenkin huomattavan työmäärän ja erikoisosaamista.
Tämä väitöskirja tutkii 1) voidaanko tilamalleja luoda automaattisesti järjestelmistä, joissa on graafinen käyttöliittymä, ja 2) voidaanko automaattisesti luotuja tilamalleja käyttää testauksen automatisointiin. Tutkimus keskittyy työpöytäsovelluksiin ja dynaamisen analyysin käyttämiseen graafisen käyttöliittymän kautta järjestelmän automatisoidun läpikäynnin aikana. Tutkimustulokset osoittavat, että tilamallien automaattinen luominen graafisen käyttöliittymän kautta on mahdollista, ja malleja voidaan käyttää testitapausten generointiin regressiotestauksessa. Lupaavampi lähestymistapa on kuitenkin vertailla malleja, jotka on luotu järjestelmän peräkkäisistä versioista, ja havaita versioiden väliset muutokset automaattisesti.
|
42 |
A Comparative Study of Automated Test ExplorersGustavsson, Johan January 2015 (has links)
With modern computer systems becoming more and more complicated, theimportance of rigorous testing to ensure the quality of the product increases.This, however, means that the cost to perform tests also increases. In orderto address this problem, a lot of research has been conducted during thelast years to find a more automated way of testing software systems. Inthis thesis, different algorithms to automatically explore and test a systemhave been implemented and evaluated. In addition to this, a second setof algorithms have been implemented with the objective to isolate whichinteractions with the system were responsible for a failure. These algorithmswere also evaluated and compared against each other. In the first evaluationtwo explorers, which I called DeBruijn and LStarExplorer, were consideredsuperior to the other. The first used a DeBruijn sequence to brute forcea solution while the second used the L*-algorithm to build an FSM overthe system under test. This FSM could then be used to provide a moreaccurate description for when the failure occurred. The result from thesecond evaluation were two reducers which both tried to recreate a failureby first applying interactions performed just before the failure occurred. Ifthis was not successful, they tried interactions further and further away, untilthe failure was triggered. In addition to this, the thesis contains descriptionsabout the framework used to run the different strategies. / D ̊a v ̊ara moderna datasystem blir allt mer komplicerade, ̈okar detta st ̈andigtbehovet av rigor ̈osa tester f ̈or att s ̈akerst ̈alla kvaliteten p ̊a den slutgiltiga pro-dukten. Det h ̈ar inneb ̈ar dock att kostnaden f ̈or att utf ̈ora testerna ocks ̊ao ̈ kar. F ̈or att f ̈ors ̈oka hitta en l ̈osning p ̊a det h ̈ar problemet har forsknin-gen under senare tid arbetat med att ta fram automatiserade metoder atttesta mjukvarusystem. I den h ̈ar uppsatsen har olika algoritmer, f ̈or attutforska och testa ett system, implementerats och utv ̈arderats. D ̈arut ̈overhar ocks ̊a en grupp algoritmer implementerats som ska kunna isolera vilkainteraktioner med ett system som f ̊ar det att fallera. ̈aven dessa algoritmerhar utv ̈arderats och testats mot varandra. Resultatet fr ̊an det f ̈orsta ex-perimentet var tv ̊a explorers, h ̈ar kallade DeBruijn och LStarExplorer, somvisade sig vara b ̈attre ̈an de andra. Den f ̈orsta av dessa anv ̈ande en DeBruijn-sekvens f ̈or att hitta felen, medan den andra anv ̈ande en L*-algoritm f ̈or attbygga upp en FSM ̈over systemet. Den h ̈ar FSM:en kunde sedan anv ̈andasf ̈or att mer precist beskriva n ̈ar felet uppstod. Resultatet fr ̊an det andraexperimentet var tv ̊a reducers, vilka b ̊ada f ̈ors ̈okte ̊aterskapa fel genom attf ̈orst applicera interaktioner som ursprungligen utf ̈ordes percis innan feletuppstod. Om felet inte kunde ̊aterskapas p ̊a detta s ̈att, fortsatte de medatt applicera interaktioner l ̈angre bort tills felet kunde ̊aterskapas. Ut ̈overdetta inneh ̊aller uppsatsen ocks ̊a beskrivningar av ramverken som anv ̈andsf ̈or att k ̈ora de olika strategierna.
|
43 |
Model-Based Test Case Generation for Real-Time SystemsHessel, Anders January 2007 (has links)
Testing is the dominant verification technique used in the software industry today. The use of automatic test case execution increases, but the creation of test cases remains manual and thus error prone and expensive. To automate generation and selection of test cases, model-based testing techniques have been suggested. In this thesis two central problems in model-based testing are addressed: the problem of how to formally specify coverage criteria, and the problem of how to generate a test suite from a formal timed system model, such that the test suite satisfies a given coverage criterion. We use model checking techniques to explore the state-space of a model until a set of traces is found that together satisfy the coverage criterion. A key observation is that a coverage criterion can be viewed as consisting of a set of items, which we call coverage items. Each coverage item can be treated as a separate reachability problem. Based on our view of coverage items we define a language, in the form of parameterized observer automata, to formally describe coverage criteria. We show that the language is expressive enough to describe a variety of common coverage criteria described in the literature. Two algorithms for test case generation with observer automata are presented. The first algorithm returns a trace that satisfies all coverage items with a minimum cost. We use this algorithm to generate a test suite with minimal execution time. The second algorithm explores only states that may increase the already found set of coverage items. This algorithm works well together with observer automata. The developed techniques have been implemented in the tool CoVer. The tool has been used in a case study together with Ericsson where a WAP gateway has been tested. The case study shows that the techniques have industrial strength.
|
44 |
Modeliais paremtas testavimas: testavimo įrankių tyrimas / Model-based testing: analysis of the model based testing toolsAdomaitis, Ernestas 27 June 2014 (has links)
Modeliais paremtas testavimas tampa vis populiaresnis. Sudėtingos programinės įrangos kokybės užtikrinimas ir modeliais orientuotas sistemų kūrimas yra pagrindinės šio testavimo būdo išpopuliarėjimo priežastys. Pagrindiniai šio darbo tikslai yra modeliais paremtų testavimo įrankių analizė ir jų tobulinimo galimybės. Darbe naudojama daugiau nei dešimt įvairių įrankių vertinimo kriterijų. Analizuojama testų padengimo kriterijų pritaikymo ir tobulinimo galimybės. Analizuojamos modeliais paremto proceso problemos ir pateikiami sprendimo būdai. Atlikta detali testų kūrimo kriterijų ir modelio perėjimo algoritmų analizė. Atlikus detalę kriterijų ir modelio perėjimo algoritmų analizę, pateikiama kriterijų apjungimo privalumai ir kaip naudojant įvairius kriterijus galima valdyti testų kūrimo procesą ir siekti 100 procentinio modelio padengimo. Pateikiama ir detaliai išanalizuojama kriterijų kūrimo metodika, kurią galim taikyti testavimo įrankiuose. / Model-based testing has become increasingly popular in recent years. Major reasons include the need for quality assurance for increasingly complex systems and the emerging model-centric development paradigm. The present thesis aims at analysing model-based testing tools and presents the possibilities for their improvement. More than dozen criteria are applied in analysing selected tools. The paper analyses the application of testing coverage criteria and presents their possible improvements. The problems occurring in the model-based testing process are being analysed and the solutions presented. The study contains an in-depth analysis of test coverage criteria and model traversal algorithms. A thorough analysis of test criteria and model traversal algorithms being performed, the advantages of the integration of test criteria are presented. Furthermore, a solution for managing the development process of test cases as well as pursuing a hundred percent model coverage is proposed. The paper presents a comprehensive analysis of test criteria development methodology that could be applied in testing tools.
|
45 |
Abordagens para avaliação experimental de testes baseado em modelos de aplicações reativas. / Approaches for experimental evaluation of tests based on reactive application modelsNASCIMENTO, Laísa Helena Oliveira do. 27 August 2018 (has links)
Submitted by Johnny Rodrigues (johnnyrodrigues@ufcg.edu.br) on 2018-08-27T18:21:34Z
No. of bitstreams: 1
LAÍSA HELENA OLIVEIRA DO NASCIMENTO - DISS PPGCC 2008..pdf: 1446971 bytes, checksum: 3622ab4c366ab0a686c4f32d688c13b6 (MD5) / Made available in DSpace on 2018-08-27T18:21:34Z (GMT). No. of bitstreams: 1
LAÍSA HELENA OLIVEIRA DO NASCIMENTO - DISS PPGCC 2008..pdf: 1446971 bytes, checksum: 3622ab4c366ab0a686c4f32d688c13b6 (MD5)
Previous issue date: 2008-02-28 / Processos de teste de software vêm ganhando cada vez mais espaço na indústria. Empresas têm investindo na definição e formalização dos seus processos e em meio a essa mudança de comportamento, Model-Based Testing (MBT) apresenta-se como uma técnica promissora de teste. No entanto, a utilização de MBT ainda é baixa e pesquisadores têm focado em maneiras de superar as barreiras para que se obtenha uma adoção maior por parte da indústria. O mundo empresarial é movido a processos e resultados. Dessa forma, o uso de MBT precisa se adaptar aos processos existentes, e estudos de caso que evidenciem as vantagens de sua utilização precisam ser conduzidos. Neste trabalho, o paradigma Goal Question Metric é utilizado na definição de modelos de medição que têm como foco principal a avaliação e o acompanhamento do desempenho de MBT sem causar impacto ao processo de teste já existente. Os modelos de medição consideram métricas como esforço, percentual de requisitos testáveis cobertos, percentual de casos de teste modificados, percentual de falhas,dentre outros. Os modelos não estão atrelados ao processo de MBT apresentado, podendo ser aplicados
em qualquer processo que permita a coleta dos dados necessários para o cálculo das
métricas. Para validar os modelos, estudos de caso foram conduzidos dentro do ambiente de testes da Motorola. / Software testing processes have become more common in industry. Companies are investing on the definition and the formalization of their test processes and, in this context,
Model-Based Testing (MBT) appears as an interesting testing technique. However, industrial adoption of MBT remains low and researchers are also focusing on how to beat the barriers to wide adoption. Processes and results move the business world so, MBT processes must be adaptable to actual testing processes. For this, experiments to evaluate the results achieved with its use must be conduct. In this work, measurement models based on the Goal Question Metric methodology are proposed. The purpose is evaluating the use of MBT without increasing actual testing process costs. The models focus on aspects as effort, testable requirements coverage, modified test cases, failures, among others. The models are not associated with the MBT process presented. They can be applied with any process that allows metrics collection. In order to validate the measurement models, case studies were conducted into Motorola testing environment.
|
46 |
Filtering and reduction techniques of combinatorial tests / Filtrage et réduction de tests combinatoiresTriki, Taha 04 October 2013 (has links)
L'objectif principal de cette thèse est d'apporter des solutions à certaines problèmes du test combinatoire. Le test combinatoire consiste à générer des tests qui couvrent toutes les combinaisons de valeurs d'entrée définies. La première problème abordé, c'est que le test combinatoire peut générer un grand nombre de tests qui sont invalides par rapport à la spécification du système à tester (SUT). Ces tests invalides sont typiquement ceux qui échouent lors de la vérification de la pré-condition d'une opération de système. Ces tests invalides doivent être éliminés de l'ensemble des tests utilisé pour évaluer le SUT, car ils conduisent à des verdicts non concluants. Comme solution, nous proposons de coupler la technique de test combinatoire à une technique d'animation qui repose sur une spécification pour filtrer les tests invalides. Dans notre travail, les tests combinatoires sont générés à partir d'un patron de test. Ce patron est essentiellement défini comme une séquence d'appels d'opérations, en utilisant un ensemble de valeurs pour les paramètres. Le dépliage d'un patron de test complexe, où plusieurs valeurs d'entrée sont utilisées, peut être soumis à une explosion combinatoire, et il est impossible d'avoir des tests valides à partir du patron de test. Il s'agit d'une deuxième problématique de cette thèse. Comme solution, nous proposons un processus de dépliage et d'animation incrémental qui permet de filtrer à un stade précoce (dans la séquence d'appels d'opération) les tests invalides, et donc de maîtriser l'explosion combinatoire. D'autres mécanismes de filtrage sont proposés, pour filtrer les tests qui ne couvrent pas certains comportements d'opération ou ne remplissent pas une propriété donnée. Le nombre de tests générés à partir d'un patron de test peut être considérablement grand pour être exécuté sur un SUT avec ressources mémoires et processeurs limitées. Ce problème est connu sous le nom de problème de réduction de suites de tests, et il représente le troisième problème de cette thèse. Comme solution, nous proposons une nouvelle technique de réduction de suites de tests basée sur les annotations (appelés tags) insérées dans le code source ou la spécification du SUT. L'exécution / animation de tests génère une trace des annotations couverts. Basé sur cette trace d'exécution, une famille de relations d'équivalence est proposée, pour réduire une suite de tests, en utilisant les critères d'ordre et de nombre de répétition des tags couverts. / The main objective of this thesis is to provide solutions to some combinatorial testing issues. The combinatorial testing consists in generating tests that cover all combinations of defined input values. The first issue of this thesis is that combinatorial testing can generate a large number of tests that are invalid according to the specification of the System Under Test (SUT). These invalid tests are typically those which fail the verification of the precondition of system operation. These invalid tests must be discarded from the set of tests used to evaluate the SUT, because they lead to inconclusive verdicts. As a solution, we propose to couple the combinatorial testing technique to an animation technique that relies on a specification to filter out invalid tests. In our work, combinatorial tests are generated from a test pattern. This pattern is mainly defined as a sequence of operation calls, using a set of values for their parameters. The unfolding of a complex test pattern, where many operation calls and/or input values are used, may be subject to combinatorial explosion, and it is impossible to provide valid tests from the test pattern. This is a second issue of this thesis. As a solution, we propose an incremental unfolding and animation process that allows to filter out at early stage (in the operation sequence) invalid tests, and therefore to master the combinatorial explosion. Other mechanisms of filtering are proposed to filter out tests which do not cover some operation behaviors or do not fulfill a given property. The test suites generated from a test pattern can be very large to execute on the SUT due the limited memory or CPU resources. This problem is defined as the test suite reduction problem, and it is the third issue of this thesis. As a solution, we propose a new test suite reduction technique based on annotations (called tags) inserted in the source code or the specification of the SUT. The execution/animation of tests generates a trace of the covered annotations. Based on the trace, a family of equivalence relations is proposed, to reduce a test suite, using the criteria of order and number of repetition of covered tags.
|
47 |
Análise de cobertura de critérios de teste estruturais a partir de conjuntos derivados de especificações formais: um estudo comparativo no contexto de aplicações espaciais / Structural coverage analysis of test sets derived from formal specifications: a comparative study in the space applications contextPaula Fernanda Ramos Herculano 24 April 2007 (has links)
As técnicas de teste podem ser divididas, num primeiro nível, naquelas baseadas no código (caixa branca) e naquelas baseadas na especificação (caixa preta ou funcionais). Nenhuma delas é completa pois visam a identificar tipos diferentes de defeitos e a sua utilização em conjunto pode elevar o nível de confiabilidade das aplicações. Assim, tornam-se importantes estudos que contribuam para um melhor entendimento da relação existente entre técnicas funcionais e estruturais, como elas se complementam e como podem ser utilizadas em conjunto. Este trabalho está inserido no contexto do projeto PLAVIS (Plataforma para Validação e Integração de Software em Aplicações Espaciais), e tem como objetivo realizar um estudo comparativo entre as técnicas de geração de casos de teste funcionais (baseadas nas especificações formais) e os critérios estruturais baseados em fluxo de controle e fluxo de dados, aplicados nas implementações. Num contexto específico, esse estudo deve fornecer dados de como se relacionam essas duas técnicas (funcional e estrutural) gerando subsídios para sua utilização em conjunto. Num contexto mais amplo - o do projeto PLAVIS - visa a estabelecer uma estratégia de teste baseada em critérios funcionais e estruturais e que possam, juntamente com as ferramentas que dão suporte a eles, compor um ambiente de teste disponível à utilização em aplicações espaciais dentro do INPE / Testing techniques can be divided, in high level, in code-based ones (white box) and specification based ones (black box). None of them are complete as they intend to identify different kinds of faults. The use of them together can increase the application confidence level. Thus, it is important to investigate the relationship between structural testing techniques and functional testing techniques, how they complete themselves and how they can be used together. This paper was developed in the context of the Plavis (PLAtform of software Validation & Integration on Space systems) project. This project provides comparative studies between functional generation testing techniques (based on formal specifications) and structural generation testing techniques, such as control-flow and data-flow criteria, applied in the implementation. In a specific context, this study provides data about the relationship between these techniques and how they can be used together. In the context of the Plavis project, the goal is to provide a testing strategy, based on functional and structural criteria, and a set of tools, composing a testing environment to be used in Space Applications projects, at INPE
|
48 |
Técnicas de testes aplicadas a software embarcado em redes ópticas / Tests techniques applied to embedded software in optical networksFadel, Aline Cristine, 1984- 19 August 2018 (has links)
Orientadores: Regina Lúcia de Oliveira Moraes, Eliane Martins / Dissertação (mestrado) - Universidade Estadual de Campinas, Faculdade de Tecnologia / Made available in DSpace on 2018-08-19T14:09:37Z (GMT). No. of bitstreams: 1
Fadel_AlineCristine_M.pdf: 3259764 bytes, checksum: a287ca33254d027f23e2f2f818464ee1 (MD5)
Previous issue date: 2011 / Resumo: Esse trabalho apresenta os detalhes e os resultados de testes automatizados e manuais que utilizaram a técnica de injeção de falhas e que foram aplicados em redes ópticas. No primeiro experimento o teste foi automatizado e utilizou a emulação de falhas físicas baseadas na máquina de estados do software embarcado dessa rede. Para esse teste foi utilizado uma chave óptica que é controlada por um robô de testes. O segundo experimento foi um teste manual, que injetou falhas nas mensagens de comunicação do protocolo dessa rede, a fim de validar os mecanismos de tolerância a falhas do software central dessa rede. Esse experimento utilizou a metodologia Conformance and Fault injection para preparar, executar e relatar os resultados dos casos de testes. Nos dois experimentos também foi utilizado um padrão de documentação de testes que visa facilitar a reprodução dos testes, a fim de que eles possam ser aplicados em outros ambientes. Com a aplicação desses testes, a rede óptica pode alcançar uma maior confiabilidade, disponibilidade e robustez, que são características essenciais para sistemas que requerem alta dependabilidade / Abstract: This work presents the details and the results of automatic and manual tests that used the fault injection technique and were applied on GPON network. In the first experiment the test was automated, and it performed the emulation of physical faults based on the state machine of the embedded software in this network. In this test is used an optical switch that is controlled by a test robot. The second experiment was a manual test, which injected faults on protocol communication message exchanged through the optical network, in order to validate the main software fault tolerance mechanisms. This experiment used a Conformance and Fault injection methodology to prepare, execute and report the results of the test cases. In both experiments, it was used a standard test documentation to facilitate the reproduction of the tests, so that they can be applied in other environments. With applying both tests, the optical networks reach greater reliability, availability and robustness. These attributes are essential for systems that require high dependability / Mestrado / Tecnologia e Inovação / Mestre em Tecnologia
|
49 |
A Test Framework for Executing Model-Based Testing in Embedded SystemsIyenghar, Padma 25 September 2012 (has links)
Model Driven Development (MDD) and Model Based Testing (MBT) are gaining inroads individually for their application in embedded software engineering projects. However, their full-edged and integrated usage in real-life embedded software engineering projects (e.g. industrially relevant examples) and executing MBT in resource constrained embedded systems (e.g. 16 bit system/64 KiByte memory) are emerging fields.
Addressing the aforementioned gaps, this thesis proposes an integrated model-based approach and test framework for executing the model-based test cases, with minimal overhead, in embedded systems. Given a chosen System Under Test (SUT) and the system design model, a test framework generation algorithm generates the necessary artifacts (i.e., the test framework) for executing the model-based test cases. The main goal of the test framework is to enable test automation and test case execution at the host computer (which executes the test harness), thereby only the test input data is executed at the target. Significant overhead involved in interpreting the test data at the target is eliminated, as the test framework makes use of a target debugger (communication and decoding agent) on the host and a target monitor (software-based runtime monitoring routine) in the embedded system. In the prototype implementation of the proposed approach, corresponding (standardized) languages such as the Unified Modeling Language (UML) and the UML Testing Profile (UTP) are used for the MDD and MBT phases respectively. The applicability of the proposed approach is demonstrated using an experimental evaluation (of the prototype) in real-life examples.
The empirical results indicate that the total time spent for executing the test cases in the target (runtime-time complexity), comprises of only the time spent to decode the test input data by the target monitor and execute it in the embedded system. Similarly, the only memory requirement in the target for executing the model-based test cases in the target is that of the software-based target monitor. A quantitative comparison on the percentage change in the memory overhead (runtime-memory complexity) for the existing approach and the proposed approach indicates that the existing approach (e.g. in a MDD/MBT tool-Rhapsody), introduces approximately 150% to 350% increase in memory overhead for executing the test cases. On the other hand, in the proposed approach, the target monitor is independent of the number of test cases to be executed and their complexity. Hence, the percentage change in the memory overhead for the proposed approach shows a declining trend w.r.t the increasing code-size for equivalent application scenarios (approximately 17% to 2%).
Thus, the proposed test automation approach provides the essential benefit of executing model- based tests, without downloading the test harness in the target. It is demonstrated that it is feasible to execute the test cases specified at higher abstraction levels (e.g. using UML sequence diagrams) in resource constrained embedded systems and how this may be realized using the proposed approach. Further, as the proposed runtime monitoring mechanism is time and memory-aware, the overhead parameters can be accommodated in the earlier phases of the embedded software development cycle (if necessary) and the target monitor can be included in the final production code. The aforementioned advantages highlight the scalability, applicability, reliability and superiority of the proposed approach over the existing methodologies for executing the model-based test cases in embedded systems.
|
50 |
Model-driven development of information systemsWang, Chen-Wei January 2012 (has links)
The research presented in this thesis is aimed at developing reliable information systems through the application of model-driven and formal techniques. These are techniques in which a precise, formal model of system behaviour is exploited as source code. As such a model may be more abstract, and more concise, than source code written in a conventional programming language, it should be easier and more economical to create, to analyse, and to change. The quality of the model of the system can be ensured through certain kinds of formal analysis and fixed accordingly if necessary. Most valuably, the model serves as the basis for the automated generation or configuration of a working system. This thesis provides four research contributions. The first involves the analysis of a proposed modelling language targeted at the model-driven development of information systems. Logical properties of the language are derived, as are properties of its compiled form---a guarded substitution notation. The second involves the extension of this language, and its semantics, to permit the description of workflows on information systems. Workflows described in this way may be analysed to determine, in advance of execution, the extent to which their concurrent execution may introduce the possibility of deadlock or blocking: a condition that, in this context, is synonymous with a failure to achieve the specified outcome. The third contribution concerns the validation of models written in this language by adapting existing techniques of software testing to the analysis of design models. A methodology is presented for checking model consistency, on the basis of a generated test suite, against the intended requirements. The fourth and final contribution is the presentation of an implementation strategy for the language, targeted at standard, relational databases, and an argument for its correctness, based on a simple, set-theoretic semantics for structure and operations.
|
Page generated in 0.0595 seconds