Página 1 dos resultados de 3163 itens digitais encontrados em 0.023 segundos

JML- Based formal development of a Java card application for managing medical appointments

Rodrigues, Ricardo Miguel Soares
Fonte: Universidade da Madeira Publicador: Universidade da Madeira
Tipo: Dissertação de Mestrado
Publicado em //2009 ENG
Relevância na Pesquisa
56.21%
Although formal methods can dramatically increase the quality of software systems, they have not widely been adopted in software industry. Many software companies have the perception that formal methods are not cost-effective cause they are plenty of mathematical symbols that are difficult for non-experts to assimilate. The Java Modelling Language (short for JML) Section 3.3 is an academic initiative towards the development of a common formal specification language for Java programs, and the implementation of tools to check program correctness. This master thesis work shows how JML based formal methods can be used to formally develop a privacy sensitive Java application. This is a smart card application for managing medical appointments. The application is named HealthCard. We follow the software development strategy introduced by João Pestana, presented in Section 3.4. Our work influenced the development of this strategy by providing hands-on insight on challenges related to development of a privacy sensitive application in Java. Pestana’s strategy is based on a three-step evolution strategy of software specifications, from informal ones, through semiformal ones, to JML formal specifications. We further prove that this strategy can be automated by implementing a tool that generates JML formal specifications from a welldefined subset of informal software specifications. Hence...

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.

Sousa, Thiago Carvalho de
Fonte: Biblioteca Digitais de Teses e Dissertações da USP Publicador: Biblioteca Digitais de Teses e Dissertações da USP
Tipo: Tese de Doutorado Formato: application/pdf
Publicado em 29/11/2013 PT
Relevância na Pesquisa
56.01%
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...

Especificação formal de organizações de sistemas multiagentes; Formal specification of multiagent systems organizations

Barbosa, Raquel de Miranda
Fonte: Universidade Federal do Rio Grande do Sul Publicador: Universidade Federal do Rio Grande do Sul
Tipo: Tese de Doutorado Formato: application/pdf
POR
Relevância na Pesquisa
56.13%
A abordagem de sistemas multiagentes tem sido cada vez mais utilizada para o desenvolvimento de sistemas complexos, o que despertou o interesse das pesquisas na área de engenharia de software orientada a agentes (AOSE) e modelos organizacionais. Neste contexto, esta tese estuda a aplicabilidade de alguns métodos formais tradicionais de engenharia de software para a especificação formal de organizações de sistemas multiagentes, analisando o uso da linguagem de especificação formal RSL para representar o modelo organizacional PopOrg. A escolha da linguagem RSL ocorreu pelo fato de ela ser uma linguagem de especificação formal que cobre amplo espectro de métodos de especificação formal (baseados em modelos e baseados em propriedades, aplicativos e imperativos, sequenciais e concorrentes) e o modelo PopOrg foi escolhido por ser um modelo mínimo de organização de sistemas multiagentes, concebido para representar o conjunto mínimo de aspectos estruturais e operacionais que tais organizações devem ter. O uso da linguagem RSL foi avaliado tanto para a especificação do aspecto estrutural dos sistemas PopOrg, quanto para especificação operacional desses sistemas. Um estudo preliminar realizado com a linguagem CSP para a especificação operacional do modelo PopOrg também é apresentado...

Métodos formais algébricos para geração de invariantes; Algebraic formal methods for invariant generation

Rachid Rebiha
Fonte: Biblioteca Digital da Unicamp Publicador: Biblioteca Digital da Unicamp
Tipo: Tese de Doutorado Formato: application/pdf
Publicado em 12/08/2011 PT
Relevância na Pesquisa
56.13%
É bem sabido que a automação e a eficácia de métodos de verificação formal de softwares, sistemas embarcados ou sistemas híbridos, depende da facilidade com que invariantes precisas possam ser geradas automaticamente a partir do código fonte. Uma invariante é uma propriedade, especificada sobre um local específico do código fonte, e que sempre se verifica a cada execução de um sistema. Apesar dos progressos enormes ao longo dos anos, o problema da geração de invariantes ainda está em aberto para tanto programas não-lineares discretos, como para sistemas não-lineares híbridos. Nesta tese, primeiramente, apresentamos novos métodos computacionais que podem automatizar a descoberta e o fortalecimento de relações não-lineares entre as variáveis de um programa que contém laços não-lineares, ou seja, programas que exibem relações polinomiais multivariadas e manipulações fracionarias. Além disso, a maioria dos sistemas de segurança críticos, tais como aviões, automóveis, produtos químicos, usinas de energia e sistemas biológicos, operam semanticamente como sistemas híbridos não-lineares. Nesse trabalho, apresentamos poderosos métodos computacionais que são capazes de gerar bases de ideais polinomiais de invariantes não-lineares para sistemas híbridos não-lineares. Em segundo lugar...

An integrated formal methods tool-chain and its application to verifying a file system model

Ferreira, Miguel A.; Oliveira, José Nuno Fonseca
Fonte: Springer-Verlag Publicador: Springer-Verlag
Tipo: Artigo de Revista Científica
Publicado em //2009 ENG
Relevância na Pesquisa
65.95%
Tool interoperability as a mean to achieve integration is among the main goals of the international Grand Challenge initiative. In the context of the Verifiable file system mini-challenge put forward by Rajeev Joshi and Gerard Holzmann, this paper focuses on the integration of different formal methods and tools in modelling and verifying an abstract file system inspired by the Intel (R) Flash File System Core. We combine high-level manual specification and proofs with current state of the art mechanical verification tools into a tool-chain which involves Alloy, VDM++ and HOL. The use of (pointfree) relation modelling provides the glue which binds these tools together.; Mondrian Project funded by the Portuguese NSF under contract PTDC/EIA-CCO/108302/2008

Certification of open-source software : a role for formal methods?

Barbosa, L. S.; Cerone, Antonio; Petrenko, Alexander; Shaikh, Siraj A.
Fonte: CRL Publishing Publicador: CRL Publishing
Tipo: Artigo de Revista Científica
Publicado em //2010 ENG
Relevância na Pesquisa
65.98%
Despiteitshugesuccessandincreasingincorporationincom- plex, industrial-strength applications, open source software, by the very nature of its open, unconventional, distributed development model, is hard to assess and certify in an effective, sound and independent way. This makes its use and integration within safety or security-critical systems, a risk. And, simultaneously an opportunity and a challenge for rigourous, mathematically based, methods which aim at pushing software analysis and development to the level of a mature engineering discipline. This paper discusses such a challenge and proposes a number of ways in which open source development may benefit from the whole patrimony of formal methods.

Representations in solving a word problem: The informal development of formal methods

Amado, Nélia; Carreira, Susana; Nobre, Sandra; Ponte, João Pedro da
Fonte: Universidade de Lisboa Publicador: Universidade de Lisboa
Tipo: Conferência ou Objeto de Conferência
Publicado em //2010 ENG
Relevância na Pesquisa
65.95%
The aim of this paper is to analyse different types of representations used by grade 7 and 8 students in solving a word problem. The problem was offered to finalists of a mathematics contest held outside the classroom. The analysis of the products of different students show the key role of the representations used to solve the problem and how they are critical in the development of a sustainable process for informal learning of formal methods of solving systems of linear equations.

Representation problem solving formal methods word problem

Amado, Nélia; Carreira, Susana Paula Graça; Nobre, Sandra; Ponte, João Pedro da
Fonte: Universidade do Algarve Publicador: Universidade do Algarve
Tipo: Conferência ou Objeto de Conferência
Publicado em //2010 ENG
Relevância na Pesquisa
65.95%
The aim of this paper is to analyse different types of representations used by grade 7 and 8 students in solving a word problem. The problem was offered to finalists of a mathematics contest held outside the classroom. The analysis of the products of different students show the key role of the representations used to solve the problem and how they are critical in the development of a sustainable process for informal learning of formal methods of solving systems of linear equations.

Integrating Object-Oriented Analysis and Formal Specification

Araújo Júnior,João; Sawyer,Pete
Fonte: Sociedade Brasileira de Computação Publicador: Sociedade Brasileira de Computação
Tipo: Artigo de Revista Científica Formato: text/html
Publicado em 01/07/1998 EN
Relevância na Pesquisa
46.13%
One of the main inhibitors to the widespread acceptance of formal specification methods is the difficulty of integrating formal specification with the development process. Integrated methods seek to mitigate this difficulty by integrating formal specification with widely used structured requirements analysis methods. Several structured and formal methods are object-oriented. This paper describes a prototype integrated method and support tool called Metamorphosis that exploits the object paradigm to integrate OMT and Object-Z. Metamorphosis is presented here to demonstrate how object-oriented analysis methods such as OMT may be augmented to provide the additional rigour of formal analysis.

A rigorous methodology for developing GUI-based DSL formal tools

Silva, Robson dos Santos e; Mota, Alexandre Cabral (orientador)
Fonte: Universidade Federal de Pernambuco Publicador: Universidade Federal de Pernambuco
Tipo: Dissertação
EN
Relevância na Pesquisa
56.18%
A Engenharia Dirigida a Modelos ou (MDE—Model-Driven Engineering) é uma metodologia de desenvolvimento de software que se concentra na criação e manipulação de modelos específicos de domínio. É comum o uso de linguagens específicas de domínio (DSL) para descrever os elementos concretos de tais modelos. Ferramentas de MDE podem facilmente construir linguagens específicas de domínio (DSL), capturando seus aspectos sintáticos assim como sua semântica estática. No entanto, ainda não possuem uma forma clara de capturar a semântica dinâmica de uma DSL, assim como a verificação de propriedades de domínio antes da geração de código executável. Métodos formais são tidos como uma solução para prover software correto, onde podemos garantir que desejadas propriedades são satisfeitas. Infelizmente, as ferramentas de métodos formais disponíveis concentram-se quase que exclusivamente na semântica enquanto que a interação homem-computador é "deixada para o usuário". Indústrias em que a segurança é crítica, usam representações matemáticas para lidar com os seus domínios de problemas. Historicamente, essas representações matemáticas têm um apelo gráfico. Por exemplo, Cadeias de Markov e Árvores de Falha. Em geral...

BSmart: desenvolvimento rigoroso de aplicações Java Card com base no método formal B

Gomes, Bruno Emerson Gurgel
Fonte: Universidade Federal do Rio Grande do Norte; BR; UFRN; Programa de Pós-Graduação em Sistemas e Computação; Ciência da Computação Publicador: Universidade Federal do Rio Grande do Norte; BR; UFRN; Programa de Pós-Graduação em Sistemas e Computação; Ciência da Computação
Tipo: Dissertação Formato: application/pdf
POR
Relevância na Pesquisa
56.07%
Java Card technology allows the development and execution of small applications embedded in smart cards. A Java Card application is composed of an external card client and of an application in the card that implements the services available to the client by means of an Application Programming Interface (API). Usually, these applications manipulate and store important information, such as cash and confidential data of their owners. Thus, it is necessary to adopt rigor on developing a smart card application to improve its quality and trustworthiness. The use of formal methods on the development of these applications is a way to reach these quality requirements. The B method is one of the many formal methods for system specification. The development in B starts with the functional specification of the system, continues with the application of some optional refinements to the specification and, from the last level of refinement, it is possible to generate code for some programming language. The B formalism has a good tool support and its application to Java Card is adequate since the specification and development of APIs is one of the major applications of B. The BSmart method proposed here aims to promote the rigorous development of Java Card applications up to the generation of its code...

Formal verification of PLC programs using the B Method; Formal verification of PLC programs using the B method

Barbosa, Haniel Moreira
Fonte: Universidade Federal do Rio Grande do Norte; BR; UFRN; Programa de Pós-Graduação em Sistemas e Computação; Ciência da Computação Publicador: Universidade Federal do Rio Grande do Norte; BR; UFRN; Programa de Pós-Graduação em Sistemas e Computação; Ciência da Computação
Tipo: Dissertação Formato: application/pdf
POR
Relevância na Pesquisa
56.11%
PLCs (acronym for Programmable Logic Controllers) perform control operations, receiving information from the environment, processing it and modifying this same environment according to the results produced. They are commonly used in industry in several applications, from mass transport to petroleum industry. As the complexity of these applications increase, and as various are safety critical, a necessity for ensuring that they are reliable arouses. Testing and simulation are the de-facto methods used in the industry to do so, but they can leave flaws undiscovered. Formal methods can provide more confidence in an application s safety, once they permit their mathematical verification. We make use of the B Method, which has been successfully applied in the formal verification of industrial systems, is supported by several tools and can handle decomposition, refinement, and verification of correctness according to the specification. The method we developed and present in this work automatically generates B models from PLC programs and verify them in terms of safety constraints, manually derived from the system requirements. The scope of our method is the PLC programming languages presented in the IEC 61131-3 standard, although we are also able to verify programs not fully compliant with the standard. Our approach aims to ease the integration of formal methods in the industry through the abbreviation of the effort to perform formal verification in PLCs; Controladores Lógico Programáveis (PLCs Programmable Logic Controllers...

Can formal methods make automotive business sense? A classification of formal methods

McElligott, Pat; Mjeda, Anila; Thiel, Steffen
Fonte: SAE International Publicador: SAE International
Tipo: info:eu-repo/semantics/conferenceObject; all_ul_research; ul_published_reviewed
ENG
Relevância na Pesquisa
46.14%
peer-reviewed; Legislative bodies are directing that automotive products comply with stringent safety levels. The liability for the safety of passengers in an automobile has traditionally been quite complex. Other transport sectors are externally regulated, and liability lies with the manufacturer or the transport service provider. The automotive industry is self-regulated and the individual driver carries a significant liability. Software and electronics increasingly provide greater control of automotive safety, possibly reducing driver liability, and increasing the need for more formal software development methods. The automotive business model, however, also presents challenges to the effective use of formal methods. An automotive design change costing €600 per vehicle could consume 100% of gross margin. In aviation, this cost represents 0.01% of gross margin. [1] [2]. The automotive industry is responding to the increasing impact of automotive software with the development of standards such as AUTOSAR [3], and EU funded projects such as ATESST [4] and EASIS [5]. They propose architectures which might deliver the benefits of best software engineering practice to the industry. In terms of safety, they recommend existing accepted standards such as IEC61508 [6]...

International Refinement Workshop and Formal Methods Pacific ’98

Fonte: Universidade Nacional da Austrália Publicador: Universidade Nacional da Austrália
Tipo: Conference item Formato: 1112794 bytes; 356 bytes; application/pdf; application/octet-stream
EN_AU
Relevância na Pesquisa
46.13%
The International Refinement Workshop and Formal Methods Pacific 1998 (IRW/FMP'98), as the title suggests, is a combined event. FMP'98 itself incorporates the 7th Australasian Refinement Workshop and the 4th New Zealand Formal Program Development Colloquium, and follows the inaugural FMP'97 in Wellington. The Australasian Refinement Workshop (ARW) series began in 1990, to provide a forum for researchers in program refinement. The New Zealand Formal Program Development Colloquium (NZFPDC) series began in 1994 with similar aims. In 1997 the ARW and NZFPDC joined forces in Wellington under the umbrella name Formal Methods Pacific (FMP). The more general name, and regional focus better reflects the broader range of interests of participants and presented papers, while satisfying the need for a regional conference covering formal methods. The event became the International Refinement Workshop with the postponement of the 7th British Refinement Workshop, and the welcome support of IRW/FMP'98 by the British Computer Society FACS. IRW/FMP'98 is being held concurrently with The 11th International Conference on Theorem Proving in Higher Order Logics (TPHOLs'98) at The Australian National University. Papers for IRW/FMP'98 were sought in two streams: Completed Work and Work in Progress. The Work in Progress stream provides a forum for discussion of work that has not yet reached maturity. Submissions were vetted for relevance...

Modeling NASA swarm-based systems:using agent-oriented software engineering and formal methods

Pena, Joaquin; Rouff, Christopher; Hinchey, Mike; Ruiz-Cortes, Antonio
Fonte: Association for Computing Machinery Publicador: Association for Computing Machinery
Tipo: Article; all_ul_research; ul_published_reviewed; none
ENG
Relevância na Pesquisa
65.95%
peer-reviewed; The need to collect new data and perform new science is causing the complexity of NASA missions to continually increase. This complexity needs to be controlled via new technological advancements and balanced with a reduction in mission and operation costs. Planned and hypothesized missions involve self-management,biological-inspiration based on swarms, and autonomous operation as a means of achieving these goals.We consider a tailored software engineering approach to developing such systems based on agent-oriented software engineering and formal methods. We report on the advances in modeling, implementing, and testing NASA swarm-based concept missions.

Proceedings Quantities in Formal Methods

Fahrenberg, Uli; Legay, Axel; Thrane, Claus
Fonte: Universidade Cornell Publicador: Universidade Cornell
Tipo: Artigo de Revista Científica
Publicado em 14/12/2012
Relevância na Pesquisa
56.11%
This volume contains the proceedings of the Workshop on Quantities in Formal Methods, QFM 2012, held in Paris, France on 28 August 2012. The workshop was affiliated with the 18th Symposium on Formal Methods, FM 2012. The focus of the workshop was on quantities in modeling, verification, and synthesis. Modern applications of formal methods require to reason formally on quantities such as time, resources, or probabilities. Standard formal methods and tools have gotten very good at modeling (and verifying) qualitative properties: whether or not certain events will occur. During the last years, these methods and tools have been extended to also cover quantitative aspects, notably leading to tools like e.g. UPPAAL (for real-time systems), PRISM (for probabilistic systems), and PHAVer (for hybrid systems). A lot of work remains to be done however before these tools can be used in the industrial applications at which they are aiming.

Proceedings 2nd Workshop on Formal Methods in the Development of Software

Andrés, César; Llana, Luis
Fonte: Universidade Cornell Publicador: Universidade Cornell
Tipo: Artigo de Revista Científica
Publicado em 08/07/2012
Relevância na Pesquisa
46.12%
This volume contains the proceedings of the 2nd WorkShop on Formal Methods in the Development of Software (WS-FMDS 2012). The workshop was held in Paris, France on August 30th, 2012 as a satellite event to the 18th International Symposium on Formal Methods (FM-2012). The aim of WS-FMDS 2012 is to provide a forum for researchers who are interested in the application of formal methods on systems which are being developing with a software methodology. In particular, this workshop is intended to bring together scientists and practitioners who are active in the area of formal methods and interested in exchanging their experiences in the industrial usage of these methods. This workshop also strives to promote research and development for the improvement of formal methods and tools for industrial applications.

Proceedings First Latin American Workshop on Formal Methods

Aguirre, Nazareno; Ribeiro, Leila
Fonte: Universidade Cornell Publicador: Universidade Cornell
Tipo: Artigo de Revista Científica
Publicado em 02/01/2014
Relevância na Pesquisa
46.12%
Formal approaches to software development are techniques that aim at developing quality software by employing notations, analysis processes, etc., based on mathematical grounds. Although traditionally they aim at increasing software correctness, formal techniques have been applied to various other aspects of software quality. Moreover, while originally formal methods employed complex "heavyweight" mechanisms for analysis (often manual or semi automated), there has been progress towards embracing "lightweight", many times fully automated, analysis techniques, that broaden the adoption of formal methods in various software engineering contexts. The Latin American Workshop on Formal Methods brings together researchers working in formal methods, and related areas such as automated analysis. In particular, the workshop provides a venue for Latin American researchers working in these areas, to promote their interaction and collaboration. The workshop was held in August as a satellite event of CONCUR 2013. It took place in Buenos Aires, Argentina's capital and largest city, and one of the most interesting cultural places in South America.

Experiences with alloy in undergraduate formal methods

Lutz, Michael
Fonte: ASEE - American Society for Engineering Education Publicador: ASEE - American Society for Engineering Education
Tipo: Proceedings
EN_US
Relevância na Pesquisa
65.95%
At the core of all engineering endeavors is the modeling of proposed system designs and the use of these models to determine system properties. While some models are physical, the vast majority use mathematics to both describe and analyze the consequences of design decisions. In the case of traditional engineering disciplines, most models are based on continuous mathematics, e.g., calculus and differential equations. The situation is quite different in software engineering, however, where the applicable models are more likely to be drawn from discrete mathematics, logic, and set theory. The term of art for such modeling approaches is formal methods.; Event: 2006 ASEE Annual Conference & Exposition Location: Chicago, IL Date: June 18-21, 2006

Formal Support to Security Protocol Development: A Survey

López Pimentel,Juan Carlos; Monroy,Raúl
Fonte: Centro de Investigación en computación, IPN Publicador: Centro de Investigación en computación, IPN
Tipo: Artigo de Revista Científica Formato: text/html
Publicado em 01/09/2008 EN
Relevância na Pesquisa
55.91%
Security protocols aim to allow two or more principals to establish a secure communication over a hostile network, such as the Internet. The design of security protocols is particularly error-prone, because it is difficult to anticipate what an intruder may achieve interacting through a number of protocol runs, claiming to be an honest participant. Thus, the verification of security protocols has attracted a lot of interest in the formal methods community and as a result lots of verification techniques/tools, as well as good practices for protocol design, have appeared in the two last decades. In this paper, we describe the state of the art in automated tools that support security protocol development. This mainly involves tools for protocol verification and, to a lesser extent, for protocol synthesis and protocol diagnosis and repair. Also, we give an overview of the most significant principles for the design of security protocols and of the major problems that still need to be addressed in order to ease the development of security protocols.