[pt] A confiabilidade absoluta do software é considerada inatingível, pois mesmo quando confeccionado seguindo regras rígidas de qualidade, o software não está livre da ocorrência de falhas durante a sua vida útil. O nível de confiabilidade do software está relacionado, entre outros, à quantidade de defeitos remanescentes que serão exercitados durante seu uso. Contendo menos defeitos remanescentes, espera-se que o software falhe menos frequentemente, embora muitos desses defeitos sejam exercitados nenhuma vez durante a vida útil do software. Mas desenvolvedores, além de redigir programas, utilizam cada vez mais bibliotecas e serviços remotos que muitas vezes possuem qualidade duvidosa. Na tentativa de tornar o software capaz de observar erros em tempo de execução, surge a hipótese que o uso dos Métodos Formais Leves, por meio do emprego sistemático de assertivas executáveis, pode ser eficaz e economicamente viável para assegurar a confiabilidade do software, tanto em tempo de teste como em tempo de uso. O objetivo principal desta pesquisa é avaliar a eficácia de assertivas executáveis para prevenção e observação de falhas em tempo de execução. As avaliações da eficácia foram feitas por intermédio de uma análise quantitativa utilizando experimentos. Estes, utilizam, implementações de estruturas de dados instrumentadas com assertivas executáveis, submetidas a testes baseados em mutações. Os resultados mostraram que todos os mutantes não equivalentes foram identificados pelas assertivas, embora os testes não foram capazes disso. Também é apresentada uma estimativa do custo computacional relativo ao uso de assertivas executáveis. Com base na infraestrutura criada para realização dos experimentos é proposta uma política de instrumentação de programas utilizando assertivas executáveis a serem mantidas ativas tanto durante os testes como durante o uso produtivo. / [en] Absolute reliability of software is considered unattainable, because even when it is build following strict quality rules, software is not free of failure occurrences during its lifetime. Software s reliability level is related, among others, to the amount of remaining defects that will be exercised during its use. If software contains less remaining defects, it is expected that failures will occur less often, although many of these defects will never be exercised during its useful life. However, libraries and remote services of dubious quality are frequently used. In an attempt to enable software to check mistakes at runtime, hypothetically Lightweight Formal Methods, by means of executable assertions, can be effective and economically viable to ensure software s reliability both at test time as well as at run-time. The main objective of this research is to evaluate the effectiveness of executable assertions for the prevention and observation of run-time failures. Effectiveness was evaluated by means of experiments. We instrumented data structures with executable assertions, and subjected them to tests based on mutations. The results have shown that all non-equivalent mutants were detected by assertions, although several of them were not detected by tests using non-instrumented versions of the programs. Furthermore, estimates of the computational cost for the use of executable assertions are presented. Based on the infrastructure created for the experiments we propose an instrumentation policy using executable assertions to be used for testing and to safeguard run-time.

[pt] O trabalho entrelaça historiografia, espaços não formais, cultura e ensino de história. A pesquisa busca compreender as práticas educativas desenvolvidas no roteiro guiado da Pousada Fazenda Ponte Alta (PFPA) e suas relações com o ensino de história nas escolas cariocas. Está estruturado em três capítulos, além da introdução e considerações finas. Após a introdução, o capítulo II aborda as diversas reescritas historiográficas desenvolvidas pela Escola dos Annales e pela Nova História Cultural, assim como aprofunda no sentido e relevância da chamada educação não formal. Termina com reflexões direcionadas as propostas didáticas observadas hoje no ensino de história. O terceiro capítulo realiza uma descrição da PFPA: história, arquitetura, características centrais, os atuais serviços e, principalmente, analisa as atividades e dinâmicas educativas realizadas no local. O quarto e último capítulo está centrado na análise dos dados construídos através da pesquisa, cujas estratégias metodológicas foram revisão bibliográfica, análise documental, observações e entrevistas. Nas considerações finais destaca-se que o espaço tem consolidado seu roteiro histórico como importante ferramenta e prática educativa. Acreditamos que a PFPA possibilita avanços no ensino de história ao promover a ampliação das fontes de pesquisa, de experiências e dinâmicas pedagógicas e, assim, contribui para o enriquecimento do ensino de história nas escolas do Rio de Janeiro, particularmente no Ensino Fundamental. / [en] The work weaves together non-formal spaces, historiography, culture and history teaching. The research tries to understand the educational practices developed in the screenplay of Pousada Fazenda Ponte Alta guided (PFPA) and their relationships with the teaching of history in schools in Rio. It is structured in three chapters, besides the introduction and considerations. After the introduction, chapter II discusses the various historiographical rewritten developed by the Annales school and New Cultural history, as well as deepens in meaning and relevance of the so-called non-formal education. It ends with reflections directed to didactic proposals observed today in history teaching. The third chapter is a description of the PFPA: its history, architecture, key features, the current services offered and, above all, educational activities and dynamic analyses carried out on site. The fourth and final chapter is focused on the analysis of data built through research, whose methodological strategies were bibliographical revision, document analysis, observation and interviews. In the final considerations it stands out that the space has consolidated its historic route as an important tool and educational practice. We believe that the PFPA provides updates in teaching history to promote the expansion of research sources, experiences and pedagogical dynamics and thus contributes to the enrichment of history teaching in schools of Rio de Janeiro, particularly in elementary school.

A Análise de Conceitos Formais (FCA) é uma teoria matemática que formaliza a noção de conceitos e hierarquias conceituais. De importância central a esta teoria é uma estrutura algébrica denominada reticulado de conceitos. Esta estrutura é definida em função de um conjunto de objetos, outro de atributos e uma relação que indica os atributos apresentados por cada objeto. Uma representação gráfica de um reticulado de conceitos, por meio de uma interface computacional, é capaz de expor regularidades presentes em dados a um usuário, e este pode então realizar tarefas de análise exploratória de dados. Este tipo de aplicação de FCA vem sendo empregado em dezenas de projetos pertencentes a áreas diversas, como medicina, serviços de inteligência, engenharia de software e bioinformática. Mostramos neste trabalho um sistema de análise exploratória de dados baseado em FCA, e sua utilização sobre dados reais. Também é mostrado como reticulados de conceitos podem ser empregados em interfaces de recuperação de informação. Do ponto de vista algorítmico, analisamos métodos computacionais para a determinação do reticulado de conceitos, e também de uma subestrutura simplificada, o conjunto de conceitos. O tamanho de um reticulado de conceitos pode ser exponencial em função dos tamanhos dos conjuntos de objetos e de atributos. Assim, é de vital interesse o estabelecimento de cotas superiores para o número de conceitos de um reticulado. Neste trabalho, apresentamos as cotas já conhecidas presentes na literatura. Também estabelecemos uma nova cota superior, e mostramos famílias de casos em que nossa cota superior é mais justa que as demais. Para algumas famílias particulares, nossa cota é polinomial, enquanto que as demais são exponenciais. / Formal Concept Analysis (FCA) is a mathematical theory that formalizes the notion of concepts and conceptual hierarchies. Of central importance to this theory is an algebraic structure termed concept lattice. Such structure becomes defined after being given one set of objects, one of attributes, and an incidence relation describing the attributes held by each object. A graphical representation of a concept lattice, by means of a computational interface, is capable of unfolding regularities present in data to an user, who is then able to conduct exploratory data analysis tasks. This sort of FCA application is currently deployed in tens of projects belonging to a wide range of areas, such as medicine, intelligence services, software engineering and bioinformatics. We show in this work an FCA-based system of exploratory data analysis, and its use over real data. Moreover, it is shown how concept lattices can be employed in information retrieval interfaces. From the algorithmic viewpoint, we analyse computational methods for the determination of a concept lattice, and also of a simplified substructure, the concept set. The size of a concept lattice can be exponential when compared to the size of the objects and the attributes sets. Therefore, it is of paramount interest the establishment of upper bounds for the number of concepts of a lattice. In this work, we present the upper bounds already known in the literature. We also establish a new upper bound, and show families of cases in which our bound is sharper than the others. For particular families, our bound is polynomial, whereas the other bounds are exponential.

Neste trabalho apresentamos um modelo para ambientes inteligentes baseado em organizações de agentes, onde interações entre entidades são associadas a espaços físicos, pessoas carregam dispositivos e se movimentam entre diferentes espaços físicos e cada espaço físico contém definições de interações (comportamentos definidos por normas) próprias do seu contexto. São definidos três componentes deste modelo: (1) modelo conceitual, (2) linguagem de especificação e (3) ambiente de execução. A separação do modelo nestes três componentes traz como principais conseqüências: (1) a ativação de um ambiente inteligente é feita através de um mecanismo de alto nível, (2) a especificação de um ambiente inteligente é independente do domínio de aplicação e (3) as especificações podem ser executadas em mecanismos diferentes de execução. / We introduce a conceptual model for smart environments based on agent organizations where interactions between entities are associated with physical spaces, people (carrying mobile devices) move between different physical spaces and these physical spaces contain definitions of interactions (behaviors defined by norms) related to each context. This model defines three components: (1) conceptual model, (2) language specification, and (3) execution environment. The separation in these three components brings as main consequences: (1) activation of a smart environment is performed through a high-level mechanism, (2) specification of a smart environment is independent of the application domain, and (3) specifications can be performed on different mechanisms of execution.

As técnicas de teste podem ser divididas, num primeiro nível, naquelas baseadas no código (caixa branca) e naquelas baseadas na especificação (caixa preta ou funcionais). Nenhuma delas é completa pois visam a identificar tipos diferentes de defeitos e a sua utilização em conjunto pode elevar o nível de confiabilidade das aplicações. Assim, tornam-se importantes estudos que contribuam para um melhor entendimento da relação existente entre técnicas funcionais e estruturais, como elas se complementam e como podem ser utilizadas em conjunto. Este trabalho está inserido no contexto do projeto PLAVIS (Plataforma para Validação e Integração de Software em Aplicações Espaciais), e tem como objetivo realizar um estudo comparativo entre as técnicas de geração de casos de teste funcionais (baseadas nas especificações formais) e os critérios estruturais baseados em fluxo de controle e fluxo de dados, aplicados nas implementações. Num contexto específico, esse estudo deve fornecer dados de como se relacionam essas duas técnicas (funcional e estrutural) gerando subsídios para sua utilização em conjunto. Num contexto mais amplo - o do projeto PLAVIS - visa a estabelecer uma estratégia de teste baseada em critérios funcionais e estruturais e que possam, juntamente com as ferramentas que dão suporte a eles, compor um ambiente de teste disponível à utilização em aplicações espaciais dentro do INPE / Testing techniques can be divided, in high level, in code-based ones (white box) and specification based ones (black box). None of them are complete as they intend to identify different kinds of faults. The use of them together can increase the application confidence level. Thus, it is important to investigate the relationship between structural testing techniques and functional testing techniques, how they complete themselves and how they can be used together. This paper was developed in the context of the Plavis (PLAtform of software Validation & Integration on Space systems) project. This project provides comparative studies between functional generation testing techniques (based on formal specifications) and structural generation testing techniques, such as control-flow and data-flow criteria, applied in the implementation. In a specific context, this study provides data about the relationship between these techniques and how they can be used together. In the context of the Plavis project, the goal is to provide a testing strategy, based on functional and structural criteria, and a set of tools, composing a testing environment to be used in Space Applications projects, at INPE

Submitted by Maria Cristina (library@lncc.br) on 2015-11-25T17:21:07Z No. of bitstreams: 1 Tese-Gastao-LNCC.pdf: 33936271 bytes, checksum: 63b98a5aa6d7c3c834844f4b4af76687 (MD5) / Approved for entry into archive by Maria Cristina (library@lncc.br) on 2015-11-25T17:21:19Z (GMT) No. of bitstreams: 1 Tese-Gastao-LNCC.pdf: 33936271 bytes, checksum: 63b98a5aa6d7c3c834844f4b4af76687 (MD5) / Made available in DSpace on 2015-11-25T17:21:30Z (GMT). No. of bitstreams: 1 Tese-Gastao-LNCC.pdf: 33936271 bytes, checksum: 63b98a5aa6d7c3c834844f4b4af76687 (MD5) Previous issue date: 2015-07-02 / Coordenação de Aperfeiçoamento de Pessoal de Nível Superior (Capes) / Manifold learning techniques have been used for dimensionality reduction in applications involving pattern recognition, data mining and computer vision. This thesis describes recent works that we have done in this area as well as perspectives for future works. First, we propose a methodology called Local Riemannian Manifold Learning (LRML), which recovers the topology and geometry of the manifold using local systems of normal coordinates computed through the exponential application. The LRML strategy has the advantage of reducing the accumulation of errors during the process of manifold learning. However, the obtained parameterization can not be used as an unambiguous representation space. Furthermore, the synthesis process needs domain triangulation in the parameter space to be efficiently performed. We address this drawback of LRML using a composition procedure to structure the neighborhoods of normal coordinates building a global representation space that locally preserves radial geodesic distances. Besides, we add a geometric structure based on triangulations obtaining an efficient methodology to the synthesis process. We also explored discrete geometry concepts for generation of piecewise linear manifolds for data analysis. In the computational experiments we verify the efficiency of the LRML combined with the composition process and discrete geometry framework for the synthesis and data mining. We explored the application of foliation theory for images of human faces with multiple facial expressions. We conclude that this approach is a promising one for the study of the geometry and topology of the space of human face images. / Técnicas em aprendizado de variedades vêm sendo utilizadas para redução de dimensionalidade em aplicações envolvendo reconhecimento de padrões, mineração de dados e visão computacional. Nesta tese serão descritos trabalhos recentes que fizemos nesta área bem como perspectivas para trabalhos futuros. Primeiramente, propomos uma metodologia denominada aprendizado local de variedades Riemannianas (LRML), a qual recupera a topologia e geometria da variedade utilizando sistemas locais de coordenadas normais computadas via aplicação exponencial. A estratégia local do LRML tem a vantagem de minimizar a acumulação de erros durante o processo de reconstrução da variedade. No entanto, a parametrização obtida não pode ser utilizada como um espaço de representação sem ambiguidades. Além disso, o processo de síntese precisa de triangulação do domínio no espaço de parâmetros para ser realizada de forma eficiente. Abordamos este inconveniente do LRML usando um procedimento de composição para estruturar as vizinhanças de coordenadas normais construindo um espaço de representação que preserva localmente distâncias geodésicas radiais. Adicionamos ainda uma estrutura geométrica baseada na triangulação obtendo uma metodologia eficiente para o processo de síntese. Exploramos também a geração de variedades lineares por partes para análise de dados. Nos experimentos computacionais verificamos a eficiência do LRML combinado com as estruturas de composição e triangulação para a síntese e exploração de dados. Exploramos a aplicação da teoria de folheação para imagens de faces humanas com múltiplas expressões faciais, tal abordagem se mostrou promissora para o estudo do espaço de imagens de faces com diversas expressões faciais distintas.

O envelhecimento populacional tem como uma de suas implicações o aumento do número de indivíduos com incapacidade funcional, o que gera uma demanda por de cuidados de longa duração, exercidos principalmente pelas famílias. Essas, por suas transformações contemporâneas tendem a ter reduzida a sua capacidade de atender a essa demanda. Assim, a presença do cuidador formal domiciliar de pessoa idosa como elemento fundamental, nesse contexto, deixa de ser um problema do âmbito privado e configura-se em uma questão de saúde pública. O presente estudo investigou a trajetória ocupacional de cuidadoras formais domiciliares de pessoas idosas, com o objetivo de compreender seus principais eventos e características, a percepção que elas têm do seu trabalho, de seu processo de capacitação e do cuidado. Nesta pesquisa qualitativa, os dados foram examinados com utilização da técnica da Análise do Discurso, a partir da construção de uma linha cronológica das trajetórias, com seus principais eventos e categorização das frases significativas, destacadas dos relatos. As categorias empíricas de análise foram: trabalho, gênero, qualificação e cuidado. Verificou-se que as mulheres chegam ao trabalho de cuidadora formal domiciliar de pessoa idosa pelo trabalho doméstico, pela qualificação formal ou pela experiência de cuidar de seus familiares idosos. As trajetórias são caracterizadas pela precarização do trabalho, especialmente daqueles desenvolvidos no ambiente domiciliar, pela inserção e reinserção das mulheres no mercado de trabalho via ambiente doméstico, pela desvalorização do trabalho feminino, pela dificuldade em conciliar os cuidados aos filhos e familiares idosos com o trabalho remunerado, pela escolarização e profissionalização (quando há) tardias, pela experiência prática como sendo a principal ferramenta qualificadora, e pelo cuidado como disposição ética promotora de sentido para a atividade laboral. Conclui-se que, a promoção de relações de gênero mais igualitárias, a educação formal específica, a regulamentação da profissão e a adoção de um novo modelo de trabalho e emprego na área de cuidados à pessoa idosa, podem melhorar a qualidade desse trabalho, assim como promover o bem estar dos idosos dependentes e de suas famílias / One of the consequences of population aging is the growth of individuals with functional disability which creates a demand for long term care, primarily exercised by the families. Due to contemporary transformations, families tend to reduce their ability to meet this demand. Therefore, the presence formal home caregiver of elderly as a key element in this context is no longer a private issue to become a matter of public health. The present study investigated the occupational trajectory of formal female home caregivers of elderly, aiming to understand their key events and their main characteristics, as well as the perception they have of their own job, their process of training and about care itself. This qualitative research has examined the data using the Discourse Analysis technique, starting from the construction of a timeline of each trajectory, which embraced its main events and the categorization of all significant sentences, highlighted from their stories. The empirical categories of analysis were: work, gender, qualification and care. It was found that women start up as formal home caregivers of elderly through domestic housework, formal qualification or the experience of caring for their own elderly relatives. The trajectories are characterized by poor job relations, especially the ones developed in the home environment, by the integration and reintegration of women into the labor market through domestic environment, the devaluation of women\'s work, by the difficulty in reconciling the care of their children and elderly relatives with their professional paid activities, for late education and professional training (when existed), by practical experience as the main qualifying tool, and the care as an ethical promoter of sense for labor activities. This study concludes that promoting more equitable gender relation, specific formal education, legal regulation of the profession and the adoption of a new model of work and employment for the formal caregivers of elderly field, tend to improve the quality of this work, as well as promote the well-being of the dependent elderly and their families.

A adoção em larga escala de redes de computadores e gerenciadores de banco de dados contribuiu para o surgimento de sistemas de informação complexos. Atualmente, estes sistemas tornaram-se elementos essenciais na vida das pessoas, dando suporte a processos de negócio e serviços corporativos indispensáveis à sociedade, como automação bancária e telefonia. A utilização de componentes na estruturação destes sistemas promove maior qualidade e flexibilidade ao produto e agiliza o processo de desenvolvimento. Entretanto, para que estes benefícios sejam totalmente observados, é fundamental que os provedores de componentes de prateleira projetem especificações precisas, completas e consistentes. Geralmente, as especificações omitem ou negligenciam o comportamento dos componentes nas situações de falha. Desta forma, a utilização de componentes não confiáveis, cujos comportamentos não podem ser inteiramente previstos, compromete seriamente o projeto de sistemas tolerantes a falhas. Uma estratégia para a especificação de componentes tolerantes a falhas é informar a ocorrência de erros através de exceções e realizar a recuperação dos mesmos por rotinas de tratamento correspondentes. A especificação deve separar claramente o comportamento normal do excepcional, destinado à recuperação do erro. Entretanto, em sistemas concorrentes e distribuídos, a especificação apenas deste tratamento local não é suficiente. Uma exceção pode ser lançada em decorrência de erros sistêmicos (i.e. problemas de rede) que afetam todo o sistema. Assim, determinadas exceções devem ser tratadas em nível arquitetural, envolvendo os demais componentes no tratamento. O modelo conceitual de ações Atômicas Coordenadas (ações CA - Coordinated Atomic actions), bastante aplicado na estruturação de sistemas tolerantes a falhas, define um mecanismo geral para a coordenação do tratamento excepcional dos componentes, que cooperam na execução das atividades e competem por recursos compartilhados. Portanto, o modelo de ações CA oferece uma solução potencialmente viável para a especificação do tratamento de exceções em nível arquitetural. Este trabalho propõe um framework para a especificação do tratamento de exceções em nível arquitetural, baseando-se no modelo de aninhamento de ações CA e utilizando a linguagem orientada a eventos CSP (Communicating Sequential Processes). Sua principal característica é prover um protocolo padronizado para a coordenação do tratamento de exceções, que envolve a cooperação dos componentes do sistema. Além disso, é apresentada uma estratégia para a verificação formal dos sistemas na ferramenta FDR (Failure Divergence Refinement), com base no modelo de refinamento por rastros. / The widespread scale adoption of computer networks and database management systems has contributed to the arising of complex information systems. Nowadays, these systems have become essential aspects in the everyday life, supporting business processes and indispensable enterprise services to society such as banking automation and telephony. The usage of components in structuring of these systems promotes higher quality and flexibility to the product and accelerates the software development process. However, in order to fully observe the benefits it is essential that the suppliers of these COTS (commercial off-the-shelf) design precise, complete and consistent specifications. Generally, the specifications omit or neglect the behavior of these components in exceptional situations. Therefore, the usage of untrustworthy components whose behavior cannot be entirely foreseen seriously compromise the design of fault-tolerant systems. One of the strategies used for the specification of fault-tolerant components is to inform the occurrence of errors through exceptions and make its recovering by the correspondent exception handling routines. The specification should separate clearly the normal behavior from the exceptional one, specially designed for error recovery. However, in concurrent and distributed systems, specification of local exception handling is not enough. An exception could be raised as a result of systemic errors (i.e. network errors) which affect the entire system, thus specific types of exceptions should be treated at an architectural level involving all the other components in this handling activity. The conceptual model of Coordinated Atomic (CA) actions, often applied in the structuring of fault-tolerant systems, defines a general mechanism for coordination of exception handling with components that cooperate while executing activities and compete for shared resources. Therefore, the model of CA actions offers a perfectly viable solution for the specification of exception handling at an architectural level. This work proposes a framework for the specification of exception handling at an architectural level, based on the nesting model of CA actions and using the event-oriented language CSP (Communicating Sequential Processes). Its main characteristic is to provide a standardized protocol for coordination of exception handling that involves the cooperation of system components. Moreover, it is presented a formal strategy for system verification using the FDR (Failure Divergence Refinement) tool, based on the traces refinement model.

Gramática de grafos é uma linguagem formal bastante adequada para sistemas cujos estados possuem uma topologia complexa (que envolvem vários tipos de elementos e diferentes tipos de relações entre eles) e cujo comportamento é essencialmente orientado pelos dados, isto é, eventos são disparados por configurações particulares do estado. Vários sistemas reativos são exemplos desta classe de aplicações, como protocolos para sistemas distribuídos e móveis, simulação de sistemas biológicos, entre outros. A verificação de gramática de grafos através da técnica de verificação de modelos já é utilizada por diversas abordagens. Embora esta técnica constitua um método de análise bastante importante, ela tem como desvantagem a necessidade de construir o espaço de estados completo do sistema, o que pode levar ao problema da explosão de estados. Bastante progresso tem sido feito para lidar com esta dificuldade, e diversas técnicas têm aumentado o tamanho dos sistemas que podem ser verificados. Outras abordagens propõem aproximar o espaço de estados, mas neste caso não é possível a verificação de propriedades arbitrárias. Além da verificação de modelos, a prova de teoremas constitui outra técnica consolidada para verificação formal. Nesta técnica tanto o sistema quanto suas propriedades são expressas em alguma lógica matemática. O processo de prova consiste em encontrar uma prova a partir dos axiomas e lemas intermediários do sistema. Cada técnica tem argumentos pró e contra o seu uso, mas é possível dizer que a verificação de modelos e a prova de teoremas são complementares. A maioria das abordagens utilizam verificadores de modelos para analisar propriedades de computações, isto é, sobre a seqüência de passos de um sistema. Propriedades sobre estados alcançáveis só são verificadas de forma restrita. O objetivo deste trabalho é prover uma abordagem para a prova de propriedades de grafos alcançáveis de uma gramática de grafos através da técnica de prova de teoremas. Propõe-se uma tradução (da abordagem Single-Pushout) de gramática de grafos para uma abordagem lógica e relacional, a qual permite a aplicação de indução matemática para análise de sistemas com espaço de estados infinito. Definiu-se gramática de grafos utilizando estruturas relacionais e aplicações de regras com linguagens lógicas. Inicialmente considerou-se o caso de grafos (tipados) simples, e então se estendeu a abordagem para grafos com atributos e gramáticas com condições negativas de aplicação. Além disso, baseado nesta abordagem, foram estabelecidos padrões para a definição, codificação e reuso de especificações de propriedades. O sistema de padrões tem o objetivo de auxiliar e simplificar a tarefa de especificar requisitos de forma precisa. Finalmente, propõe-se implementar definições relacionais de gramática de grafos em estruturas de event-B, de forma que seja possível utilizar os provadores disponíveis para event-B para demonstrar propriedades de gramática de grafos. / Graph grammars are a formal language well-suited to applications in which states have a complex topology (involving not only many types of elements, but also different types of relations between them) and in which behaviour is essentially data-driven, that is, events are triggered basically by particular configurations of the state. Many reactive systems are examples of this class of applications, such as protocols for distributed and mobile systems, simulation of biological systems, and many others. The verification of graph grammar models through model-checking is currently supported by various approaches. Although model-checking is an important analysis method, it has as disadvantage the need to build the complete state space, which can lead to the state explosion problem. Much progress has been made to deal with this difficulty, and many techniques have increased the size of the systems that may be verified. Other approaches propose to over- and/or under-approximate the state-space, but in this case it is not possible to check arbitrary properties. Besides model checking, theorem proving is another wellestablished approach for verification. Theorem proving is a technique where both the system and its desired properties are expressed as formulas in some mathematical logic. A logical description defines the system, establishing a set of axioms and inference rules. The process of verification consists of finding a proof of the required property from the axioms or intermediary lemmas of the system. Each verification technique has arguments for and against its use, but we can say that model-checking and theorem proving are complementary. Most of the existing approaches use model checkers to analyse properties of computations, that is, properties over the sequences of steps a system may engage in. Properties about reachable states are handled, if at all possible, only in very restricted ways. In this work, our main aim is to provide a means to prove properties of reachable graphs of graph grammar models using the theorem proving technique. We propose an encoding of (the Single-Pushout approach of) graph grammar specifications into a relational and logical approach which allows the application of the mathematical induction technique to analyse systems with infinite state-spaces. We have defined graph grammars using relational structures and used logical languages to model rule applications. We first consider the case of simple (typed) graphs, and then we extend the approach to the non-trivial case of attributed-graphs and grammars with negative application conditions. Besides that, based on this relational encoding, we establish patterns for the presentation, codification and reuse of property specifications. The pattern has the goal of helping and simplifying the task of stating precise requirements to be verified. Finally, we propose to implement relational definitions of graph grammars in event-B structures, such that it is possible to use the event-B provers to demonstrate properties of a graph grammar.

O envelhecimento populacional tem como uma de suas implicações o aumento do número de indivíduos com incapacidade funcional, o que gera uma demanda por de cuidados de longa duração, exercidos principalmente pelas famílias. Essas, por suas transformações contemporâneas tendem a ter reduzida a sua capacidade de atender a essa demanda. Assim, a presença do cuidador formal domiciliar de pessoa idosa como elemento fundamental, nesse contexto, deixa de ser um problema do âmbito privado e configura-se em uma questão de saúde pública. O presente estudo investigou a trajetória ocupacional de cuidadoras formais domiciliares de pessoas idosas, com o objetivo de compreender seus principais eventos e características, a percepção que elas têm do seu trabalho, de seu processo de capacitação e do cuidado. Nesta pesquisa qualitativa, os dados foram examinados com utilização da técnica da Análise do Discurso, a partir da construção de uma linha cronológica das trajetórias, com seus principais eventos e categorização das frases significativas, destacadas dos relatos. As categorias empíricas de análise foram: trabalho, gênero, qualificação e cuidado. Verificou-se que as mulheres chegam ao trabalho de cuidadora formal domiciliar de pessoa idosa pelo trabalho doméstico, pela qualificação formal ou pela experiência de cuidar de seus familiares idosos. As trajetórias são caracterizadas pela precarização do trabalho, especialmente daqueles desenvolvidos no ambiente domiciliar, pela inserção e reinserção das mulheres no mercado de trabalho via ambiente doméstico, pela desvalorização do trabalho feminino, pela dificuldade em conciliar os cuidados aos filhos e familiares idosos com o trabalho remunerado, pela escolarização e profissionalização (quando há) tardias, pela experiência prática como sendo a principal ferramenta qualificadora, e pelo cuidado como disposição ética promotora de sentido para a atividade laboral. Conclui-se que, a promoção de relações de gênero mais igualitárias, a educação formal específica, a regulamentação da profissão e a adoção de um novo modelo de trabalho e emprego na área de cuidados à pessoa idosa, podem melhorar a qualidade desse trabalho, assim como promover o bem estar dos idosos dependentes e de suas famílias / One of the consequences of population aging is the growth of individuals with functional disability which creates a demand for long term care, primarily exercised by the families. Due to contemporary transformations, families tend to reduce their ability to meet this demand. Therefore, the presence formal home caregiver of elderly as a key element in this context is no longer a private issue to become a matter of public health. The present study investigated the occupational trajectory of formal female home caregivers of elderly, aiming to understand their key events and their main characteristics, as well as the perception they have of their own job, their process of training and about care itself. This qualitative research has examined the data using the Discourse Analysis technique, starting from the construction of a timeline of each trajectory, which embraced its main events and the categorization of all significant sentences, highlighted from their stories. The empirical categories of analysis were: work, gender, qualification and care. It was found that women start up as formal home caregivers of elderly through domestic housework, formal qualification or the experience of caring for their own elderly relatives. The trajectories are characterized by poor job relations, especially the ones developed in the home environment, by the integration and reintegration of women into the labor market through domestic environment, the devaluation of women\'s work, by the difficulty in reconciling the care of their children and elderly relatives with their professional paid activities, for late education and professional training (when existed), by practical experience as the main qualifying tool, and the care as an ethical promoter of sense for labor activities. This study concludes that promoting more equitable gender relation, specific formal education, legal regulation of the profession and the adoption of a new model of work and employment for the formal caregivers of elderly field, tend to improve the quality of this work, as well as promote the well-being of the dependent elderly and their families.