Contact Details / About myself

Nowadays I'm a first-year PhD student in Computer Science at Newcastle University. Previously, I did a MSc at the Federal University of Pernambuco (UFPE, 2012 - Brazil) under supervision of Juliano Iyoda, and a BSc in Computer Science at the Federal University of Bahia (UFBA, 2010 - Brazil) with conclusion work under supervision of Adolfo Duran and Aline Andrade. You can find and download some the papers I published through links on my Research Gate's profile.  More details about me are available at my profissional profile in Linkedin.

My master's dissertation title is Behavioural Preservation in Fault Tolerant Patterns and can be download from here. In order to read just the abstract, see this post. During the masters I published part of the disseration on the 14th Brazilian Symposium on Formal Methods (link). An extended version of this paper is under revision for publication in the Science of Computer Programming Journal.

My BSc's dissertation is entitled Formal Verification of the Scheduler and Synchronous Message System of a Simple Kernel (original title: Verificação formal do escalonador e do sistema de troca de mensagens síncronas de um simple kernel) and is only available in portuguese. You can download the text from this link.

In order to contact me you can post a comment in this blog. By doing it I will receive an email with your post and make effort to answer your post as soon as possible. I've regarded to translate this blog to english, as a great number of visitors are from countries where english is spoken, however I haven't had time to do it so far.

Behavioural Preservation in Fault Tolerant Patterns

 

Behavioural Preservation in Fault Tolerant Patterns

 

Abstract

In the development of critical systems it is common practise to make use of redundancy in order to achieve higher levels of reliability. There are well established design patterns that introduce redundancy and that are widely documented in the literature and adopted by the industry. However there have been few attempts to formally verify them with respect to behavioural preservation.

In this work, we purpose an approach to specify such design patterns, called here

fault tolerant patterns, using HOL. We use the theorem prover HOL4 to prove the compositionality and correctness of the fault tolerant patterns. We illustrate our approach by modelling three classical fault tolerant patterns: homogeneous redundancy, heterogeneous redundancy and triple modular redundancy. Our model takes into account that the original system (without redundancy) computes a certain function with some delay and is amenable to random failures.

In order to prove that a fault tolerant pattern preserves the behaviour of its subsystems, we defined new notions of refinement. Systems engineers commonly accept the fact that fault tolerant patterns do not change the functionality of a system. However, this practise is not compatible with the classical refinement notions. Thus we defined axiomatic notions of refinement to prove that the formalised fault tolerant patterns preserve the behaviour of its subsystems.

We also proved that our fault tolerant patterns are compositional in the sense that we can apply fault tolerant patterns consecutively and for an arbitrary number of times. The result of that is still a system whose delay, failure model and functionality can be systematically discovered (by proof) with almost no effort.

In order to illustrate the usage of the patterns we applied the triple modular redundancy pattern to a simplified avionic Elevator Control System. We showed that once a fault tolerant pattern is verified, the application of it to a specific system and the proof of the behavioural preservation of the resulting system becomes trivial. This work has been done in collaboration with the Brazilian aircraft manufacturer Embraer.

Keywords:

Fault tolerance patterns, HOL4, behavioural preservation, refinement.Download [PDF].