Author(s):
Neves, Renato 
Date: 2013
Persistent ID: http://hdl.handle.net/1822/28077
Origin: RepositóriUM - Universidade do Minho
Subject(s): Formal methods; Modelling; Reconfigurable systems; Hybrid logics; Institutions; Métodos formais; Modelação; Sistemas reconfiguráveis; Lógicas híbridas; Instituições
Description
Dissertação de mestrado em Engenharia Informática Formal methods are mathematical techniques used to certify safe systems.
Such methods abound and have been successfully used in classical Engineering
domains, yet informatics is the exception. There, they are still
immature and costly; furthermore, software engineers frequently view
them with "fear". Thus, the use of formal methods is typically restricted
to cases where they are essential. In other words, they are mostly used
in the class of systems where safety is imperative, as the lack of it can
lead to significant losses (material or human). We denote such systems
critical. The present is leading us to a future where critical systems are
ubiquitous.
Recent research in the Mondrian project emphasises the need for
expressive logics to formally specify reconfigurable systems, i.e., systems
capable of evolving in order to adapt to the different contexts induced
by the dynamics of their surroundings. In the same project, theoretical
foundations for the formal specification of reconfigurable systems, were
developed in a sound, generic, and systematic way, resorting for this to
hybrid logics – their intrinsic properties make them natural candidates for
such job. From those foundations a methodology for specifying reconfigurable
systems was built and proposed: Instead of choosing a logic for
the specification, build an hybrid ad-hoc one, by taking into account the
particular characteristics of each reconfigurable system to be specified.
The purpose of this dissertation is to bring the proposed methodology
into practice, by creating suitable tools for it, and by illustrating its
application to relevant case studies. Métodos formais são técnicas matemáticas usadas para certificar sistemas
fiáveis. Tais métodos são comuns e usados com sucesso nas engenharias
clássicas. No entanto, informática é a excepção. No que respeita este
campo, os métodos formais são prematuros e relativamente dispendiosos;
para além disso, os engenheiros de software vêem estas técnicas
com alguma apreensão. Assim, o emprego de métodos formais está tipicamente
restrito a casos onde são absolutamente essenciais. Por outras
palavras, são maioritariamente usados na classe de sistemas, cujas falhas
têm o potencial de tragédia, seja ela material ou humana; tais sistemas
têm a denominação de críticos. O presente leva-nos para um futuro em
que os sistemas críticos são ubíquos.
Investigação recente no project Mondrian enfatiza a necessidade de
lógicas expressivas, para especificar formalmente sistemas reconfiguráveis,
i.e., sistemas que evoluem de modo a se adaptarem aos diferentes contextos,
induzidos pela dinâmica do meio que os rodeia. No mesmo projecto,
bases teóricas para a especificação formal de sistemas reconfiguráveis foram
establecidas de forma sólida, genérica e sistemática, recorrendo-se
para isso às lógicas híbridas – as suas propriedades intrínsecas, fazem delas
candidatos naturais para a especificação de sistemas reconfiguráveis.
Dessas teorias foi inferida e proposta uma metodologia para especificar
sistemas reconfiguráveis: Em vez de escolher uma lógica para a especificação,
construir uma outra, híbrida ad-hoc, tendo em conta as características
particulares de cada sistema reconfigurável a especificar.
O propósito desta dissertação é de trazer a metodologia proposta à
práctica, criando-se para isso, ferramentas que a suportem, e ilustrando a
sua aplicação a casos de estudo relevantes.
