Utilize este identificador para referenciar este registo:
https://hdl.handle.net/1822/28077
Título: | Proof support for hybridised logics |
Autor(es): | Neves, Renato Jorge Araújo |
Orientador(es): | Martins, Manuel A. Barbosa, L. S. |
Palavras-chave: | Formal methods Modelling Reconfigurable systems Hybrid logics Institutions Métodos formais Modelação Sistemas reconfiguráveis Lógicas híbridas Instituições |
Data: | 27-Set-2013 |
Resumo(s): | 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. |
Tipo: | Dissertação de mestrado |
Descrição: | Dissertação de mestrado em Engenharia Informática |
URI: | https://hdl.handle.net/1822/28077 |
Acesso: | Acesso aberto |
Aparece nas coleções: | BUM - Dissertações de Mestrado |
Ficheiros deste registo:
Ficheiro | Descrição | Tamanho | Formato | |
---|---|---|---|---|
eeum_di_dissertacao_pg17229.pdf | 907,31 kB | Adobe PDF | Ver/Abrir |