Submitted by Pedro Henrique Rodrigues (pedro.henriquer@ufpe.br) on 2015-03-04T18:21:26Z
No. of bitstreams: 2
Dissertacao.pdf: 3554160 bytes, checksum: c0e2e7174583a750223705de5cd01844 (MD5)
license_rdf: 1232 bytes, checksum: 66e71c371cc565284e70f40736c94386 (MD5) / Made available in DSpace on 2015-03-04T18:21:26Z (GMT). No. of bitstreams: 2
Dissertacao.pdf: 3554160 bytes, checksum: c0e2e7174583a750223705de5cd01844 (MD5)
license_rdf: 1232 bytes, checksum: 66e71c371cc565284e70f40736c94386 (MD5)
Previous issue date: 2012-03-02 / FACEPE / 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.
| Identifer | oai:union.ndltd.org:IBICT/oai:repositorio.ufpe.br:123456789/10473 |
| Date | 02 March 2012 |
| Creators | DIAS, Diego Machado |
| Contributors | IYODA, Juliano Manabu, FARIAS, Adalberto Cajueiro de |
| Publisher | Universidade Federal de Pernambuco |
| Source Sets | IBICT Brazilian ETDs |
| Language | English |
| Detected Language | English |
| Type | info:eu-repo/semantics/publishedVersion, info:eu-repo/semantics/masterThesis |
| Source | reponame:Repositório Institucional da UFPE, instname:Universidade Federal de Pernambuco, instacron:UFPE |
| Rights | Attribution-NonCommercial-NoDerivs 3.0 Brazil, http://creativecommons.org/licenses/by-nc-nd/3.0/br/, info:eu-repo/semantics/openAccess |
Page generated in 0.0022 seconds