International Professional University of Technology in Nagoya Repository
Not a member yet
15131 research outputs found
Sort by
Détection de liens d'identité contextuels dans une base de connaissances.
No full textNational audienceDe nombreuses applications du Web de données exploitent des liens d'identités déclarés à l'aide du constructeur owl :sameAs. Cependant, différentes études ont montré qu'une utilisation abusive de ces liens peut conduire à des inférences erronées ou contradictoires. Dans ce papier nous proposons de calculer des liens d'identités contextuels qui permettent d'expliciter les contextes dans lesquels ces liens sont valides. La notion de contexte que nous proposons est représentée en se basant sur l'ontologie de domaine dans laquelle les instances sont représentées. Nous avons expérimenté cette approche dans le domaine des données scientifiques où les éléments décrivant les expériences partagent rarement un lien d'identité tel que défini par owl :sameAs
Schedulability analysis of dependent probabilistic real-time tasks
No full textInternational audienceThe complexity of modern architectures has increased the timing variability of programs (or tasks). In this context, new approaches based on probabilistic methods are proposed to decrease the pessimism by associating probabilities to the worst case values of the programs (tasks) time execution. In this paper, we extend the original work of Chetto et al. [7] on precedence constrained tasks to the case of tasks with worst case execution times described by probability distributions. The precedence constraints between tasks are defined by acyclic directed graphs and these constraints are transformed in appropriate release times and deadlines. The new release times and deadlines are built using new maximum and minimum relations between pairs of probability distributions. We provide a probabilistic schedulability condition based on these new relations
Report on the 1 st International Workshop on Debugging in Model-Driven Engineering (MDEbug'17)
No full textInternational audienceSystem developers spend a significant part of their time debugging systems (i.e., locating and fixing the cause of failures observed through verification and validation (V&V)). While V&V techniques are commonly used in model-driven engineering, locating and fixing the cause of a failure in a modelled system is most often still a manual task without tool-support. Although debugging techniques are well-established for programming languages, only a few debugging techniques and tools for models have been proposed. Debugging models faces various challenges: handling a wide variety of models and modelling languages; adapting debugging techniques initially proposed for programming languages; tailoring debugging approaches for the domain expert using the abstractions of the considered language. The aim of the first edition of the MDEbug workshop was to bring together researchers wanting to contribute to the emerging field of debugging in model-driven engineering by discussing new ideas and compiling a research agenda. This paper summarizes the workshop's discussion session and distils a list of challenges that should be addressed in future research
Engineering the Structural Nonlinearity Using Multimodal-Shaped Springs in MEMS
No full textInternational audienc
Structurer un interpréteur abstrait au moyen d'abstractions de valeurs et d'états :Eva, une analyse de valeur évoluée pour Frama-C
No full textThe formal verification of programs is nowadays a crucial challenge for computer science, as software bugs in critical systems may lead to catastrophic outcomes. Abstract interpretation is a general theory of approximation of the semantics of programming languages, practically used to detect errors in programs. Automatic analyses can be derived by computing an over-approximation of the possible behaviors of a program, through abstractions of its concrete semantics.This thesis proposes a new framework for the combination of multiple abstractions in the abstract interpretation theory. Its core concept is the structuring of the abstract semantics by following the usual distinction between expressions and statements. This can be achieved by a convenient architecture where abstractions are separated in two layers: value abstractions, in charge of the expression semantics, and state abstractions (or abstract domains), in charge of the statement semantics.This design leads naturally to an elegant communication system where the abstract states, when interpreting a statement, interact and exchange information through abstract values, that express properties about expressions. While the values form the communication interface between states, they are also standard elements of the abstract interpretation framework. The communication system is thus embedded in the abstract semantics, and the usual tools of abstract interpretation apply naturally to value abstractions. For instance, different kinds of value abstractions can be composed through the existing methods of combination of abstractions, enabling even further interaction between the components of the abstract semantics.This thesis explores the possibilities offered by this framework. We discuss efficient strategies to compute precise value abstractions from the properties inferred by abstract domains, and illustrate the means of communication between different state abstractions. Our architecture also features a direct collaboration for the emission of alarms that report the possible errors of a program.The general system of abstractions combination has been implemented within EVA, the new version of the abstract interpreter provided by the Frama-C platform. Thus, EVA enjoys a modular and extensible architecture designed to facilitate the introduction of new abstractions and to enable rich interactions between them. Thanks to this work, five new domains from the literature have been implemented in less than a year, enhancing both the scope and the precision of the analyzer.La vérification formelle de programmes est devenue un enjeu majeur de l'informatique, à l'heure où des erreurs logicielles dans des systèmes critiques peuvent avoir des conséquences dramatiques. L'interprétation abstraite est une théorie générale d'approximation des sémantiques des langages de programmation, qui permet des analyses automatiques de programmes pour en détecter de façon certaine les comportements indésirables. Ces analyses reposent sur des abstractions d'une sémantique concrète, qui calculent une sur-approximation des comportements possibles d'un programme.Cette thèse propose une nouvelle technique de composition modulaire entre les abstractions d'un interpréteur abstrait. L'idée principale en est l'organisation d'une sémantique abstraite suivant la distinction usuelle entre expressions et instructions. Les abstractions sont alors séparées entre abstractions de valeurs, en charge de la sémantique des expressions, et les abstractions d'états (ou domaines abstraits), en charge de la sémantique des instructions.Cette adéquate hiérarchie guide les interactions entre abstractions durant l'analyse. Lors de l'interprétation d'une instruction, les états abstraits peuvent échanger des informations au moyen de valeurs abstraites, qui expriment des propriétés sur les expressions. Ces valeurs abstraites forment donc l'interface de communication entre les domaines, mais sont également des éléments canoniques de l'interprétation abstraite. Les outils standards de la théorie s'appliquent donc naturellement aux abstractions de valeurs. En particulier, elles peuvent elle-mêmes être composées par les techniques existantes, ouvrant la voie à plus d'interactions encore.Cette thèse explore les possibilités offertes par cette nouvelle architecture des sémantiques abstraites. Elle décrit en particulier des stratégies efficaces pour le calcul de valeurs abstraites précises à partir des propriétés inférées par les domaines, et illustre les différents moyens d’interactions que ce système offre. Notre architecture comprend également une collaboration directe des différentes abstractions à l'émission des alarmes qui signalent les erreurs possibles d'un programme. Ce système de composition des abstractions a été mis en œuvre dans EVA, la nouvelle version de l'interpréteur abstrait de la plateforme Frama-C. EVA a été spécifiquement conçu pour faciliter l’introduction de nouvelles abstractions, et permettre des interactions riches entre ces abstractions. Grâce à son architecture modulaire et extensible, cinq nouveaux domaines abstraits ont pu être introduits dans l’analyseur en moins d’un an, améliorant ainsi tant ses capacités que sa précision
Quantification in Frame Semantics with Binders and Nominals of Hybrid Logic
No full textInternational audienceThis paper aims at integrating logical operators into frame-based semantics. Frames are semantic graphs that allow to capture lexical meaning in a fine-grained way but that do not come with a natural way to integrate logical operators such as quantifiers. The approach we propose starts from the observation that modal logic is a powerful tool for describing relational structures, hence frames. We use its hybrid logic extension in order to incorporate quantification and thereby allow for inference and reasoning. We integrate our approach to a type theoretic compositional semantics, formulated within Abstract Categorial Grammars. We also show how the key ingredients of hybrid logic, nominals and binders, can be used to model semantic coercion, such as the one induced by the begin predicate. In order to illustrate the effectiveness of the proposed syntax-semantics interface, all the examples can be run and tested with the Abstract Categorial Grammar development toolkit
ASAP.V2 and ASAP.V3: Sequential optimization of an Algorithm Selector and a Scheduler
No full textInternational audienceAlgorithm portfolios are known to offer robust performances, efficiently overcoming the weakness of every single algorithm on some particular problem instances. The presented ASAP system relies on the alternate optimization of two complementary portfolio approaches , namely a sequential scheduler and a per-instance algorithm selector
A hierarchy of proof rules for checking positive invariance of algebraic and semi-algebraic sets
No full textInternational audienceThis paper studies sound proof rules for checking positive invariance of algebraic and semi-algebraic sets, that is, sets satisfying polynomial equalities and those satisfying finite boolean combinations of polynomial equalities and inequalities, under the flow of polynomial ordinary differential equations. Problems of this nature arise in formal verification of continuous and hybrid dynamical systems, where there is an increasing need for methods to expedite formal proofs. We study the trade-off between proof rule generality and practical performance and evaluate our theoretical observations on a set of benchmarks. The relationship between increased deductive power and running time performance of the proof rules is far from obvious; we discuss and illustrate certain classes of problems where this relationship is interesting
On the topological semigroup of equational classes of finite functions under composition
No full textInternational audienceWe consider the set of equational classes of finite functions endowed with the operation of class composition. Thus defined, this set gains a semigroup structure. This paper is a contribution to the under-standing of this semigroup. We present several interesting properties of this semigroup. In particular, we show that it constitutes a topological semigroup that is profinite and we provide a description of its regular elements in the Boolean case
Stabilization of MISO fractional systems with delays
No full textInternational audienceWe consider multi-input single-output (MISO) fractional systems of commensurate fractional orders with different input or output delays. We derive explicit expressions of left and right coprime factorizations over H∞ and of the associated Bézout factors of the transfer matrix of the systems. These factors allow the construction of the Youla-Kučera parametrization of the set of stabilizing controllers which guarantee the internal stability of the closed-loop systems