Rely/Guarantee Refinement Calculus' blog

On my PhD, I worked on the mechanisation of a refinement calculus to supports derivation of programs specified using rely-guarantee. Yesterday, while preparing a manuscript to FACJ, I decided to start a blog about the theory that I worked on during the PhD. The blog can be accessed here.


The thesis:

My thesis is entitled Mechanising an Algebraic Rely-Guarantee Refinement Calculus. Refinement calculus can be thought as programming methodologies where design decisions are formally recorded. They generally consist on a collection of refactoring templates that can be applied by a programmer to transform mathematical specifications into executable code. The benefit of using this approach is that it guarantees that the implementation constructed by the programmer does exactly what the mathematical specification demands. This methodology results in software that is correct-by-construction, eliminating potential costs in post-production due to bugs. In my thesis this approach is illustrated via the derivation of non-trivial algorithms taken from the literature on refinement calculus.

Exemplos de especificacoes em Z

Em resposta a um visitante do blog, estou adicionando um exemplo de especificacoes em Z que usei durante minha experiencia com Z/Eves.

1. IBM CIC'S Browser Component


Este mecanização corresponde ao exemplo discutido no post

Technical Report No 257 by IBM (A specification, refinement and Verification Using Z Schema Calculus)

Abraco,
Diego Dias

Technical Report No 257 by IBM (A specification, refinement and Verification Using Z Schema Calculus)

The document made available on this post was recovered during the moving from Claremont Tower to the Urban Sciences Building while I was at Newcastle University. Leo Freitas, one of the co-authors of the paper "Mecanizando o componente de navegação do IBM’s CICS: um experimento do Grande Desafio" found a paper copy of this document and gave. It was part of my first foray into the mechanisation of formal theories using theorem provers, and since it is the basis for the paper mentioned above, and it is unrestricted, I decided to make it available!

A specification, refinement and Verification Using Z Schema Calculus

Enjoy it!

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].