Made available in DSpace on 2014-12-17T15:47:59Z (GMT). No. of bitstreams: 1
MadielSCF_DISSERT.pdf: 1874479 bytes, checksum: dc22e7d8884791a523682f62c1e8c32c (MD5)
Previous issue date: 2011-10-07 / Coordena??o de Aperfei?oamento de Pessoal de N?vel Superior / The use of increasingly complex software applications is demanding greater investment
in the development of such systems to ensure applications with better quality. Therefore,
new techniques are being used in Software Engineering, thus making the development
process more effective. Among these new approaches, we highlight Formal
Methods, which use formal languages that are strongly based on mathematics and have a
well-defined semantics and syntax. One of these languages is Circus, which can be used
to model concurrent systems. It was developed from the union of concepts from two other
specification languages: Z, which specifies systems with complex data, and CSP, which
is normally used to model concurrent systems. Circus has an associated refinement calculus,
which can be used to develop software in a precise and stepwise fashion. Each step
is justified by the application of a refinement law (possibly with the discharge of proof
obligations). Sometimes, the same laws can be applied in the same manner in different
developments or even in different parts of a single development. A strategy to optimize
this calculus is to formalise these application as a refinement tactic, which can then be
used as a single transformation rule. CRefine was developed to support the Circus refinement
calculus. However, before the work presented here, it did not provide support for
refinement tactics. The aim of this work is to provide tool support for refinement tactics.
For that, we develop a new module in CRefine, which automates the process of defining
and applying refinement tactics that are formalised in the tactic language ArcAngelC. Finally,
we validate the extension by applying the new module in a case study, which used
the refinement tactics in a refinement strategy for verification of SPARK Ada implementations
of control systems. In this work, we apply our module in the first two phases of
this strategy / A utiliza??o de aplica??es de software cada vez mais complexas est? exigindo um
maior investimento no desenvolvimento de sistemas, garantindo uma melhor qualidade
das aplica??es. Diante desse contexto, novas t?cnicas est?o sendo utilizadas na ?rea de
Engenharia de Software, tornado o processo de desenvolvimento mais eficaz. Destacam-
se, como exemplo dessas novas abordagens, os M?todos Formais. Estes m?todos utilizam
linguagens formais que t?m sua base fundamentada na matem?tica, apresentando uma
sem?ntica e sintaxe bem definidas. Uma dessas linguagens ? Circus, que possibilita a mo-
delagem de sistemas concorrentes. Esta linguagem foi desenvolvida a partir da uni?o dos
conceitos das linguagens formais Z (que permitem a modelagem de dados complexos) e
CSP Communicating Sequential Processes (que permitem a modelagem de sistemas con-
correntes). Adicionalmente, Circus tamb?m possui um c?lculo de refinamento associado,
que pode ser utilizado para desenvolver software de forma precisa e gradual. Cada etapa
deste c?lculo ? justificada pela aplica??o de uma lei de refinamento (possivelmente com a
prova de certas condi??es chamadas de obriga??es de prova). Algumas vezes, as mesmas
leis podem ser aplicadas da mesma forma em diferentes desenvolvimentos ou mesmo em
partes diferentes de um ?nico desenvolvimento. Uma estrat?gia para otimizar esse c?l-
culo ? formalizar estas aplica??es como t?ticas de refinamento, que podem ser utilizadas
como uma simples regra de transforma??o. A ferramenta CRefine foi desenvolvida para
realizar o suporte a este c?lculo de refinamento de Circus. Entretanto, antes deste traba-
lho, essa ferramenta n?o fornecia suporte para as t?ticas. A proposta desta disserta??o ?
oferecer um suporte ferramental para a utiliza??o das t?ticas no c?lculo de refinamento de
programas Circus. Para tanto, foi desenvolvido um novo m?dulo em CRefine, que auto-
matiza o processo de defini??o e aplica??o das t?ticas de refinamento. Nesta extens?o as
t?ticas s?o formalizadas na linguagem de t?ticas para sistemas concorrentes, ArcAngelC.
Por fim, validamos a extens?o, aplicando o novo m?dulo a um estudo de caso, que utiliza
as t?ticas em uma estrat?gia de refinamento para verifica??o de implementa??es SPARK
Ada de sistemas de controle. Nesta disserta??o, aplicamos o novo modulo ?s duas fases
iniciais desta estrat?gia.
| Identifer | oai:union.ndltd.org:IBICT/oai:repositorio.ufrn.br:123456789/18037 |
| Date | 07 October 2011 |
| Creators | Conserva Filho, Madiel de Souza |
| Contributors | CPF:02386943488, http://lattes.cnpq.br/1756952696097255, Moreira, Anamaria Martins, CPF:82573611787, http://lattes.cnpq.br/5861361541278876, Sampaio, Augusto Cezar Alves, CPF:41521633487, http://lattes.cnpq.br/3977760354511853, Oliveira, Marcel Vinicius Medeiros |
| Publisher | Universidade Federal do Rio Grande do Norte, Programa de P?s-Gradua??o em Sistemas e Computa??o, UFRN, BR, Ci?ncia da Computa??o |
| Source Sets | IBICT Brazilian ETDs |
| Language | Portuguese |
| Detected Language | English |
| Type | info:eu-repo/semantics/publishedVersion, info:eu-repo/semantics/masterThesis |
| Format | application/pdf |
| Source | reponame:Repositório Institucional da UFRN, instname:Universidade Federal do Rio Grande do Norte, instacron:UFRN |
| Rights | info:eu-repo/semantics/openAccess |
Page generated in 0.0026 seconds