Gse.ufsc.br

Garantir o funcionamento correto de sistemas tolerantes a falhas n˜ envolve o dom´ınio de detalhados aspectos do sistema em quest˜ funcionamento, bem como dos tipos de falhas que podem ocorrer e dos adequados mecanismospara seu tratamento. O construtor do sistema deve ter uma clara compreens˜ oes normais ou anormais do sistema, bem como de recupera¸ sistema com comportamento bem definido na presen¸ Dada esta complexidade, e alinhado com dire¸ oes de pesquisa dos centros de contato, este identificar metodologias adequadas para o desenvolvimento de sistemas tolerantes a falhas comoformalizar abstra¸ oes e mecanismos de suporte para tal. Para a realiza¸ se parceiria com importantes centros mundais de pesquisa tanto na ´ (Centre for Software Reliability - Newcastle University), como na ´ Integrity Systems Engineering group - University of York).
e uma tarefa complexa. Mecanismos para tolerˆ ao pois eles aumentam a complexidade adi- ao do comportamento do sistema. O desenvolvedor tem que ancia a falhas A complexidade da constru¸ sistemas tolerantes a falhas aumenta no caso de sistemas concorrentes e com a considera¸ ambientes como os baseados em dispositivos m´ comuns. Em tais ambientes tanto o grau de dificuldade no tratamento quanto a freq¨ falhas pode aumentar significativamente, se comparados a ambientes mais controlados, como porexemplo redes locais de esta¸ e natural a busca por processos rigorosos de desenvolvimento. De fato, a literatura reporta numerosos trabalhos onde mecanismos espec´ıficos de tolerˆ especificados e analisados, frequentemente com m´ em uma linha mais recente de trabalhos nesta ´ ancia a falhas durante o projeto de diversas aplica¸ diversos tipos de sistemas e dom´ınios de aplica¸ ao, aos diversos tipos de falhas e ambientes computacionais e aos diversos tipos de mecanismos de tolerˆ cessidade de suportar o processo de desenvolvimento de software tolerante a falhas de formametodol´ oes adequadas e de forma rigorosa. Neste sentido, abordagens para o desenvolvimento rigoroso de sistemas tolerantes a falhas tˆ Complementarmente, em os autores relatam alguns fatores para a crescente aceita¸ cou um programa para acelerar o amadurec- financeiramente convincentes (Verification Grand Challenge). Este desafio n˜ plicitamente em software tolerante a falhas, mas ´ e esperado que tais sistemas sejam naturalmente Neste contexto, este plano de trabalho prop˜ alise de sistemas tolerantes a falhas. No cap´ıtulo o autor comenta sobre seus trabalhos relacionados ao tema do plano.
mencionados os grupos de trabalho no exterior para desenvolvimento do est´ e a metodologia de trabalho, detalhando atividades e cronograma. No cap´ıtulo s˜ os resultados esperados do plano proposto.
ultimos anos o proponente tem trabalhado com o desenvolvimento e utiliza¸ alise de sistemas distribu´ıdos. Em foi proposta uma forma ao de sistemas distribu´ıdos. Segundo a classifica¸ sistemas distribu´ıdos utilizando passagem de mensagem proposto em o formalismo GGBOproporciona: topologia de grafos dirigidos; permite modelar sistemas ass´ıncronos; sem modelo defalha definido; e com capacidade infinita de armazenamento de mensagens (buffering) tratadasde forma n˜ alise de modelos descritos em GGBO foram constru´ıdos. De permitindo utilizar o ambiente SPIN para prova de propriedades . Aabordagem permite verificar propriedades descritas em LTL (Linear Temporal Logic) tantosobre estados como sobre computa¸ ao de eventos em propriedades de tempo linear .
util como ferramenta interativa para o desenvolvedor, permitindo enten- der melhor o comportamento dos modelos constru´ıdos. Definimos em um mapeamentode modelos descritos em GGBO para Redes de Autˆ ao quantitativa de modelos. No que se refere ` trabalhamos com mapeamentos para linguagens de implementa¸ oes em C utilizando a interface MPI (Message Passing Inter- face), ou mesmo para Java utilizando uma plataforma de suporte ` como um cap´ıtulo do livro e uma descri¸ ao do ambiente de desenvolvimento pode ser Entre os modelos especificados utilizando GGBO e posteriormente analisados, pode-se citar: oveis um detector de falhas redes ativas um algoritmo de ao distribu´ıda , um algoritmo de exclus˜ , o problema dos leitores e escritores o protocolo two-phase commit e o sistema de controle de um posto de gasolina Em uma linha mais recente de trabalhos, a especifica¸ modelos GGBO de forma a representar o comportamento de falhas do tipo colapso e omiss˜ em sistemas distribu´ıdos. A representa¸ ao do comportamento falho serve para a analisar se o ao em duas fases (two-phase commit), analisando seu comportamento em oes de colapso de participantes e coordenador. Em , utilizando-se destes ao quantitativa dos modelos obtidos um estudo de caso foi realizado onde obtivemos parˆ ametros de desempenho e disponibilidade de um sistema os-doutoral pretendido contempla colabora¸ Newcastle University - Centre for Software Reliability (CSR). O conduz ativi- a com o Prof. Alexander RomaO Prof. Romanovsky conta com signi- ao cient´ıfica relacionada ao desenvolvimento de sistemas tolerantes a falhas, sendo membro ativo na comunidade com a elabora¸ arios projetos europeus de pesquisa, recentemente o Prof.
Romanovsky coordenou o projeto Rigorous Open Development Environment for ComplexSystems (RODIN) IST Project e atualmente coordena o projeto Industrialdeployment of system engineering methods providing high dependability and productivity(DEPLONeste mesmo centro, o projeto Trustworthy Ambient Systems (TrAmSco-ordenado pelo Prof. Cliff Jones e contando com a participa¸ no caso espec´ıfico voltado a ambientes m´ oveis. Conforme o Cap´ıtulo pode-se perceber o alinhamento dos objetivos deste plano com as atividades neste centro. O envolvimentoneste tema de pesquisa provˆ em do Prof. Romanovsky, com outros membros University of York - Department of Computer Science. Na Universidade de York o con- tato acontece com o High Integrity Systems Engineering Grouatrav´ asica e procura validar seus conceitos com a utiliza¸ de problemas reais encontrados em aplica¸ ustria como Rolls-Royce, BAE Systems, Jaguar e Land Rover. No caso espec´ıfico deste plano de trabalho, com mais detalhes no Cap´ıtulo est´ 1http://www.csr.ncl.ac.uk/2http://homepages.cs.ncl.ac.uk/alexander.romanovsky/home.formal/3http://rodin.cs.ncl.ac.uk/index.htm4http://deploy-project.eu/5http://www.cs.ncl.ac.uk/research/current%20projects?pid=2236http://www.cs.york.ac.uk/hise/7http://www-users.cs.york.ac.uk/ alcc/ e uma empresa internacional com sede na Inglaterra e l´ıder na ind´ ao com a Dra. Ana Cavalcanti, o envolvimento neste tema provˆ outros membros do grupo HISE e da empresa QinetiQ.
area de confiabilidade de sistemas a ado¸ desenvolvimento, sendo uma abordagem de preven¸ ao de falhas, e deste ponto de vista importante no desenvolvimento em geral de sistemas.
ancia a falhas significa evitar defeitos no servi¸ ancia a falhas se entende mais diretamente no tratamento de falhas f´ısicas, mas n˜ ambiente suposto para seu funcionamento, dos tipos de falhas que podem estar envolvidos, dosmecanismos de tolerˆ ancia que podem ser empregados e de como introduz´ı-los no sistema.
Desta forma, defende-se que o processo de constru¸ etodos formais, ferramentas e metodologias de constru¸ outra forma tais mecanismos podem, ao inv´ sistema. Ou seja, deve-se adotar medidas de preven¸ ao de falhas de desenvolvimento durante a ancia direta com o grupo CSR em Newcastle, ´ e identificar diretrizes para o introdu¸ ancia a falhas em modelos de sistemas.
ao de sistemas tolerantes a falhas, que poderia ser apoiada ao e arquiteturas de software. Tal abordagem tamb´ etodos formais nesta classe de sistemas.
alise dos modelos gerados, preferencialmente utilizando-se de verifica¸ A partir de um modelo de sistema que inclui mecanismos de tolerˆ e direta. Dependendo do tipo de falha (por exemplo para falhas ao do comportamento falho no modelo do sistema. Este do modelo com base em pressupostos falsos. Uma vez que isto ´ efetividade do mecanismo modelado na presen¸ ca da falha supostamente tolerada pelo mecanismo alise. Como mencionado no Cap´ıtulo esta dire¸ resultados, utilizando-se de model checking. Entretanto a an´ ancia a falhas adiciona uma nova dimens˜ conjunto de estados do modelo e, no pior caso, deve-se pressupor sua possibilidade de ocorrˆ em qualquer ponto do funcionamento do sistema, o que leva a uma multiplica¸ aveis. Na continuidade dos estudos, com este plano de trabalho, deve-se tamb´ O1 Especificar formalmente sistemas tolerantes a falhas e identificar diretrizes para guiar este a previsto o desenvolvimento de modelos de mecanismos existentes de tolerˆ a falhas. Um destes mecanismos, conforme contato pr´ omicas Coordenadas (Coordinated Atomic Actions - CA Actions) ao escolhidos para modelagem durante o est´ os-doutorado. Neste processo, as aplica¸ com a empresa QinetiQ - vide Cap´ıtulo ser˜ a interesse em uma abordagem estruturada para introdu¸ Durante a modelagem de tais mecanismos, colaborando com uma abordagem em exper-imenta¸ ao inicial no CSR em Newcastle, deveremos utilizar t´ a citados no Cap´ıtulo o formalismo Event-B ao de sistemas complexos tolerantes a fal- ao de fazer uso de passos de refinamentos, suportados em render trabalhos conjuntos com o grupo de York, que tem foco no desenvolvimento e uso de Circus. Circus ´ deste objetivo pretende-se realizar estudos comparados, baseados em casos, da utiliza¸ dos formalismos mencionados (Circus e Event-B) para esta classe de aplica¸ O2 Identificar tipos de falhas de interesse e propor abstra¸ ca de falhas pode acontecer a partir de modelos j´ ou de modelos gerados a partir do processo a ser identificado no objetivo O1. Em ambosos casos, deve-se identificar exatamente o tipo e escopo de falhas que supostamente s˜ um sistema. Como se pretende utilizar uma abordagem baseada em refinamentos para aconstru¸ ao de sistemas, estima-se que a representa¸ dar como um passo de refinamento do modelo, preparando-o para an´ ao do sistema, no entanto, deve-se partir de um modelo ao inclua o comportamento falho uma vez que este foi introduzido com o objetivo alise da efetividade dos mecanismos de tolerˆ oes de controle em estudo no grupo de York, segundo contato pr´ apesar de contarem com tratamento para algumas falhas f´ısicas em seu projeto, n˜ eias aqui propostas e serviriam para validar as estrat´ ao descritas utilizando Simulink existe um passo estabelecido de mapeamento para o formalismo Circus. A partir do modelo em Circuspode-se propor constru¸ oes para representar o comportamento das falhas f´ısicas pressupostas em de um verificador de modelos em constru¸ a estar dispon´ıvel, ferramentas dispon´ıveis de an´ O3 Identificar propriedades comuns a serem provadas sobre mecanismos de tolerˆ egias adequadas para prova de tais propriedades.
teve resultados positivos. Entretanto somente a modelos restritos foram analisados devidoao problema da explos˜ co de estados. Assim, tem-se como objetivo avaliar quais ao a serem empregadas, dependendo do tipo de propriedade e do processo de modelagem a ser experimentado, conforme relatado no obje-tivo O1.
Tanto propriedades sobre os dados do sistema, assim como as de controle, s˜ ao frequentemente concorrentes e os mecanismos de ancia a falhas podem envolver sofisticadas formas de sincroniza¸ oes dos processos, tanto de forma isolada como Durante o per´ıodo que antecede o est´ os-doutoral, o autor pretende estudar os m´ ao a serem empregados e respectivas ferramentas de especifica¸ em adiantar, em conjunto com os grupos de trabalho, a decis˜ os estudos de caso a serem realizados. Durante o per´ıodo do est´ e cronograma abaixo listados devem ser seguidos.
e-se deslocamentos semanais entre York e Newcastle para contato com os membros dos ao cr´ıtica de interesse, caracterizar os tipos de falhas toleradas e as propriedades que devem ser verificadas, referentes tanto o funcionamento normal quanto napresen¸ 4. Dependendo do andamento, repetir as atividades 1, 2, e 3 para outra aplica¸ 9York e Newcastle ficam a aproximadamente 1h10min de trem. O local de residˆencia pretendido ´e York pois a esposa do autor, Dra. Leila Ribeiro, est´ em contato com o Prof. Jim Woodcock, naquela cidade.
encia nas atividades anteriores, generalizar abstra¸ ficados, dando origem a uma metodologia para an´ alise de sistemas tolerantes a falhas.
ancia a falhas e especificar formalmente o mesmo uti- ecnicas de refinamento. Definir formalmente e provar as propriedades do mecan- ismo.
O mecanismo a ser modelado deve ser definido em contato com os grupos de York e New-castle, agregando preferencialmente um parceiro interessado na utiliza¸ ao cr´ıtica. Dependendo do andamento dos trabalhos em grupo, este formalismo 7. Modelar o mecanismo de Coordinated Atomic Actions utilizando t´ Definir formalmente e provar as propriedades do mecanismo.
encia nas atividades 6 e 7, criar uma metodologia para modelagem de sistemas tolerantes a falhas, envolvendo: em modelos constru´ıdos por refinamentos; egias para prova de propriedades em sistemas constru´ıdos por refina- ao, baseada em casos, dos formalismos utilizados - Event-B e Circus.
ao de sistemas tolerantes a falhas utilizando refinamentos; ancia a falhas, incluindo Coordinated Atomic • estudos de caso da metodologia de an´ em conjunto com o grupo de Newcastle, podendo ser aplica¸ oes, dependendo do andamento do projeto DEPLOY.
A partir dos resultados obtidos, pretende-se a submiss˜ ao, o conhecimento detalhado do ambiente suposto para seu funcionamento, dos tipos de falhas que podem estar envolvidos, dos mecanismos de tolerˆ que podem ser empregados e de como introduz´ı-los no sistema. Por outro lado, enfatiza-se aimportˆ cr´ıticos, pois de outra forma tais mecanismos podem, ao inv´ a qualidade do sistema. Assim, a pesquisa em desenvolvimento rigoroso de sistemas tolerantesa falhas ´ ao cient´ıfica importante. Tal como proposto neste projeto, deve-se suportar o processo de desenvolvimento de software tolerante a falhas de forma metodol´ Como se pode perceber pelas atividades pautadas, prevˆ ao acontece principalmente com os centros acadˆ area do projeto, com os quais o contato est´ e l´ıder em pesquisa no que tange a constru¸ ao a pesquisadores de outras Universidades proporcionado pela acolhida tanto em Newcastle como em York ´ grupo do Prof. Dr. Reiko Heckel, na Universidade de Leicester, que trabalha no desenvolvimentoe aplica¸ aticas de Grafos Baseadas em Objetos Estoc´ ao e melhoria de abordagens bem como desenvolvimento conjunto Jean-Raymond Abrial and Stefan Hallerstede, Refinement, decomposition, and in-stantiation of discrete models: Application to event-b, Fundam. Inform. 77 (2007),no. 1-2, 1–28.
etayer, Rodin deliverable 3.2 - event-b language, Tech.
report, Newcastle University, England, 2005.
[BCD+06] P. Baldan, A. Corradini, F. Dotti, L. Foss, F. Gadducci, and L. Ribeiro, Towards a notion of transaction in graph rewriting, GT-VMT - 5th International Workshop onGraph Transformation and Visual Modeling Techniques, 2006, pp. 1–12.
Michael Butler, Cliff B. Jones, Alexander Romanovsky, and Elena Troubitsyna (eds.),Rigorous development of complex fault-tolerant systems [fp6 ist-511599 rodin project],Lecture Notes in Computer Science, vol. 4157, Springer, 2006.
Philippa J. Broadfoot and A. W. Roscoe, Tutorial on fdr and its applications, SPIN(Klaus Havelund, John Penix, and Willem Visser, eds.), Lecture Notes in ComputerScience, vol. 1885, Springer, 2000, p. 322.
A. Corradini, F. Dotti, L. Foss, and L. Ribeiro, Translating Java code to graph trans-formation systems, ICGT - International Conference on Graph Transformation, LNCS,vol. 3256, Springer, 2004, pp. 383–398.
A L C Cavalcanti, A C A Sampaio, and J C P Woodcock, A Refinement Strategy forCircus, Formal Aspects of Computing 15 (2003), no. 2-3, 146–181.
L. Duarte and F.L. Dotti, Development of an active network architecture using mobileagents - a case study, Tech. Report TR-043, PPGCC-FACIN-PUCRS, Brazil, 2004.
[DDCR02] F. L. Dotti, L. M. Duarte, B. Copstein, and L. Ribeiro, Simulation of mobile ap- plications, 2002 Communication Networks and Distributed Systems Modeling andSimulation Conference (USA), SCS, 2002, pp. 261–267.
[DDF+04] F. L. Dotti, L. Duarte, L. Foss, L. Ribeiro, D. Russi, and O. Santos, An environment for the development of concurrent object-based applications, ENTCS (InternationalWorkshop on Graph-Based Tools) (2004).
[DFRS03a] F. L. Dotti, L. Foss, L. Ribeiro, and O. M. Santos, Verification of object-based dis- tributed systems, 6th Int. Conference on Formal Methods for Open Object-BasedDistributed Systems (France), LNCS, vol. 2884, Springer-Verlag, 2003, pp. 261–275.
[DFRS03b] F.L. Dotti, L. Foss, L. Ribeiro, and O.M. Santos, Specification and formal verifica- tion of distributed systems (in portuguese), 17th Brazilian Symposium on SoftwareEngineering (SBES), 2003, pp. 225–240.
James B. Dabney and Thomas L. Harman, Mastering simulink, Prentice Hall PTR,Upper Saddle River, NJ, USA, 1997.
onig, O. M. Santos, and L. Ribeiro, A case study: Verifying a mutual exclusion protocol with process creation using graph transformation systems, Tech.
Report 08/2004, Universit¨ erio de Lemos, Cristina Gacek, and Alexander B. Romanovsky (eds.), Architecting dependable systems iv [the book is a result of the icse 2006 and dsn 2006 workshops],Lecture Notes in Computer Science, vol. 4615, Springer, 2007.
[DMdS05] Fernando Lu´ıs Dotti, Odorico Machado Mendizabal, and Osmar Marchi dos San- tos, Verifying fault-tolerant distributed systems using object-based graph grammars, ao Gabriel Silva, Aline Maria Santos Andrade, and avio Morais de Assis Silva, eds.), Lecture Notes in Computer Science, vol. 3747, F.L. Dotti, F. Pasini, and O.M. Santos, A methodology for the verification of partialsystems modelled with object based graph grammars, 18th Brazilian Symposium onSoftware Engineering (SBES), 2004, pp. 86–101.
F. L. Dotti and L. Ribeiro, Specification of mobile code systems using graph grammars,4th Int. Conference on Formal Methods for Open Object-Based Distributed Systems(USA), IFIP Conference Proceedings, vol. 177, Kluwer Academic Publishers, 2000,pp. 45–64.
F. L. Dotti, L. Ribeiro, and O. M. Santos, Specification and analysis of fault behav-iours using graph grammars, 2nd International Workshop on Applications of GraphTransformations with Industrial Relevance (USA), LNCS, vol. 3062, Springer-Verlag,2003, pp. 120–133.
odel, On the use of formal specifications to analyze fault behaviors of distributed systems, 1st Latin-American Symposium onDependable Computing (Brazil), LNCS, vol. 2847, Springer-Verlag, 2003, pp. 341–360.
L. M. Duarte, Development of distributed systems with mobile code through formalspecification (in portuguese), Master’s thesis, PUCRS - Faculdade de Inform´ H. Ehrig, Introduction to the algebraic theory of graph grammars, Lecture Notes inComputer Science 73 (1979), 1–69.
P. Fernandes, B. Plateau, and W.J. Stewart, Numerical Issues for Stochastic AutomataNetworks, 4th Workshop on Process Algebras and Performance Modelling (Torino,Italy), Ed. M. Ribaudo, 1996, pp. 215–234.
L. Freitas, Model checking circus, Ph.D. thesis, University of York, 2005.
Barbara Gallina, Nicolas Guelfi, and Alexander B. Romanovsky (eds.), Coordinatedatomic actions for dependable distributed systems: the current state in concepts,semantics and verification means, IEEE, 2007.
C. A. R. Hoare, Communicating sequential processes, Prentice Hall, 1985.
G. J. Holzmann, The model checker SPIN, IEEE Trans. on Soft. Eng. 23 (1997),no. 5, 279–295.
Cliff Jones, Peter O’Hearn, and Jim Woodcock, Verified software: A grand challenge,Computer 39 (2006), no. 4, 93–95.
L. Lamport and N. Lynch, Distributed computing: models and methods, Handbookof theoretical computer science, vol. B: formal models and semantics, Elsevier, 1990.
Jean-Claude Laprie and Brian Randell, Basic concepts and taxonomy of dependableand secure computing, IEEE Trans. Dependable Secur. Comput. 1 (2004), no. 1,11–33, Fellow-Algirdas Avizienis and Senior Member-Carl Landwehr.
Odorico Machado Mendizabal and Fernando Lu´ıs Dotti, Non-functional analysis ofdistributed systems in unreliable environments using stochastic object based graphgrammars, ICGT (Andrea Corradini, Hartmut Ehrig, Ugo Montanari, Leila Ribeiro, andGrzegorz Rozenberg, eds.), Lecture Notes in Computer Science, vol. 4178, Springer,2006, pp. 275–290.
Odorico Machado Mendizabal, Fernando Lu´ıs Dotti, and Leila Ribeiro, Stochasticobject-based graph grammars, Electr. Notes Theor. Comput. Sci. 184 (2007), 151–170.
Z. Manna and A. Pnueli, The temporal logic of reactive and concurrent systems:specification, Springer, 1991.
Henry Muccini, Patrizio Pelliccione, and Alexander Romanovsky, Architecting faulttolerant systems, WICSA, IEEE Computer Society, 2007, p. 43.
B. Plateau and K. Atif, Stochastic Automata Networks for modelling parallel systems,IEEE Transactions on Software Engineering 17 (1991), no. 10, 1093–1108.
aun and M. Chechik, Events in linear-time properties, 4th Int. Conference on Requirements Engineering (Ireland), IEEE Computer Society Press, 1999, pp. 123–132.
abio Pasini and Fernando Lu´ıs Dotti, Code generation for parallel applications mod- elled with object-based graph grammars, Electr. Notes Theor. Comput. Sci. 184(2007), 113–131.
L. Ribeiro, F. L. Dotti, and R. Bardohl, A formal framework for the development ofconcurrent object-based systems, Lecture Notes in Computer Science 3393 (2005),385–401.
L. Ribeiro, F. Dotti, O. Santos, and F. Pasini, Verifying object-based graph grammars:An assume-guarantee approach, Software and Systems Modeling 5 (2006), 289–312.
Alexander Romanovsky, A looming fault tolerance software crisis?, SIGSOFT Softw.
Eng. Notes 32 (2007), no. 2, 1–4.
G. Rozemberg, Handbook of graph grammars and computing by graph transformation1: foundations, World Scientific Publisher, 1997.
M. Saaltink, The Z/EVES system, UM ’97: Proceedings of the 10th InternationalConference of Z Users on The Z Formal Specification Notation, Lecture Notes inComputer Science, vol. vol 1212, Springer, 1997, pp. 72–85.
O. M Santos, F. L. Dotti, and L. Ribeiro, Verifying object-based graph grammars,Eletronic Notes in Theoretical Computer Science 109 (2004), 125–136.
J. Spivey, The z notation: A reference manual, 2nd. edition ed., Prentice Hall, 1992.
http://www.jucs.org/jucs 13 5/the verification grand challenge.
J. Woodcock and A. Cavalcanti, The semantics of circus, ZB, 2002, pp. 184–203.

Source: http://gse.ufsc.br/~bezerra/students/LeonardoAmaral/Papers_Dr/projPosDoc2008-dotti.pdf