• Refine Query
  • Source
  • Publication year
  • to
  • Language
  • 402
  • 41
  • 3
  • 2
  • 2
  • 2
  • 2
  • 1
  • 1
  • Tagged with
  • 446
  • 446
  • 182
  • 148
  • 84
  • 81
  • 58
  • 50
  • 50
  • 50
  • 44
  • 44
  • 43
  • 42
  • 41
  • About
  • The Global ETD Search service is a free service for researchers to find electronic theses and dissertations. This service is provided by the Networked Digital Library of Theses and Dissertations.
    Our metadata is collected from universities around the world. If you manage a university/consortium/country archive and want to be added, details can be found on the NDLTD website.
341

Investigação do processo de desenvolvimento de software a partir da modelagem organizacional, enfatizando regras do negócio / Investigation of the process in software development based on enterprise modeling, emphasizing business rules

Pádua, Silvia Inês Dallavalle de 27 March 2001 (has links)
A preocupação da engenharia de software esteve por muito tempo relacionada a aspectos da funcionalidade do sistema, ou seja, com \"o que\" e \"como\" fazer e não com o \"por que\" fazer. Tais aspectos, envolvidos nos processos existentes, buscam a definição das propriedades desejadas, em lugar de observarem a informação de uma forma mais ampla, começando com as necessidades do próprio negócio, ou dos objetivos dos sistemas nele embutidos. As técnicas de análise estruturadas, diagrama de fluxo de dados e modelagem entidade e relacionamento modelam importantes conceitos para o desenvolvimento de sistemas, mas não buscam por soluções alternativas inovadoras aos problemas da organização. É comum encontrar situações onde o sistema não satisfaz às reais necessidades do negócio, embora esteja tecnicamente correto. O entendimento dos aspectos sociais, organizacionais, técnicos, jurídicos e econômicos é essencial para a realização de um bom trabalho de engenharia de requisitos. Nesse sentido, a modelagem organizacional facilita a compreensão do ambiente empresarial e é reconhecida como uma atividade valiosa pela engenharia de requisitos. O modelo organizacional representa o \"mundo\" onde se aplicam as regras do negócio. O entendimento das regras do negócio é muito importante para a organização ser flexível em um ambiente de crescente competitividade. Com a necessidade de se ter a modelagem dos aspectos relativos à organização para que o sistema atenda as suas reais necessidades, o presente trabalho tem como objetivo investigar o processo de desenvolvimento de software buscando conhecer técnicas ou métodos que atendem aos requisitos organizacionais, enfatizando o uso de regras do negócio com a finalidade de obter a especificação de requisitos. / The software engineering\'s focus were for a long time related to system\'s functionality aspects, or with \"what\" and \"how\" to do, and not with \"why\" to do. Those aspects in the existents process are looking for the definition of the desired proprieties instead observe the information in a more large aspect, beginning with the business needs itself or the systems goals inserted in it. The structure analysis techniques, flux data diagram, and relationship and entity modeling form important concepts for systems development but do not search for innovating alternatives solutions for organization\'s problems. It is very common to find situations were the system does not satisfy the real business needs, thought it is technically correct. The comprehension of social, organizational, technical, juridical and economics aspects are essential for a good realization of requirements in engineering work. In that way the enterprise modeling makes the business environment comprehension easier and is recognized as a value activity by the requirements engineering. The enterprise model represents the \"world\" where the business rules are applied. The comprehension of the business rules is very important so the organization can be flexible in a growing competitive environment. With the necessity to have a modeling of the relative aspects to the organization so the system can accomplish the real needs, this present research has the objective to investigate a software development process trying to find techniques or methods that answer the enterprise\'s requirement, emphasizing the use of business rules to obtain the specifics requirements.
342

Geração parcial de código Java a partir de especificações formais Z. / Partial generation of Java code from Z formal specifications.

Miyazawa, Alvaro Heiji 03 October 2008 (has links)
Especificações formais são úteis para descrever o que um sistema deve fazer sem definir como, e, em virtude da sua natureza formal e da possibilidade de abstração, é possível analisá-las sistematicamente. No entanto, o uso de especificações formais como parte do desenvolvimento de software não constitui prática comum. Isso se dá, em parte, pelo fato de existirem apenas um pequeno número de metodologias e ferramentas adequadas que dêem suporte a esse desenvolvimento. O primeiro objetivo deste trabalho é propor uma metodologia de desenvolvimento que possibilite, a partir de uma especificação formal em notação Z, produzir uma implementação dessa especificação em Java. Essa metodologia centra-se na geração do esqueleto da aplicação Java e na instrumentação desse esqueleto com mecanismos de verificação de condições (invariantes, pré e pós-condições) e rastreamento de violações dessas condições. Através desses mecanismos, possibilita-se intercalar desenvolvimento formal e informal no processo global de desenvolvimento de software. O segundo objetivo é desenvolver uma ferramenta que implemente parte dessa metodologia, produzindo uma implementação parcial que deverá ser complementada pelo usuário. / Formal specifications are useful for describing what a system should do, without defining how, and, owing to its formal nature, it is possible to analyse them systematically. However useful formal specifications are, their usage as part of the software development process is rather rare. This is, in part, due to the scarcity of both methodologies and tools that support this development. The first goal of this work is to define a software development methodology that enables the developer to produce a Java application from a formal specification written in Z. This methodology will rely strongly on the generation of Java application skeletons and instrumentation of the generated code with means of verifying conditions (invariants, pre and post-conditions) e tracing violations of these conditions. Through this mechanisms, it is possible to mix formal and informal development in the global software development process. The second goal of this work is to develop a tool that will implement part of this methodology, producing a partial implementation that must be complemented by the developer.
343

Um modelo de referência para o desenvolvimento ágil de software / The reference model for agile development

Nascimento, Gustavo Vaz 20 September 2007 (has links)
A crescente procura por software de qualidade vem causando grande pressão sobre as empresas que trabalham com desenvolvimento de software. As entregas de produtos de software dentro do prazo e custo previstos vêm se tornando, a cada dia, um diferencial importante nesse ramo de atividade. Nesse sentido, as empresas procuram por metodologias que propiciem o desenvolvimento de produtos com qualidade, e que respeitem o custo e prazo previstos. Em resposta a essas necessidades, surgiu uma nova classe de metodologias de desenvolvimento de software, conhecidas como metodologias ágeis. Este trabalho apresenta um estudo realizado sobre as principais características existentes nessa nova classe de metodologias. Uma análise permitiu a identificação de semelhanças e diferenças existentes entre elas, o que possibilitou a criação de um modelo de referência para o desenvolvimento ágil de software. O modelo foi utilizado em uma avaliação de processo baseada no modelo de avaliação da ISO/IEC 15504. A avaliação permitiu a identificação de forças e fraquezas no processo avaliado e possibilitou a definição de ações de melhoria para que o processo avaliado se assemelhasse à um processo de desenvolvimento ágil. Palavra-chave: Metodologia ágil de desenvolvimento. Modelo de referência. Processo de desenvolvimento de software. Avaliação de processo de software / The vast demand for software with quality is causing a great pressure on the companies which work with software development. The delivery of software products within the schedule and cost is becoming, every day, an important issue in this area. Therefore, companies are seeking for methodologies to develop products with quality, within the timetable and the cost. Considering these needs, it became a new class of software development methodologies, known as agile methodologies. This research shows a work done upon the main existing characteristics in this new class of methodologies. An analysis allowed the identification of the existing similarities and differences among them, which it made possible to create a new reference model for agile software development. The agile model was used in process assessment based on assessment model from ISO/IEC 15504. The assessment alowed a identification of power and weakness on the process and alowed a definition of improvement action to the process with the intention of to approach the agile development process
344

Desenvolvimento de um simulador computacional de dinâmica de fluidos utilizando o método de Lattice Boltzmann. / Development of a computational simulator fo fluid dynamica using the Lattice Boltzmann method.

Komori, Fabio Sussumu 23 May 2012 (has links)
Este trabalho aborda a utilização do método de Lattice Boltzmann como ferramenta de simulação para a área de dinâmica de fluidos. Além disso, apresenta o programa LBSim desenvolvido durante o período de pesquisa, construído para ser flexível e extensível (através do emprego de técnicas de orientação a objetos) e com uma interface gráfica mais amigável do que outros projetos semelhantes. Como resultado deste trabalho, o software LBSim implementa uma série de módulos diferentes que utilizam o método de Lattice Boltzmann como base, permitindo a simulação de casos monofásico, multifásico, multicomponente, com suporte à gravidade, meios porosos, difusão, transferência de calor e paredes deslizantes. / This work approaches the use of the Lattice Boltzmann method as a simulation tool for the fluid dynamics area. Beyond that, it presents the LBSim software, developed during the period of the research and built to be flexible and extensible (through the application of techniques of the object oriented paradigm) and with a graphical interface more friendly than other similar projects. As a result of this work, the LBSim software implements a series of different modules that uses the Lattice Boltzmann method as a base, allowing the simulations of the following cases: monophase, multiphase, multicomponent, with support of gravity, porous media, diffusion, heat transfer and moving walls.
345

\"Um provador de teoremas multi-estratégia\" / A Multi-Strategy Tableau Prover

Seca Neto, Adolfo Gustavo Serra 30 January 2007 (has links)
Nesta tese apresentamos o projeto e a implementação do KEMS, um provador de teoremas multi-estratégia baseado no método de tablôs KE. Um provador de teoremas multi-estratégia é um provador de teoremas onde podemos variar as estratégias utilizadas sem modificar o núcleo da implementação. Além de multi-estratégia, o KEMS é capaz de provar teoremas em três sistemas lógicos: lógica clássica proposicional, mbC e mCi. Listamos abaixo algumas das contribuições deste trabalho: * um sistema KE para mbC que é analítico, correto e completo; * um sistema KE para mCi que é correto e completo; * um provador de teoremas multi-estratégia com as seguintes características: - aceita problemas em três sistemas lógicos: lógica clássica proposicional, mbC e mCi; - tem seis estratégias implementadas para lógica clássica proposicional, duas para mbC e duas para mCi; - tem treze ordenadores que são usados em conjunto com as estratégias; - implementa regras simplificadoras para lógica clássica proposicional; - possui uma interface gráfica que permite a visualização de provas; - é de código aberto e está disponível na Internet em http://kems.iv.fapesp.br; * benchmarks obtidos através da comparação das estratégias para lógica clássica proposicional resolvendo várias famílias de problemas; - sete famílias de problemas para avaliar provadores de teoremas paraconsistentes; * os primeiros benchmarks para as famílias de problemas para avaliar provadores de teoremas paraconsistentes. / In this thesis we present the design and implementation of KEMS, a multi-strategy theorem prover based on the KE tableau inference system. A multi-strategy theorem prover is a theorem prover where we can vary the strategy without modifying the core of the implementation. Besides being multi-strategy, KEMS is capable of proving theorems in three logical systems: classical propositional logic, mbC and mCi. We list below some of the contributions of this work: * an analytic, correct and complete KE system for mbC; * a correct and complete KE system for mCi; * a multi-strategy prover with the following characteristics: - accepts problems in three logical systems: classical propositional logic, mbC and mCi; - has 6 implemented strategies for classical propositional logic, 2 for mbC and 2 for mCi; - has 13 sorters to be used alongside with the strategies; - implements simplification rules of classical propositional logic; - provides a proof viewer with a graphical user interface; - it is open source and available on the internet at http://kems.iv.fapesp.br; * benchmark results obtained by KEMS comparing its classical propositional logic strategies with several problem families; * seven problem families designed to evaluate provers for logics of formal inconsistency; * the first benchmark results for the problem families designed to evaluate provers for logics of formal inconsistency.
346

Metodologia para implementação do MPS.BR utilizando o ambiente webapsee

ROCHA, Vanderlene Covre 29 April 2009 (has links)
Submitted by Irvana Coutinho (irvana@ufpa.br) on 2011-03-30T16:38:01Z No. of bitstreams: 2 ROCHA, Vanderlene Covre PPGEngenharia Elétrica.pdf: 2493637 bytes, checksum: ac14f60ec89cf61fb6b7fd05ccdbf266 (MD5) license_rdf: 22876 bytes, checksum: 0a4e855daae7a181424315bc63e71991 (MD5) / Made available in DSpace on 2011-03-30T16:38:01Z (GMT). No. of bitstreams: 2 ROCHA, Vanderlene Covre PPGEngenharia Elétrica.pdf: 2493637 bytes, checksum: ac14f60ec89cf61fb6b7fd05ccdbf266 (MD5) license_rdf: 22876 bytes, checksum: 0a4e855daae7a181424315bc63e71991 (MD5) Previous issue date: 2009 / Eletronorte - Centrais Elétricas do Norte do Brasil S/A / FAPESPA - Fundação Amazônia de Amparo a Estudos e Pesquisas / A number of initiatives to improve the software process has emerged recently to improve quality and productivity in software organizations. Some models and standards have focused the implementation of improvements in the software development process area; MPS.BR model is an example of thiese models. This process improvement model aims to improve software quality, preferably for micro, small and medium enterprises in order to meet the needs of their business model and was chosen to be explored in this work. Several advantages are gained during process improvement effort, one of them is the definition of a systematic process for software development, which helps to achieve the process quality and productivity and also the developed product quality. The use of a defined process model brings several benefits associated with standardization, such as the optimization, the re-work cost reduction, less defects in products, among others. But there is a lack of models that can be applied directly to a specific company of software development and therefore it is necessary to model the process, customizing it with the ultimate goal of creating a model that adequately represents the organization process. One of the difficulties for the implementation of models such as MPS.BR is the lack of methodologies that shows how the implementation of improvements to be made and not only what should be done. In this context, this work proposes a methodology for the implementation of the MPS.BR model based on IDEAL model, through a specific tool, called WebAPSEE, which works to coordinate the methodology execution. The methodology was tested in a local organization called CTIC - Center for Information Technology and Communication of UFPA which was assessed as level of G MPS.BR. / Uma série de iniciativas para melhoria do processo de software surgiu recentemente visando melhorar a qualidade e a produtividade em organizações de desenvolvimento de software. Alguns modelos e normas têm buscado a implantação de melhorias no processo de desenvolvimento de software, o MPS.BR é um deles. Esse modelo de melhoria de processo é voltado para as micro, pequenas e médias empresas, de forma a atender as suas necessidades de negócio e foi o modelo escolhido para ser explorado nesse trabalho. Várias são as vantagens adquiridas com a implantação de um modelo de melhoria, umas delas é a definição de um processo sistemático de desenvolvimento de software, que auxilie tanto na qualidade e produtividade do processo quanto na qualidade do produto desenvolvido. Com um modelo de processo definido a organização pode contar com diversos benefícios associados à padronização, como, por exemplo, a otimização, a redução de custos com retrabalho, a redução de defeitos nos produtos, dentre outros. Mas não existem modelos prontos que possam ser aplicados diretamente a uma empresa específica de desenvolvimento de software e, por isso, é necessário modelar o processo, customizando-o, com o objetivo final de gerar um modelo que adequadamente represente o processo da organização. Uma das dificuldades para a implantação de modelos como o MPS.BR é a falta de metodologia que mostre como a implantação de melhoria deve ser feita e não apenas o que deve ser feito. Este trabalho propõe uma metodologia para a implementação do modelo MPS.BR baseada no modelo de implantação IDEAL, através de uma ferramenta específica, chamada WebAPSEE. A metodologia foi experimentada no CTIC - Centro de Tecnologia da Informação e Comunicação da UFPA que ao final do trabalho foi avaliado Nível G do MPS.BR.
347

Modelagem de objetos tridimensionais para um ambiente interativo de instruções técnicas virtuais

NASCIMENTO, Messias José Amador do 10 September 2010 (has links)
Submitted by Edisangela Bastos (edisangela@ufpa.br) on 2012-04-13T19:19:11Z No. of bitstreams: 2 Dissertacao_ModelagemObjetosTridimensionais.pdf: 3042891 bytes, checksum: 373f6a0d7c39f681ae694cbf6d72b2b9 (MD5) license_rdf: 23898 bytes, checksum: e363e809996cf46ada20da1accfcd9c7 (MD5) / Approved for entry into archive by Edisangela Bastos(edisangela@ufpa.br) on 2012-04-13T19:19:22Z (GMT) No. of bitstreams: 2 Dissertacao_ModelagemObjetosTridimensionais.pdf: 3042891 bytes, checksum: 373f6a0d7c39f681ae694cbf6d72b2b9 (MD5) license_rdf: 23898 bytes, checksum: e363e809996cf46ada20da1accfcd9c7 (MD5) / Made available in DSpace on 2012-04-13T19:19:22Z (GMT). No. of bitstreams: 2 Dissertacao_ModelagemObjetosTridimensionais.pdf: 3042891 bytes, checksum: 373f6a0d7c39f681ae694cbf6d72b2b9 (MD5) license_rdf: 23898 bytes, checksum: e363e809996cf46ada20da1accfcd9c7 (MD5) Previous issue date: 2010 / Esta dissertação aborda metodologias de criação de objetos tridimensionais destinados a ambientes virtuais interativos, contextualizando as principais técnicas de implementação computacional envolvidas no processo. Foi utilizado como estudo de caso o Sistema de Instruções Técnicas Virtuais, desenvolvido pelo Laboratório de Realidade Virtual (LaRV) da Universidade Federal do Pará (UFPA) para as Centrais Elétricas do Norte do Brasil S/A (Eletronorte), como recurso de treinamento e simulação de procedimentos de manutenção e operação da Usina Hidrelétrica de Tucuruí. / Esta dissertação aborda metodologias de criação de objetos tridimensionais destinados a ambientes virtuais interativos, contextualizando as principais técnicas de implementação computacional envolvidas no processo. Foi utilizado como estudo de caso o Sistema de Instruções Técnicas Virtuais, desenvolvido pelo Laboratório de Realidade Virtual (LaRV) da Universidade Federal do Pará (UFPA) para as Centrais Elétricas do Norte do Brasil S/A (Eletronorte), como recurso de treinamento e simulação de procedimentos de manutenção e operação da Usina Hidrelétrica de Tucuruí. / This dissertation discusses creation paradigms of tridimensional objects, to be used into interactive virtual environments, contextualizing the main techniques for computing implementation of the whole process. As a case study, it was used the Virtual Technical Instructions System, developed by Virtual Reality Laboratory at Federal University of Pará, to Eletronorte S/A, as an auxiliary resource of simulation and training in maintenance and operation procedures at Tucuruí Hydroelectric Power Plant.
348

Prontuário eletrônico do centro de atendimento a pacientes especiais: desenvolvimento e implementação / Electronic patient record in the Special Care Dentistry Center: development and implementation

Alexandre Fraige 05 June 2007 (has links)
O Prontuário Eletrônico do Paciente (PEP) é atualmente um dos principais temas de pesquisa e desenvolvimento no âmbito da Informática em Saúde. No entanto, no Brasil e em odontologia, poucos são os estudos publicados. Frente às deficiências apresentadas no fluxo das informações clínicas nos prontuários baseados em papel e visando o aperfeiçoamento deste fluxo para benefício do paciente e da própria instituição, nos propusemos a desenvolver um prontuário eletrônico direcionado ao atendimento odontológico de pacientes portadores de necessidades especiais do Centro de Atendimento a Pacientes Especiais da Faculdade de Odontologia da USP. Para tanto foi utilizada a metodologia de desenvolvimento denominada ?modelagem orientada ao objeto?. O software foi desenvolvido em conjunto com o Centro de Tecnologia XML do Instituto de Pesquisas Tecnológicas de São Paulo. Uma vez terminado, o software foi submetido ao processo de obtenção de registro na Agência USP de Inovações. / The Electronic Patient Record (EPR) is currently one of the main subjects of research and development in the scope of Health Informatics. In Dentistry, however, few are the published studies in Brazil. Facing deficiencies presented in the clinical information flow in paper based patient record and aiming to improve this flow for both patient and institution benefit, we proposed to develop a electronic patient record system suited to Dentistry attendance of patients with special needs of the Special Care Dentistry Center of University of São Paulo. For such task, it was utilized the ?Object-oriented modeling? software development methodology. The software was developed with the Center of Technology XML of the Institute of Technological Research of São Paulo. Once finished, it was submitted to patent attainment at the University of São Paulo Innovations Agency.
349

PD4CAT: método de design participativo para desenvolvimento customizado de alta tecnologia assistiva. / PD4CAT: a participatory design method for customized development of high assistive technology.

Luciana Correia Lima de Faria Borges 04 June 2014 (has links)
Tecnologias assistivas computacionais, ou Alta Tecnologia Assistiva (ATA) não podem prescindir de customização para atender efetivamente pessoas com deficiência nas atividades de vida diária e em terapia de reabilitação. Hoje, tais tecnologias são ofertadas de forma padronizada, cabendo aos terapeutas adaptarem-nas para que seus pacientes possam usá-las. O design participativo (DP), como metodologia de envolvimento ativo do usuário no processo de projeto, adequa-se bem à ideia de customização de ATAs, permitindo a participação ativa do usuário com deficiência como co-designer da sua solução. Apesar disso, são raros os estudos que apresentam recomendações para o DP incluindo esses usuários. Quando se considera métodos de DP para incluir pessoas com deficiência, independentemente da deficiência apresentada, nenhum trabalho de pesquisa foi localizado. Visando preencher essa lacuna, esta pesquisa tem o objetivo de propor o PD4CAT Participatory Design for Customized Assistive Technology, método que objetiva auxiliar equipes multidisciplinares a conceberem soluções computacionais customizadas utilizando o DP para o envolvimento ativo da equipe - que inclui a pessoa com deficiência, seus terapeutas e cuidadores - no ciclo de design e desenvolvimento. A metodologia adotada neste trabalho para obter a proposta do PD4CAT foi a pesquisa-ação, em dois ciclos que inseriram os pesquisadores em instituições de reabilitação. Neste processo, foram realizados dois estudos de caso de desenvolvimento de ATAs personalizadas para dois pacientes com paralisia cerebral, com deficiências motora e verbal, sendo um adulto de quarenta e seis anos (M) e, uma criança de quatro anos (MI). Resultaram deste processo as diretrizes que compõem o PD4CAT, bem como as soluções em TAs. / Customization is essential for Computer Assistive Technologies, or High Assistive Technology (HAT), to effectively meet the needs of people with disabilities in their daily activities and in rehabilitation therapy. These technologies are currently provided in a standardized way, and therapists have to adapt them so that their patients can use them. Participatory design (PD), as a methodology that actively involves the user in the design process, is very adequate to customize HATs, allowing active participation by users with impairments as co-designers of their solutions. However, few are the studies presenting recommendations to PD including these users. No research work was spotted considering PD methods to include people with disabilities, independently of their impairment. Aiming to fill this gap, this research proposes PD4CAT Participatory Design for Customized Assistive Technology, a method to aid multidisciplinary teams to conceive customized computer solutions using PD for actively involving the team - which includes persons with impairments, their therapists and caretakers in the design and development cycle. The methodology adopted in this work for obtaining the PD4CAT proposal was the research-action, in two cycles that inserted the researchers in rehabilitation institutions. In the process, two case studies were conducted for developing customized HATs for two patients with cerebral palsy, with motor and verbal impairments, one being a forty-six-year old adult (M) and a four-year-old child (MI). This process resulted in the guidelines composing PD4CAT, as well as the AT solutions.
350

Um processo de desenvolvimento orientado a objetos com suporte à verificação formal de inconsistências. / An object-oriented development process with support to inconsistencies formal verification.

Thiago Carvalho de Sousa 29 November 2013 (has links)
As melhores práticas de engenharia de software indicam que a atividade de verificação é fundamental para se alcançar o mínimo de qualidade na construção de um software. Nos processos de desenvolvimento baseados na UML, um dos seus focos principais é detectar inconsistências nos diagramas representativos do software. No entanto, a maioria desses processos, como o Iconix, aplica apenas técnicas informais (ex: inspeções visuais nos modelos), fazendo com que muitas vezes essa atividade seja negligenciada pelos desenvolvedores. Por outro lado, com o avanço das ferramentas automatizadas de verificação, os métodos formais, tais como o Event-B, estão atraindo cada vez mais a atenção das empresas de software. Porém, ainda é difícil convencer os desenvolvedores a adotá-los, pois não estão acostumados com os conceitos matemáticos envolvidos. Assim, este trabalho apresenta uma proposta de inclusão do Event-B no Iconix, dando origem ao BIconix, um processo de desenvolvimento orientado a objetos com suporte à verificação formal de inconsistências. Mais especificamente, esta tese aborda a tradução automática dos quatro diagramas existentes no Iconix (classes, casos de uso, robustez e sequência) para o Event-B, além de mostrar como esta formalização pode auxiliar na atividade de verificação em pontos específicos e bem definidos no processo proposto. / The best practices of software engineering indicate that the verification activity is essential to achieve some quality during the software construction. In UML-based development processes, one of its main focuses is the detection of inconsistencies in diagrams that represent the software. However, most of these processes, such as Iconix, apply only informal techniques (eg. visual model inspections), often implying the negligence of that activity by developers. Moreover, with the advance of automated verification tools, formal methods, such as Event-B, are increasingly attracting the attention of software companies. However, it is still difficult to convince developers to adopt them, because they are not acquainted with some mathematical concepts. Thus, this paper presents a proposal for the inclusion of Event-B within Iconix, giving rise to BIconix, an object-oriented development process that supports automatic inconsistencies formal verification. More specifically, this thesis addresses the translation of the four existing diagrams in Iconix (classes, use cases, robustness and sequence) to Event- B, and show how this formalization can assist the verification activity in well-defined check points of the proposed process.

Page generated in 0.0915 seconds