Proof support for hybridised logics

Abstract

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.