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.

Orientador: Itala Maria Loffredo D'Ottaviano / Dissertação (mestrado) - Universidade Estadual de Campinas, Instituto de Filosofia e Ciências Humanas / Made available in DSpace on 2018-08-22T15:04:13Z (GMT). No. of bitstreams: 1 Almeida_EdgarLuisBezerrade_M.pdf: 946200 bytes, checksum: e8e316a3ee7420c8d7f45a751651a436 (MD5) Previous issue date: 2013 / Resumo: Esta Dissertação apresenta uma definição de lógica abstrata e caracteriza alguns sistemas lógicos bastante conhecidos na literatura como casos particulares desta. Em especial, mostramos que a lógica de primeira ordem, lógica de segunda ordem, lógica com o operador Q1 de Mostowski e a lógica infinitária L!1! são casos particulares de lógicas abstratas. Mais que isso, mostramos que tais lógicas são regulares. Na análise de cada uma das lógicas acima citadas, mostramos o comportamento das mesmas com relação às propriedades de Löwenheim-Skolem e compacidade enumerável, resultados estes centrais à teoria de modelos. Nossa análise permite-nos constatar que, dentre os quatro casos apresentados, o único que goza de ambas as propriedades é a lógica de primeira ordem; as demais falham em uma, na outra ou em ambas as propriedades. Mostramos que isso não é mera coincidência, mas sim um resultado profundo, que estabelece fronteiras bem delimitadas à lógica de primeira ordem, conhecido como primeiro teorema de Lindström: se uma lógica é regular, ao menos tão expressiva quanto à lógica de primeira ordem e satisfaz ambas as propriedades citadas, então esta é equivalente a lógica de primeira ordem. Realizamos uma prova cuidadosa do teorema, em que cada ideia e cada estratégia de prova é estabelecida criteriosamente. Com seu trabalho, Lindström inaugurou um novo e profícuo campo de estudo, a teoria abstrata de modelos que estabelece, com relação a diversas combinações de propriedades de sistemas lógicos, uma estratificação entre lógicas. Apresentamos um outro exemplo de tal estratificação através de uma versão modal do teorema de Lindström, versão esta que caracteriza a lógica modal básica como maximal quanto a bissimilaridade e compacidade. Encerramos esta Dissertação com algumas considerações acerca da influência do primeiro teorema de Lindström / Abstract: This thesis presents the definition of abstract logic and features some quite logical systems presented in the literature as particular cases of this. In particular, we show that first-order logic, second-order logic, the logic with Mostowski's operator Q1 and the infinitary logic L!1! are specific systems of abstract logic. Moreover, we show that such logics are regular. In the analysis of each above mentioned logical systems we analyses his performance with regard to the properties of compactness and Löwenheim-Skolem, results that have important role in model theory. Our analysis allows us to conclude that among the four cases, the only one who enjoys both properties is the first-order logic, and all others fail in one, other or both properties. We show that this is not mere coincidence, but rather a deep, well-defined boundaries establishing the first-order logic, known as first Lindström's theorem: a regular logic that is at least as expressive as first-order logic and satisfies both properties mentioned, then this is equivalent to first-order logic. We conducted a thorough proof of the theorem, in which each idea and each proof strategy is carefully established. With his work Lindström inaugurated a new and fruitful field of study, the abstract model theory, which establishes with respect to different combinations of properties of logical systems, stratification between logical. Here is another example of such stratification through one of the theorem of modal version Lindström, which characterizes this version of the logic basic modal such as maximal bissimimulation and compactness. We conclude the thesis with some considerations about the influence of the Lindström's theorem / Mestrado / Filosofia / Mestre em Filosofia

The increasing use of model-driven software development has renewed emphasis on using domain-specific models during application development. More specifically, there has been emphasis on using domain-specific modeling languages (DSMLs) to capture user-specified requirements when creating applications. The current approach to realizing these applications is to translate DSML models into source code using several model-to-model and model-to-code transformations. This approach is still dependent on the underlying source code representation and only raises the level of abstraction during development. Experience has shown that developers will many times be required to manually modify the generated source code, which can be error-prone and time consuming. An alternative to the aforementioned approach involves using an interpreted domain-specific modeling language (i-DSML) whose models can be directly executed using a Domain Specific Virtual Machine (DSVM). Direct execution of i-DSML models require a semantically rich platform that reduces the gap between the application models and the underlying services required to realize the application. One layer in this platform is the domain-specific middleware that is responsible for the management and delivery of services in the specific domain. In this dissertation, we investigated the problem of designing the domain-specific middleware of the DSVM to facilitate the bifurcation of the semantics of the domain and the model of execution (MoE) while supporting runtime adaptation and validation. We approached our investigation by seeking solutions to the following sub-problems: (1) How can the domain-specific knowledge (DSK) semantics be separated from the MoE for a given domain? (2) How do we define a generic model of execution (GMoE) of the middleware so that it is adaptable and realizes DSK operations to support delivery of services? (3) How do we validate the realization of DSK operations at runtime? Our research into the domain-specific middleware was done using an i-DSML for the user-centric communication domain, Communication Modeling Language (CML), and for microgrid energy management domain, Microgrid Modeling Language (MGridML). We have successfully developed a methodology to separate the DSK and GMoE of the middleware of a DSVM that supports specialization for a given domain, and is able to perform adaptation and validation at runtime.

<p>Many computer systems in our daily life require highly available applications (such as medical equipment) and some others run on difficult to access places (such as satellites). These systems are subject to a variety of potential failures that may degrade their performance. Therefore, being able to reason about faults and their impact on systems is gaining considerable attention. Existing work on fault tolerance is mostly focused on addressing faults at the programming language level. In the recent past, significant efforts have been made to use formal methods to specify and verify fault tolerant systems to provide more reliable software. Related with this, some researchers have pointed out that Deontic Logic is useful for reasoning about fault tolerant systems due to its expressive nature in relation to defining norms, used to describe expected behaviour and prescribing what happens when these norms are violated.</p> <p>In this thesis, we demonstrate how Deontic Logic can be used to model an existing real world problem concerning fault tolerance mechanisms. We consider different situations that a vehicle faces on the road and the consequent reactions of the driver or vehicle based on good and bad behaviour. We got the idea and motivation for this case study from the SASPENCE sub-project, conducted under the European Integrated Project PReVENT. This sub-project focuses on a vehicle’s behaviour in maintaining safe speed and safe distance on the road. As our first modelling attempt, we use a Propositional Deontic Logic approach, to justify to what extent we can apply this Logical approach to model a real world problem. Subsequently, we use a First Order Deontic Logic approach, as it can incorporate the use of parameters and quantification over them, which is more useful to model real world scenarios.</p> <p>We state and prove some interesting expected properties of the models using a First Order proof system. Based on these modelling exercises, we acquired different engineering ideas and lessons, and present them in this thesis in order to aid modelling of future fault tolerant systems.</p> / Master of Science (MSc)

The specification of enterprise information systems using formal specification languages enables the formal verification of these systems. Reasoning about the properties of a formal specification is a tedious task that can be facilitated much through the use of an automated reasoner. However, set theory is a corner stone of many formal specification languages and poses demanding challenges to automated reasoners. To this end a number of heuristics has been developed to aid the Otter theorem prover in finding short proofs for set-theoretic problems. This dissertation investigates the applicability of these heuristics to next generation theorem provers. / Computing / M.Sc. (Computer Science)

Programs have precise semantics, so we can use mathematical proof to establish their properties. These proofs are often too large to validate with the usual "social process" of mathematics, so instead we create and check them with theorem-proving software. This software must be advanced enough to make the proof process tractable, but this very sophistication casts doubt upon the whole enterprise: who verifies the verifier? We begin with a simple proof checker, Level 1, that only accepts proofs composed of the most primitive steps, like Instantiation and Cut. This program is so straightforward the ordinary, social process can establish its soundness and the consistency of the logical theory it implements (so we know theorems are "always true"). Next, we develop a series of increasingly capable proof checkers, Level 2, Level 3, etc. Each new proof checker accepts new kinds of proof steps which were not accepted in the previous levels. By taking advantage of these new proof steps, higher-level proofs can be written more concisely than lower-level proofs, and can take less time to construct and check. Our highest-level proof checker, Level 11, can be thought of as a simplified version of the ACL2 or NQTHM theorem provers. One contribution of this work is to show how such systems can be verified. To establish that the Level 11 proof checker can be trusted, we first use it, without trusting it, to prove the fidelity of every Level n to Level 1: whenever Level n accepts a proof of some phi, there exists a Level 1 proof of phi. We then mechanically translate the Level 11 proof for each Level n into a Level n - 1 proof---that is, we create a Level 1 proof of Level 2's fidelity, a Level 2 proof of Level 3's fidelity, and so on. This layering shows that each level can be trusted, and allows us to manage the sizes of these proofs. In this way, our system proves its own fidelity, and trusting Level 11 only requires us to trust Level 1. / text

To improve quality of software systems, change-based fault prediction and scope-bounded checking have been used to predict or detect faults during software development. In fault prediction, changes to program source code, such as added lines or deleted lines, are used to predict potential faults. In fault detection, scope-bounded checking of programs is an effective technique for finding subtle faults. The central idea is to check all program executions up to a given bound. The technique takes two basic forms: scope-bounded static checking, where all bounded executions of a program are transformed into a formula that represents the violation of a correctness property and any solution to the formula represents a counterexample; or scope-bounded testing where a program is tested against all (small) inputs up to a given bound on the input size. Although the accuracies of change-based fault prediction and scope-bounded checking have been evaluated with experiments, both of them have effectiveness and efficiency limitations. Previous change-based fault predictions only consider the code modified by a change while ignoring the code impacted by a change. Scope-bounded testing only concerns the correctness specifications, and the internal structure of a program is ignored. Although scope-bounded static checking considers the internal structure of programs, formulae translated from structurally complex programs might choke the backend analyzer and fail to give a result within a reasonable time. To improve effectiveness and efficiency of these approaches, we introduce local semantic analysis into change-based fault prediction and scope-bounded checking. We use data-flow analysis to disclose internal dependencies within a program. Based on these dependencies, we identify code segments impacted by a change and apply fault prediction metrics on impacted code. Empirical studies with real data showed that semantic analysis is effective and efficient in predicting faults in large-size changes or short-interval changes. While generating inputs for scope-bounded testing, we use control-flow to guide test generation so that code coverage can be achieved with minimal tests. To increase the scalability of scope-bounded checking, we split a bounded program into smaller sub-programs according to data-flow and control-flow analysis. Thus the problem of scope-bounded checking for the given program reduces to several sub-problems, where each sub-problem requires the constraint solver to check a less complex formula, thereby likely reducing the solver’s overall workload. Experimental results show that our approach provides significant speed-ups over the traditional approach. / text

Made available in DSpace on 2016-04-27T17:27:13Z (GMT). No. of bitstreams: 1 Carlos Roberto Teixeira Alves.pdf: 1331347 bytes, checksum: cebe03a83120937101a3595710844df2 (MD5) Previous issue date: 2015-12-14 / Coordenação de Aperfeiçoamento de Pessoal de Nível Superior / This work aims to show the current treatment of the semantic notion of satisfiability to the logic of the first order, the relevant problems of Tarski's solution to define this notion - in this case, the use of infinite sequences to satisfy the formulas - and propose an alternative to circumvent this problem. The notion established by Tarski became, in discussions on the subject, standard solution and resulted in rich tools to work with the languages, in particular tools such as the Theory of Models. However, from a philosophical point of view, it is very important to broaden perspectives and look at the problem from a new dimension. Our proposal is to avoid the counterintuitive idea of using infinite sequences of objects to satisfy the finite formulas, knowing that these infinite sequences are composed almost entirely of 'superfluous terms', expendable in the process of satisfaction, but they should and are listed and indexed in the process. It would be interesting to solve the issue involving sequences without 'superfluous terms'. We propose a structure of first-order language that dispenses variables and constants. The notion of satisfaction in this case is distinct, which increases the possibilities and provides an alternative to the satisfaction of infinite sequences. In the end, we show how our solution can produce the satisfaction of formulas of a first-order language within a framework where satisfaction is interpreted according to certain specific criteria and can be performed by finite sequences, differing essentially from Tarski solution / Este trabalho tem por objetivo mostrar o tratamento atual da noção semântica de satisfatibilidade para as lógicas de primeira ordem, os problemas relevantes da solução de Tarski para definir essa noção no caso, o uso de sequências infinitas para a satisfação das fórmulas , e propor uma alternativa que contorne esse problema. A noção estabelecida por Tarski tornou-se, nas discussões a respeito do tema, a solução padrão e resultou em ferramentas ricas para operar com as linguagens, em especial ferramentas como a Teoria dos Modelos. No entanto, de um ponto de vista filosófico, é sadio ampliar as perspectivas e olhar o problema sob uma dimensão nova. Nossa proposta é superar a ideia contraintuitiva de elencarmos sequências infinitas de objetos para satisfação das formulas finitas, sabendo que essas sequências infinitas são compostas quase que totalmente de termos supérfluos , dispensáveis no processo de satisfação, mas que devem e são enumerados e indexados no processo. Seria interessante solucionar a questão envolvendo sequências sem termos supérfluos . Proporemos uma estrutura de linguagem de primeira ordem que dispensa variáveis e constantes. A noção de satisfação nesse caso é distinta, o que amplia as possibilidades e fornece uma alternativa à satisfação por sequências infinitas. No fim, mostraremos como nossa solução consegue produzir a satisfação de fórmulas de uma linguagem de primeira ordem dentro de uma estrutura interpretada onde a satisfação ocorre segundo certos critérios específicos e consegue ser realizada por sequências finitas, diferindo essencialmente da solução de Tarski

Application of neural networks in deep learning is rapidly growing due to their ability to outperform other machine learning algorithms in different kinds of problems. But one big disadvantage of deep neural networks is its internal logic to achieve the desired output or result that is un-understandable and unexplainable. This behavior of the deep neural network is known as “black box”. This leads to the following questions: how prevalent is the black box problem in the research literature during a specific period of time? The black box problems are usually addressed by socalled rule extraction. The second research question is: what rule extracting methods have been proposed to solve such kind of problems? To answer the research questions, a systematic literature review was conducted for data collection related to topics, the black box, and the rule extraction. The printed and online articles published in higher ranks journals and conference proceedings were selected to investigate and answer the research questions. The analysis unit was a set of journals and conference proceedings articles related to the topics, the black box, and the rule extraction. The results conclude that there has been gradually increasing interest in the black box problems with the passage of time mainly because of new technological development. The thesis also provides an overview of different methodological approaches used for rule extraction methods.

Les bibliothèques numériques sont des systèmes d'information complexes stockant des ressources numériques (par exemple, texte, images, sons, audio), ainsi que des informations sur les ressources numériques ou non-numériques; ces informations sont appelées des métadonnées. Nous proposons un modèle de données pour les bibliothèques numériques permettant l'identification des ressources, l’utilisation de métadonnées et la réutilisation des ressources stockées, ainsi qu’un langage de requêtes pour l’interrogation de ressources. Le modèle que nous proposons est inspiré par l'architecture du Web, qui forme une base solide et universellement acceptée pour les notions et les services attendus d'une bibliothèque numérique. Nous formalisons notre modèle comme une théorie du premier ordre, afin d’exprimer les concepts de bases de la bibliothèque numérique, sans aucune contrainte technique. Les axiomes de la théorie donnent la sémantique formelle des notions du modèle, et en même temps fournissent une définition de la connaissance qui est implicite dans une bibliothèque numérique. La théorie est traduite en un programme Datalog qui, étant donnée une bibliothèque numérique, permet de la compléter efficacement avec les connaissances implicites. Le but de notre travail est de contribuer à la technologie de gestion des informations des bibliothèques numériques. De cette façon, nous pouvons montrer la faisabilité théorique de notre modèle, en montrant qu'il peut être efficacement appliqué. En outre, nous démontrons la faisabilité pratique du modèle en fournissant une traduction complète du modèle en RDF et du langage de requêtes en SPARQL.Nous fournissons un calcul sain et complet pour raisonner sur les graphes RDF résultant de la traduction. Selon ce calcul, nous prouvons la correction de ces deux traductions, montrant que les fonctions de traduction préservent la sémantique de la bibliothèque numérique et de son langage de requêtes. / Digital Libraries are complex information systems, storing digital resources (e.g., text, images, sound, audio), as well as knowledge about digital or non-digital resources; this knowledge is referred to as metadata. We propose a data model for digital libraries supporting resource identification, use of metadata and re-use of stored resources, as well as a query language supporting discovery of resources. The model that we propose is inspired by the architecture of the Web, which forms a solid, universally accepted basis for the notions and services expected from a digital library. We formalize our model as a first-order theory, in order to be able to express the basic concepts of digital libraries without being constrained by any technical considerations. The axioms of the theory give the formal semantics of the notions of the model, and at the same time, provide a definition of the knowledge that is implicit in a digital library. The theory is then translated into a Datalog program that, given a digital library, allows to efficiently complete the digital library with the knowledge implicit in it. The goal of our research is to contribute to the information management technology of digital libraries. In this way, we are able to demonstrate the theoretical feasibility of our digital library model, by showing that it can be efficiently implemented. Moreover, we demonstrate our model’s practical feasibility by providing a full translation of the model into RDF and of the query language into SPARQL. We provide a sound and complete calculus for reasoning on the RDF graphs resulting from translation. Based on this calculus, we prove the correctness of both translations, showing that the translation functions preserve the semantics of the digital library and of the query language.