Yes / Fault tree analysis (FTA) is a powerful technique that is widely used for evaluating system safety and reliability. It can be used to assess the effects of combinations of failures on system behaviour but is unable to capture sequence dependent dynamic behaviour. A number of extensions to fault trees have been proposed to overcome this limitation. Pandora, one such extension, introduces temporal gates and temporal laws to allow dynamic analysis of temporal fault trees (TFTs). It can be easily integrated in model-based design and analysis techniques. The quantitative evaluation of failure probability in Pandora TFTs is performed using exact probabilistic data about component failures. However, exact data can often be difficult to obtain. In this paper, we propose a method that combines expert elicitation and fuzzy set theory with Pandora TFTs to enable dynamic analysis of complex systems with limited or absent exact quantitative data. This gives Pandora the ability to perform quantitative analysis under uncertainty, which increases further its potential utility in the emerging field of model-based design and dependability analysis. The method has been demonstrated by applying it to a fault tolerant fuel distribution system of a ship, and the results are compared with the results obtained by other existing techniques.

Yes / Fuzzy data-driven reliability analysis has been used in different safety-critical domains for risk assessment and decision-making where precise failure data is non-existent. Expert judgements and fuzzy set theory have been combined with different variants of fault trees as part of fuzzy data-driven reliability analysis studies. In such fuzzy fault tree analyses, different people represented failure data using different membership functions for the fuzzy set, and different parameters were set differently in the expert opinion elicitation process. Due to the availability of a wide variety of options, it is possible to obtain different outcomes when choosing one option over another. This article performed an analysis in the context of fuzzy data-based temporal fault tree analysis to investigate the effect of choosing different membership functions on the estimated system reliability and criticality ranking of different failure events. Moreover, the effect of using different values for the relaxation factor, a parameter set during the expert elicitation process, was studied on the system reliability and criticality evaluation. The experiments on the fuel distribution system case study show system reliability did not vary when triangular and trapezoidal fuzzy numbers were used with the same upper and lower bounds. However, it was seen that the criticality rankings of a couple of events were changed due to choosing different membership functions and different values of relaxation factor

Specification plays a vital role in software engineering to facilitate the development of highly dependable software. The importance of specification in software development is to serve, amongst others, as a communication tool for stakeholders in the software project. The specification also adds to the understanding of operations, and describes the properties of a system. Various techniques may be used for specification work. Z is a formal specification language that is based on a strongly-typed fragment of Zermelo-Fraenkel set theory and first-order logic to provide for precise and unambiguous specifications. Z uses mathematical notation to build abstract data, which is necessary for a specification. The role of abstraction is to describe what the system does without prescribing how it should be done. Diagrams, on the other hand, have also been used in various areas, and in software engineering they could be used to add a visual component to software specifications. It is plausible that diagrams may also be used to reason in a semi-formal way about the properties of a specification. Many diagrammatic languages are based on contours and set theory. Examples of these languages are Euler-, Spider-, Venn- and Pierce diagrams. Euler diagrams form the foundation of most diagrams that are based on closed curves. Diagrams, on the other hand, have also been used in various areas, and in software engineering they could be used to add a visual component to software specifications. It is plausible that diagrams may also be used to reason in a semi-formal way about the properties of a specification. Many diagrammatic languages are based on contours and set theory. Examples of these languages are Euler-, Spider-, Venn- and Pierce diagrams. Euler diagrams form the foundation of most diagrams that are based on closed curves. The purpose of this research is to demonstrate the extent to which diagrams can be used to represent a Z specification. A case study is used to transform the specification modelled with Z language into a diagrammatic specification. Euler, spider, Venn and Pierce diagrams are combined for this purpose, to form one diagrammatic notation that is used to transform a Z specification / School of Computing / M. Sc. (Information Systems)

No description available.

Fuzzy relational databases deal with imprecise data or fuzzy information in a relational database. The purpose of this fuzzy database implementation is to retrieve images by using fuzzy queries whose common-language descriptions are defined by the consensus of a particular user community. The fuzzy set, which is presentation of fuzzy attribute values of the images, is determined through membership function. This paper compares two methods of constructing membership functions, the Direct Rating and New Random Proportional, to determine which method gives maximum users satisfaction with minimum feedback from the community. The statistical analysis of results suggests the use of Direct Rating method. Moreover, the analysis shows that the performance of the New Random Proportional method can be improved with the inclusion of a "Not" modifier. This paper also identifies and analyzes issues that are raised by different versions of the database system.

The GUHA method is one of the oldest methods of exploratory data analysis, which is regarded as part of the data mining or knowledge discovery in databases (KDD) scienti_c area. Unlike many other methods of data mining, the GUHA method has firm theoretical foundations in logic and statistics. In scope of the method, finding interesting knowledge corresponds to finding special formulas in satisfactory rich logical calculus, which is called observational calculus. The main topic of the thesis is application of the "fuzzy paradigm" to the GUHA method By the term "fuzzy paradigm" we mean approaches that use many-valued membership degrees or truth values, namely fuzzy set theory and fuzzy logic. The thesis does not aim to cover all the aspects of this application, it emphasises mainly on: - Association rules as the most prevalent type of formulas mined by the GUHA method - Usage of fuzzy data - Logical aspects of fuzzy association rules mining - Comparison of the GUHA theory to the mainstream fuzzy association rules - Implementation of the theory using the bit string approach The thesis throughoutly elaborates the theory of fuzzy association rules, both using the theoretical apparatus of fuzzy set theory and fuzzy logic. Fuzzy set theory is used mainly to compare the GUHA method to existing mainstream approaches to formalize fuzzy association rules, which were studied in detail. Fuzzy logic is used to define novel class of logical calculi called logical calculi of fuzzy association rules (LCFAR) for logical representation of fuzzy association rules. The problem of existence of deduction rules in LCFAR is dealt in depth. Suitable part of the proposed theory is implemented in the Ferda system using the bit string approach. In the approach, characteristics of examined objects are represented as strings of bits, which in the crisp case enables efficient computation. In order to maintain this feature also in the fuzzy case, a profound low level testing of data structures and algoritms for fuzzy bit strings have been carried out as a part of the thesis.

O presente trabalho centra-se no estudo da narrativa do romance O Castelo, escrito em 1922, pelo escritor tcheco Franz Kafka. Por meio da análise formal da obra em questão, objetiva-se estabelecer relações entre aspectos presentes na narrativa que possuam associações metafóricas a temas vigentes no cotidiano do autor e, conseqüentemente, do homem moderno, e que possuam conotação negativa, tais como o poder, simbolizado pela burocracia, pela divinização, e pelo espaço. Partindo dessa premissa, propõe-se relacionar esses temas à teoria dos conjuntos da matemática, na qual um conjunto maior contém um conjunto menor, esse atuando por sua vez como um subconjunto daquele. Propõe-se aqui fazer uma analogia do conjunto poder e seu enfoque negativo como poder com o subconjunto burocracia, este intimamente ligado àquele, e que possui intersecção com os subconjuntos divinização e espaço. Por fim, ressaltar-se-á a universalidade da obra de Kafka, que possibilita a efetuação de analogias temáticas das mais diversas, não só as aqui expostas em forma de conjuntos e subconjuntos, pelo fato de seu texto ser multifacetado no tocante a temas. / This monograph focuses on analyzing the narrative of The Castle, a novel written by the Czech author Franz Kafka, in 1922. It aims at establishing a connection between certain aspects within the text which may have a metaphorical association with themes related to not only the authors life experiences, but also any other modern mans. It will be centered on a formal analysis of the novel and on metaphorical aspects within the narrative, which may have a negative connotation linked with power, represented by bureaucracy, divinization and space. Afterwards, we will propose a relation of such themes to the set theory from Mathematics, in which a greater set contains a smaller set, also known as a subset. We aim at drawing an analogy of power as a set and its negative connotation with the bureaucratic subset, which are intimately connected. Bureaucracy intersects the two other subsets called divinization and space. Eventually, we will focus on the universality of Kafkas work, which enables the drawing of many other thematic analogies, not only the ones discussed in this set theory proposed in this monograph, due to the fact that Kafkas work is multifaceted in terms of themes.

Cette thèse présente des techniques efficaces pour déléguer des obligations de preuves TLA+ dans des démonstrateurs automatiques basées sur la logique du premier ordre non-sortée et multi-sortée. TLA+ est un langage formel pour la spécification et vérification des systèmes concurrents et distribués. Sa partie non-temporelle basée sur une variante de la théorie des ensembles Zermelo-Fraenkel permet de définir des structures de données. Le système de preuves TLAPS pour TLA+ est un environnement de preuve interactif dans lequel les utilisateurs peuvent vérifier de manière déductive des propriétés de sûreté sur des spécifications TLA+. TLAPS est un assistant de preuve qui repose sur les utilisateurs pour guider l’effort de preuve, il permet de générer des obligations de preuve puis les transmet aux vérificateurs d’arrière-plan pour atteindre un niveau satisfaisant d’automatisation. Nous avons développé un nouveau démonstrateur d’arrière-plan qui intègre correctement dans TLAPS des vérificateurs externes automatisés, en particulier, des systèmes ATP et solveurs SMT. Deux principales composantes constituent ainsi la base formelle pour la mise en oeuvre de ce nouveau vérificateur. Le premier est un cadre de traduction générique qui permet de raccorder à TLAPS tout démonstrateur automatisé supportant les formats standards TPTP/ FOF ou SMT-LIB/AUFLIA. Afin de coder les expressions d’ordre supérieur, tels que les ensembles par compréhension ou des fonctions totales avec des domaines, la traduction de la logique du premier ordre repose sur des techniques de réécriture couplées à une méthode par abstraction. Les théories sortées telles que l’arithmétique linéaire sont intégrés par injection dans la logique multi-sortée. La deuxième composante est un algorithme pour la synthèse des types dans les formules (non-typées) TLA+. L’algorithme, qui est basé sur la résolution des contraintes, met en oeuvre un système de type avec types élémentaires, similaires à ceux de la logique multi-sortée, et une extension avec des types dépendants et par raffinement. Les informations de type obtenues sont ensuite implicitement exploitées afin d’améliorer la traduction. Cette approche a pu être validé empiriquement permettant de démontrer que les vérificateurs ATP/SMT augmentent de manière significative le développement des preuves dans TLAPS / This thesis presents effective techniques for discharging TLA+ proof obligations to automated theorem provers based on unsorted and many-sorted first-order logic. TLA+ is a formal language for specifying and verifying concurrent and distributed systems. Its non-temporal fragment is based on a variant of Zermelo-Fraenkel set theory for specifying the data structures. The TLA+ Proof System TLAPS is an interactive proof environment in which users can deductively verify safety properties of TLA+ specifications. While TLAPS is a proof assistant that relies on users for guiding the proof effort, it generates proof obligations and passes them to backend verifiers to achieve a satisfactory level of automation. We developed a new back-end prover that soundly integrates into TLAPS external automated provers, specifically, ATP systems and SMT solvers. Two main components provide the formal basis for implementing this new backend. The first is a generic translation framework that allows to plug to TLAPS any automated prover supporting the standard input formats TPTP/FOF or SMT-LIB/AUFLIA. In order to encode higher-order expressions, such as sets by comprehension or total functions with domains, the translation to first-order logic relies on term-rewriting techniques coupled with an abstraction method. Sorted theories such as linear integer arithmetic are homomorphically embedded into many-sorted logic. The second component is a type synthesis algorithm for (untyped) TLA+ formulas. The algorithm, which is based on constraint solving, implements one type system for elementary types, similar to those of many-sorted logic, and an expansion with dependent and refinement types. The obtained type information is then implicitly exploited to improve the translation. Empirical evaluation validates our approach: the ATP/SMT backend significantly boosts the proof development in TLAPS

Dans ces travaux de thèse nous proposons de tirer parti de la théorie des ensembles flous afin d'améliorer les interactions entre les systèmes de bases de données et les utilisateurs. Les mécanismes coopératifs visent à aider les utilisateurs à mieux interagir avec les SGBD. Ces mécanismes doivent faire preuve de robustesse : ils doivent toujours pouvoir proposer des réponses à l'utilisateur. Empty set (0,00 sec) est un exemple typique de réponse qu'il serait désirable d'éradiquer. Le caractère informatif des explications de réponses est parfois plus important que les réponses elles-mêmes : ce peut être le cas avec les réponses vides et pléthoriques par exemple, d'où l'intérêt de mécanismes coopératifs robustes, capables à la fois de contribuer à l'explication ainsi qu'à l'amélioration des résultats. Par ailleurs, l'utilisation de termes de la langue naturelle pour décrire les données permet de garantir l'interprétabilité des explications fournies. Permettre à l'utilisateur d'utiliser des mots de son propre vocabulaire contribue à la personnalisation des explications et améliore l'interprétabilité. Nous proposons de nous intéresser aux explications dans le contexte des réponses coopératives sous trois angles : 1) dans le cas d'un ensemble pléthorique de résultats ; 2) dans le contexte des systèmes de recommandation ; 3) dans le cas d'une recherche à partir d'exemples. Ces axes définissent des approches coopératives où l'intérêt des explications est de permettre à l'utilisateur de comprendre comment sont calculés les résultats proposés dans un effort de transparence. Le caractère informatif des explications apporte une valeur ajoutée aux résultats bruts, et forme une réponse coopérative. / In this thesis, we are interested in how we can leverage fuzzy logic to improve the interactions between relational database systems and humans. Cooperative answering techniques aim to help users harness the potential of DBMSs. These techniques are expected to be robust and always provide answer to users. Empty set (0,00 sec) is a typical example of answer that one may wish to never obtain. The informative nature of explanations is higher than that of actual answers in several cases, e.g. empty answer sets and plethoric answer sets, hence the interest of robust cooperative answering techniques capable of both explaining and improving an answer set. Using terms from natural language to describe data --- with labels from fuzzy vocabularies --- contributes to the interpretability of explanations. Offering to define and refine vocabulary terms increases the personalization experience and improves the interpretability by using the user's own words. We propose to investigate the use of explanations in a cooperative answering setting using three research axes: 1) in the presence of a plethoric set of answers; 2) in the context of recommendations; 3) in the context of a query/answering problem. These axes define cooperative techniques where the interest of explanations is to enable users to understand how results are computed in an effort of transparency. The informativeness of the explanations brings an added value to the direct results, and that in itself represents a cooperative answer.

Concept Maps (CMs) are considered a well-known pedagogy technique in creating curriculum, educating, teaching, and learning. Determining comprehension of concepts result from comparisons of candidate CMs against a master CM, and evaluate "goodness". Past techniques for comparing CMs have revolved around the creation of a subjective rubric. We propose a novel CM scoring scheme called MAnanA based on a Fuzzy Similarity Scaling (FSS) score to vastly remove the subjectivity of the rubrics in the process of grading a CM. We evaluate our framework against a predefined rubric and test it with CM data collected from the Introduction to Computer Security course at the University of New Orleans (UNO), and found that the scores obtained via MAnanA captured the trend that we observed from the rubric via peak matching. Based on our evaluation, we believe that our framework can be used to objectify CM analysis.