Submitted by Luiz Felipe Barbosa (luiz.fbabreu2@ufpe.br) on 2015-03-12T14:30:39Z
No. of bitstreams: 2
Dissertacao Robson Santos Silva.pdf: 2657380 bytes, checksum: e8bfe7912e7136af0fbf6082153115fd (MD5)
license_rdf: 1232 bytes, checksum: 66e71c371cc565284e70f40736c94386 (MD5) / Approved for entry into archive by Daniella Sodre (daniella.sodre@ufpe.br) on 2015-03-13T12:57:10Z (GMT) No. of bitstreams: 2
Dissertacao Robson Santos Silva.pdf: 2657380 bytes, checksum: e8bfe7912e7136af0fbf6082153115fd (MD5)
license_rdf: 1232 bytes, checksum: 66e71c371cc565284e70f40736c94386 (MD5) / Made available in DSpace on 2015-03-13T12:57:10Z (GMT). No. of bitstreams: 2
Dissertacao Robson Santos Silva.pdf: 2657380 bytes, checksum: e8bfe7912e7136af0fbf6082153115fd (MD5)
license_rdf: 1232 bytes, checksum: 66e71c371cc565284e70f40736c94386 (MD5)
Previous issue date: 2013-08-23 / It is well-known that model-driven engineering (MDE) is a software development methodology
that focuses on creating and exploiting (specific) domain models. Domain models
(conceptually) capture all the topics (for instance, entities and their attributes, roles, and
relationships as well as more specific constraints) related to a particular problem. It is
common to use domain-specific languages (DSL) to describe the concrete elements of
such models.
MDE tools can easily build domain-specific languages (DSL), capturing syntactic
as well as static semantic information. However, we still do not have a clear way of
capturing the dynamic semantics of a DSL as well as checking the domain properties prior
to generating the implementation code. Formal methods are a well-known solution for
providing correct software, where we can guarantee the satisfaction of desired properties.
Unfortunately the available formal methods tools focus almost exclusively on semantics
whereas human-machine interaction is "left to the user". Several industries, and in
particular the safety-critical industries, use mathematical representations to deal with
their problem domains. Historically, such mathematical representations have a graphical
appeal. For example, Markov chains and fault-trees are used in safety assessment processes
to guarantee that airplanes, trains, and other safety-critical systems work within
allowed safety margins. In general, due to the difficulty to obtain correct software, such
industries use Commercial Off-The-Shelf (COTS) software or build them specifically
to satisfy their needs with a related testing campaign effort. Such DSLs are difficult
to capture, using just MDE tools for instance, because they have specific semantics to
provide the desired (core) information for the industries that use them.
In this sense, given a DSL (L) composed of a syntax and static semantics (SSL),
and dynamic semantics (DSL) parts, our work proposes a rigorous methodology for
combining the easiness of MDE tools, to capture SSL, with the correctness assured by
formal methods, to capture DSL as well and check its properties. This combination
is specifically handled in the following way, we capture all aspects of L using formal
methods, check the desired properties and adjust if necessary. After that, we automatically
translate part of it in terms of constructs of a MDE tool, from which we can build a
user-friendly (GUI) front-end very easily (automatically). Finally, we link the front-end
code to the automatically synthesized code from the formal dynamic semantics back-end.
Although we require the use of a formal methods tool, the distance from the mathematical
representations used in industry and the formal methods notation is very close.
With this proposed methodology we intend that safety-critical industries create their domain specific software as easy as possible and with the desired static and dynamic
properties formally checked. / 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, devido à dificuldade em obter softwares formalmente verificados, essas
indústrias utilizam sistemas comerciais prontos para uso (Commercial Off-the-shelf -
COTS) ou os constróem especificamente para satisfazerem as suas necessidades com
um esforço considerável em testes. Tais DSLs são difíceis de capturar, usando apenas
ferramentas MDE por exemplo, porque possuem uma semântica particular para prover as
informações específicas desejadas para as indústrias que as utilizam.
Neste sentido, dada uma DSL (L), composta por sintaxe e semântica estática (SSL), e
semântica dinâmica (DSL), este trabalho propõe uma metodologia rigorosa para combinar
a facilidade de ferramentas MDE em capturar SSL, com a corretude assegurada por
métodos formais para capturar DSL e verificar suas propriedades. Esta combinação é
especificamente tratada da seguinte maneira: captura-se todos os aspectos de L utilizando
métodos formais, verificam-se as propriedades desejadas e as ajustam caso necessário.
Em seguida, parte de L é traduzida automaticamente em termos de artefatos para uma
ferramenta MDE, a partir da qual é possível construir uma interface amigável (front-end)
facilmente (automaticamente). Por fim, o código do front-end é integrado com o código
sintetizado automaticamente a partir da semântica dinâmica formal (back-end).
| Identifer | oai:union.ndltd.org:IBICT/oai:repositorio.ufpe.br:123456789/12366 |
| Date | 23 August 2013 |
| Creators | Silva, Robson dos Santos e |
| Contributors | Mota, Alexandre Cabral |
| Publisher | Universidade Federal de Pernambuco |
| Source Sets | IBICT Brazilian ETDs |
| Language | English |
| Detected Language | English |
| Type | info:eu-repo/semantics/publishedVersion, info:eu-repo/semantics/masterThesis |
| Source | reponame:Repositório Institucional da UFPE, instname:Universidade Federal de Pernambuco, instacron:UFPE |
| Rights | Attribution-NonCommercial-NoDerivs 3.0 Brazil, http://creativecommons.org/licenses/by-nc-nd/3.0/br/, info:eu-repo/semantics/openAccess |
Page generated in 0.0028 seconds