• Refine Query
  • Source
  • Publication year
  • to
  • Language
  • 6
  • 2
  • Tagged with
  • 8
  • 8
  • 5
  • 4
  • 4
  • 4
  • 4
  • 3
  • 3
  • 3
  • 3
  • 3
  • 2
  • 2
  • 2
  • About
  • The Global ETD Search service is a free service for researchers to find electronic theses and dissertations. This service is provided by the Networked Digital Library of Theses and Dissertations.
    Our metadata is collected from universities around the world. If you manage a university/consortium/country archive and want to be added, details can be found on the NDLTD website.
1

On improving the ease of use of the software transactional memory abstraction / Faciliter l'utilisation des mémoires transactionnelles logicielles

Crain, Tyler 06 March 2013 (has links)
Les architectures multicœurs changent notre façon d'écrire des programmes. L'écriture de programmes concurrents est bien connue pour être difficile. Traditionnellement, l'utilisation de verrous (locks) permettant au code de s'exécuter en exclusion mutuelle, a été l'abstraction la plus largement utilisée pour l'écriture des programmes concurrents. Malheureusement, il est difficile d'écrire des programmes concurrents efficaces et corrects reposant sur des verrous. En outre, les verrous présentent d'autres problèmes, notamment celui du passage à l'échelle. Le concept de mémoire transactionnelle a été proposé comme une solution à ces difficultés. Les transactions peuvent être considérées comme une abstraction de haut niveau, ou une méthodologie pour l'écriture de programmes concurrents, ce qui permet au programmeur de pouvoir déclarer des sections de code devant être exécutés de façon atomique, sans avoir à se soucier des détails de synchronisation. Malheureusement, bien qu'assurément plus facile à utiliser que les verrous, la mémoire transactionnelle souffre encore de problèmes de performance et de facilité d'utilisation. En fait, de nombreux concepts relatifs à l'utilisation et à la sémantique des transactions n'ont pas encore des normes convenues. Cette thèse propose de nouvelles solutions permettant de faciliter l'utilisation des mémoires transactionellles. La thèse débute par un chapitre qui donne un bref aperçu de la mémoire transactionnelle logicielle (STM) ainsi qu'une discussion sur le problème de la facilité d'utilisation. Les contributions à la recherche sont ensuite divisées en quatre chapitres principaux, chacun proposant une approche différente afin de rendre les STMs plus facile à utiliser. / Multicore architectures are changing the way we write programs. Writing concurrent programs is well known to be difficult task. Traditionally, the use of locks allowing code to execute in mutual exclusion has been the most widely used abstraction to write concurrent programs. Unfortunately, using locks it is difficult to write correct concurrent programs that perform efficiently. Additionally, locks present other problems such as scalability issues. Transactional memory has been proposed as a possible promising solution to these difficulties of writing concurrent programs. Transactions can be viewed as a high level abstraction or methodology for writing concurrent programs, allowing the programmer to be able to declare what sections of his code should be executed atomically, without having to worry about synchronization details. Unfortunately, although arguably easier to use then locks, transactional memory still suffers from performance and ease of use problems. In fact many concepts surrounding the usage and semantics of transactions have no widely agreed upon standards. This thesis specifically focuses on these ease of use problems by discussing how previous research has dealt with them and proposing new solutions putting ease of use first. The thesis starts with a chapter giving a brief overview of software transactional memory (STM) as well as a discussion of the problem of ease of use that is focused on in the later chapters. The research contributions are then divided into four main chapters, each looking at different approaches working towards making transactional memory easier to use.
2

Faciliter l'utilisation des mémoires transactionnelles logicielles

Crain, Tyler 06 March 2013 (has links) (PDF)
Les architectures multicœurs changent notre façon d'écrire des programmes. L'écriture de programmes concurrents est bien connue pour être difficile. Traditionnellement, l'utilisation de verrous (locks) permettant au code de s'exécuter en exclusion mutuelle, a été l'abstraction la plus largement utilisée pour l'écriture des programmes concurrents. Malheureusement, il est difficile d'écrire des programmes concurrents efficaces et corrects reposant sur des verrous. En outre, les verrous présentent d'autres problèmes, notamment celui du passage à l'échelle. Le concept de mémoire transactionnelle a été proposé comme une solution à ces difficultés. Les transactions peuvent être considérées comme une abstraction de haut niveau, ou une méthodologie pour l'écriture de programmes concurrents, ce qui permet au programmeur de pouvoir déclarer des sections de code devant être exécutés de façon atomique, sans avoir à se soucier des détails de synchronisation. Malheureusement, bien qu'assurément plus facile à utiliser que les verrous, la mémoire transactionnelle souffre encore de problèmes de performance et de facilité d'utilisation. En fait, de nombreux concepts relatifs à l'utilisation et à la sémantique des transactions n'ont pas encore des normes convenues. Cette thèse propose de nouvelles solutions permettant de faciliter l'utilisation des mémoires transactionellles. La thèse débute par un chapitre qui donne un bref aperçu de la mémoire transactionnelle logicielle (STM) ainsi qu'une discussion sur le problème de la facilité d'utilisation. Les contributions à la recherche sont ensuite divisées en quatre chapitres principaux, chacun proposant une approche différente afin de rendre les STMs plus facile à utiliser.
3

Data structures for current multi-core and future many-core architectures / Structures de données pour des architectures multi-cœur actuelles et de futures architectures many-cœur

Kanellou, Eleni 14 December 2015 (has links)
Actuellement, la majorité des architectures de processeurs sont fondées sur une mémoire partagée avec cohérence de caches. Des prototypes intégrant de grandes quantités de cœurs, reliés par une infrastructure de transmission de messages, indiquent que, dans un proche avenir, les architectures de processeurs vont probablement avoir ces caractéristiques. Ces deux tendances exigent que les processus s'exécutent en parallèle et rendent la programmation concurrente nécessaire. Cependant, la difficulté inhérente du raisonnement sur la concurrence peut rendre ces nouvelles machines difficiles à programmer. Nous explorons trois approches ayant pour but de faciliter la programmation concurrente. Nous proposons WFR-TM, une approche fondé sur la mémoire transactionnelle (TM), un paradigme de programmation concurrente qui utilise des transactions afin de synchroniser l'accès aux données partagées. Une transaction peut soit terminer (commit), rendant visibles ses modifications, soit échouer (abort), annulant toutes ses modifications. WFR-TM tente de combiner des caractéristiques désirables des TM optimistes et pessimistes. Une TM pessimiste n'échoue jamais aucune transaction; néanmoins les algorithmes existants utilisent des verrous pour exécuter de manière séquentielle les transactions qui contiennent des opérations d'écriture. Les algorithmes TM optimistes exécutent toutes les transactions en parallèle mais les terminent seulement si elles n'ont pas rencontré de conflit au cours de leur exécution. WFR-TM fournit des transactions en lecture seule qui sont wait-free, sans jamais exécuter d'opérations de synchronisation coûteuse (par ex. CAS, LL\SC, etc) ou sacrifier le parallélisme entre les transactions d'écriture. Nous présentons également Dense, une implémentation concurrente de graphe. Les graphes sont des structures de données polyvalentes qui permettent la mise en oeuvre d'une variété d'applications. Cependant, des applications multi-processus qui utilisent des graphes utilisent encore largement des versions séquentielles. Nous introduisons un nouveau modèle de graphes concurrents, permettant l'ajout ou la suppression de n'importe quel arc du graphe, ainsi que la traversée atomique d'une partie (ou de l'intégralité) du graphe. Dense offre la possibilité d'effectuer un snapshot partiel d'un sous-ensemble du graphe défini dynamiquement. Enfin, nous ciblons les futures architectures. Dans l'intérêt de la réutilisation du code il existe depuis quelques temps une tentative d'adaptation des environnements d'exécution de logiciel - comme par ex. JVM, l'environnement d'exécution de Java - initialement prévus pour mémoire partagée, à des machines sans cohérence de caches. Nous étudions des techniques générales pour implémenter des structures de données distribuées en supposant qu'elles vont être utilisées sur des architectures many-core, qui n'offrent qu'une cohérence partielle de caches, voir pas de cohérence du tout. / Though a majority of current processor architectures relies on shared, cache-coherent memory, current prototypes that integrate large amounts of cores, connected through a message-passing substrate, indicate that architectures of the near future may have these characteristics. Either of those tendencies requires that processes execute in parallel, making concurrent programming a necessary tool. The inherent difficulty of reasoning about concurrency, however, may make the new processor architectures hard to program. In order to deal with issues such as this, we explore approaches for providing ease of programmability. We propose WFR-TM, an approach based on transactional memory (TM), which is a concurrent programming paradigm that employs transactions in order to synchronize the access to shared data. A transaction may either commit, making its updates visible, or abort, discarding its updates. WFR-TM combines desirable characteristics of pessimistic and optimistic TM. In a pessimistic TM, no transaction ever aborts; however, in order to achieve that, existing TM algorithms employ locks in order to execute update transactions sequentially, decreasing the degree of achieved parallelism. Optimistic TMs execute all transactions concurrently but commit them only if they have encountered no conflict during their execution. WFR-TM provides read-only transactions that are wait-free, without ever executing expensive synchronization operations (like CAS, LL/SC, etc), or sacrificing the parallelism between update transactions. We further present Dense, a concurrent graph implementation. Graphs are versatile data structures that allow the implementation of a variety of applications. However, multi-process applications that rely on graphs still largely use a sequential implementation. We introduce an innovative concurrent graph model that provides addition and removal of any edge of the graph, as well as atomic traversals of a part (or the entirety) of the graph. Dense achieves wait-freedom by relying on light-weight helping and provides the inbuilt capability of performing a partial snapshot on a dynamically determined subset of the graph. We finally aim at predicted future architectures. In the interest of ode reuse and of a common paradigm, there is recent momentum towards porting software runtime environments, originally intended for shared-memory settings, onto non-cache-coherent machines. JVM, the runtime environment of the high-productivity language Java, is a notable example. Concurrent data structure implementations are important components of the libraries that environments like these incorporate. With the goal of contributing to this effort, we study general techniques for implementing distributed data structures assuming they have to run on many-core architectures that offer either partially cache-coherent memory or no cache coherence at all and present implementations of stacks, queues, and lists.
4

Structured interactive scores : from a structural description of a multimedia scenario to a real-time capable implementation with formal semantics / Partitions interactives structurées

Toro-Bermudez, Mauricio 25 September 2012 (has links)
La plupart des scénarios multimédia interactifs sont basés sur des spécifications informelles, il n'est donc pas possible de vérifier formellement des propriétés de ces systèmes. Nous préconisons la nécessité d'un modèle général et formel. Partitions interactives est un formalisme pour décrire des scénarios multimédia interactifs. Nous proposons une nouvelle sémantique pour les partitions interactives basée sur les structures d'événements temporisés. Avec une telle sémantique, nous pouvons spécifier des propriétés pour le système, en particulier, des propriétés sur les traces, qui sont difficiles à préciser avec la programmation par contraintes. Nous présentons également une sémantique opérationnelle des partitions interactives basée sur le calcul non-déterministe, temporisé, concurrent, par contraintes (ntcc) et nous rapportons la sémantique operationelle à la semantique en structures d'événements temporisés. Avec la sémantique opérationnelle, nous pouvons décrire formellement le comportement d'un scenario dont les durées des objets temporels peuvent être des intervalles d'entiers arbitraires. La sémantique opérationnelle est obtenue à partir de la sémantique en structures d'événements temporisés de la partition interactive. Pour fournir une telle traduction, nous avons d'abord défini la forme normale d'une structure d'événements temporisés, dans laquel les événements liés avec une durée zéro sont regroupés en un seul. Nous avons également défini la notion de structures d'événements temporisés répartissables, de telle sorte que son graphe de contraintes peut être expédié en se fondant uniquementsur la propagation locale. Nous croyons que la sémantique opérationnelle basée sur ntcc offre certains avantages par rapport à la sémantique des partitions interactives basée sur des réseaux de Petri; par exemple, les durées des objets temporels peuvent être des intervalles d'entiers arbitraires, tandis que dans la plupart des modèles de partitions interactives, les intervalles ne peut être utilisés que pour représenterles relations telles que l'égalité et les inégalités. Nos modèles ntcc de partitions interactives sont exécutés en utilisant Ntccrt, un interprète temps réel pour ntcc. Nos modèles peuvent également être vérifiés automatiquement en utilisant ntccMC, un vérificateur pour ntcc, de temps borné, basée sur les automates finis, que nous introduisons dans cette thèse. En utilisant ntccMC, nous pouvons vérifier des propriétés de logique de temps linéaire avec des contrantes (CLTL). Dans cette thèse, nous introduisons deux extensions du formalisme de partitions interactives:(1) l'une pour gérer le traitement audio en utilisant le langage de programmation français Faustet (2) l'autre pour traiter des condition et des branchements, permettant de spécifier des choix et des boucles. Pour la première extension, nous présentons une sémantique basée sur les structures d'événements temporisés et des idées sur la façon de définir une sémantique opérationnelle. Pour la deuxième extension, nous présentons une mise en oeuvre et la comparaison des résultats du jitter relative moyenne d'une implémentation d'un arpège base sur l'algorithme de Karplus-Strong par rapport aux implémentations existants écrits dans Pure Data. Nous définissons aussi un format de sauvegarde XML pour les partitions interactives et pour la extension avec branchement conditionnel. Un format de sauvegarde est crucial pour assurer la persistance des partitions. / Technology has shaped the way on which we compose and produce music. Notably, the invention of microphones and computers pushed the development of new music styles in the 20th century. In fact, several artistic domains have been benefiting from such technology developments ; for instance, Experimental music, non-linear multimedia, Electroacoustic music, and interactive multimedia. In this dissertation, we focus on interactive multimedia.Interactive multimedia deals with the design of scenarios where multimedia content and interactive events are handled by computer programs. Examples of such scenarios are multimedia art installations, interactive museum exhibitions, some Electroacoustic music pieces, and some Experimental music pieces. Unfortunately, most interactive multimedia scenarios are based on informal specifications, thus it is not possible to formally verify properties of such systems. We advocate the need of a general and formal model. Interactive scores is a formalism to describe interactive multimedia scenarios. We propose new semantics for interactive scores based on timed eventstructures. With such a semantics, we can specify properties for the system, in particular, properties about traces, which are difficult to specify as constraints. In fact, constraints are an important part of the semantic model of interactive scores because the formalism is based on temporal constraints among the objects of the scenario. We also present an operational semantics of interactive scores based on the non-deterministic timed concurrent constraint (ntcc) calculus and we relate such a semantics to the timed event structures semantics. With the operational semantics, we formally describe the behavior of a score whose temporal object durations can be arbitrary integer intervals. The operational semantics is obtained from the timed event structures semantics of the score. To provide such a translation, we first define the normal form of a timed event structure in which events related with zero-duration delays are collapsed into a single one. We also define the notion of dispatchable timed event structures. Event structures such that its constraint graph can be dispatched by relying only on local propagation.We believe that operational semantics in ntcc offers some advantages over existing Petri nets semantics for interactive scores; for instance, the duration of the temporal objects can be arbitrary integer intervals, whereas inprevious models of interactive scores, such durations can only be intervals to represent equalities and inequalities. In this dissertation, we also introduce two extensions of the formalism of interactive scores : (1) one to handle audio processing using the Fast AUdio Stream (Faust) languageand (2) another one to handle conditional branching, allowing designers to specify choices and loops. For the first extension, we present a timed event structures semantics and ideas on how to define operational semantics. For the second extension, we present an implementation and results comparing the average relative jitter of an implementation ofan arpeggio based on Karplus-Strong with respect to existing implementations of Karplus written in Pure Data. We also define a XML file format for interactive scores and for the conditional branching extension. A file format is crucial to assure the persistence of the scores. Ntcc models of interactive scores are executed using Ntccrt, a real-time capable interpreter for ntcc. They can also be verified automatically using ntccMC, a bounded-time automata based model checker for ntcc which we introduce in this dissertation. Using ntccMC, we can verify properties expressed on constraint linear-time logic. Ntcc has been used in the past, not only for multimedia interaction models, but alsofor system biology, security protocols and robots.
5

Conception et mise en oeuvre d'un système déclaratif de géométrie dynamique

Channac, Stéphane 07 June 1999 (has links) (PDF)
Cette thèse a pour objet de montrer la faisabilité d'un système de "géométrie dynamique déclarative". Un tel système, GDRev (pour Géométrie Déclarative Réversible) a été conçu et réalisé, dans l'optique de l'enseignement de la géométrie. D'un point de vue conceptuel, GDRev repose sur la définition d'un langage logique, ELDL (pour Extented Logical Description Language), pour l'expression de spécifications de "figures" (l'objet mathématique sous-jacent à un dessin) : il intègre la possibilité de spécifications modulaires et récursives, via l'usage de "clauses". Au niveau dessin, GDRev est pourvu d'un langage de construction et d'animation dont la sémantique est définie à l'aide de ELDL. l'interface, qui peut être vu comme une extension déclarative de celle de Cabri-Géomètre, doit assurer, d'une façon originale, d'une part des fonctionnalités équivalentes par manipulation directe sur la figure et sur le dessin, d'autre part un invariant imposant la cohérence temporelle entre figure et dessin. D'un point de vue algorithmique, GDRev résout les contraintes géométriques par "coopération de solveurs" reposant sur un schéma de "programmation concurrente avec contraintes". Trois résolveurs généraux (linéaires, quadratiques, intervalle) coopèrent avec trois résolveurs spécifiques et originaux : complétion d'objets (créant automatiquement des objets), complétion de propriétés (ajoutant automatiquement des propriétés redondantes à la figure), règle et compas (calculant une construction optimisée de la figure pour l'animation du dessin). D'un point de vue pratique, GDRev est réalisé par interopérabilité entre les interfaces écrites en Visual C++ et le résolveur de contraintes géométriques écrit en Prolog IV. Les expérimentations réalisées ont donné des résultats encourageants en particulier en ce qui concerne le choix des heuristiques utilisées.
6

Continuation-Passing C : Transformations de programmes pour compiler la concurrence dans un langage impératif

Kerneis, Gabriel 09 November 2012 (has links) (PDF)
La plupart des programmes informatiques sont concurrents : ils doivent effectuer plusieurs tâches en même temps. Les threads et les événements sont deux techniques usuelles d'implémentation de la concurrence. Les événements sont généralement plus légers et efficaces que les threads, mais aussi plus difficiles à utiliser. De plus, ils sont souvent trop limités ; il est alors nécessaire d'écrire du code hybride, encore plus complexe, utilisant à la fois des threads ordonnancés préemptivement et des événements ordonnancés coopérativement. Nous montrons dans cette thèse que des programmes concurrents écrits dans un style à threads sont traduisibles automatiquement en programmes à événements équivalents et efficaces par une suite de transformations source-source prouvées. Nous proposons d'abord Continuation-Passing C, une extension du langage C pour l'écriture de systèmes concurrents qui offre des threads très légers et unifiés (coopératifs et préemptifs). Les programmes CPC sont transformés par le traducteur CPC pour produire du code à événements séquentialisé efficace, utilisant des threads natifs pour les parties préemptives. Nous définissons et prouvons ensuite la correction de ces transformations, en particulier le lambda lifting et la conversion CPS, pour un langage impératif. Enfin, nous validons la conception et l'implémentation de CPC en le comparant à d'autres bibliothèques de threads et en exhibant notre seeder BitTorrent Hekate. Nous justifions aussi notre choix du lambda lifting en implémentant eCPC, une variante de CPC utilisant les environnements, et en comparant ses performances à celles de CPC.
7

Etude de la programmation logico-fonctionnelle concurrente

Serwe, Wendelin 15 March 2002 (has links) (PDF)
La construction de programmes nécessite l'utilisation d'outils adaptés. Un outil particulier est le langage de programmation. Les langages logico-fonctionnels sont des langages de programmation dits déclaratifs qui se basent sur les notions mathématiques de fonction et de prédicat. Ce fondement théorique solide facilite à la fois la description d'un système à un niveau proche de la spécification ainsi que la validation de programmes. Néanmoins, les concepts sous-jacents aux langages logico-fonctionnels sont insuffisants pour la description aisée de systèmes complexes qui nécessitent l'interactivité, la concurrence et la distribution. Pour la modélisation de ces systèmes, la notion de processus a été introduite. Dans le contexte des algèbres de processus, un processus est caractérisé par les actions qu'il est capable d'exécuter. Cependant, les langages fondés uniquement sur les algèbres de processus doivent être étendus afin d'éviter le codage de fonctions et de prédicats en termes de processus. Dans cette thèse nous proposons un modèle de calcul qui intègre la programmation concurrente et déclarative. Nous suggérons de modéliser un système par un ensemble de composants. Chacun de ces composants comporte un programme déclaratif, appelé store, et un ensemble de processus interagissant par l'exécution d'actions. De plus, un composant peut contenir de nouvelles actions définissables par le programmeur. L'interaction entre composants est fondée sur le même principe, c.-à.-d. un processus peut exécuter des actions sur les stores des autres composants. Les différents composants d'un système peuvent utiliser des langages déclaratifs différents pour la description de leurs stores respectifs, ce qui nécessite la traduction des valeurs communiquées. Nous donnons une sémantique compositionnelle ainsi qu'une analyse de la confidentialité pour les processus d'un composant, et présentons les principes d'un prototype implanté
8

Using Event-Based and Rule-Based Paradigms to Develop Context-Aware Reactive Applications / Programmation événementielle et programmation à base de règles pour le développement d'applications réactives sensibles au contexte

Le, Truong Giang 30 September 2013 (has links)
Les applications réactives et sensibles au contexte sont des applications intelligentes qui observent l’environnement (ou contexte) dans lequel elles s’exécutent et qui adaptent, si nécessaire, leur comportement en cas de changements dans ce contexte, ou afin de satisfaire les besoins ou d'anticiper les intentions des utilisateurs. La recherche dans ce domaine suscite un intérêt considérable tant de la part des académiques que des industriels. Les domaines d'applications sont nombreux: robots industriels qui peuvent détecter les changements dans l'environnement de travail de l'usine pour adapter leurs opérations; systèmes de contrôle automobiles pour observer d'autres véhicules, détecter les obstacles, ou surveiller le niveau d'essence ou de la qualité de l'air afin d'avertir les conducteurs en cas d'urgence; systèmes embarqués monitorant la puissance énergétique disponible et modifiant la consommation en conséquence. Dans la pratique, le succès de la mise en œuvre et du déploiement de systèmes sensibles au contexte dépend principalement du mécanisme de reconnaissance et de réaction aux variations de l'environnement. En d'autres termes, il est nécessaire d'avoir une approche adaptative bien définie et efficace de sorte que le comportement des systèmes peut être modifié dynamiquement à l'exécution. En outre, la concurrence devrait être exploitée pour améliorer les performances et la réactivité des systèmes. Tous ces exigences, ainsi que les besoins en sécurité et fiabilité constituent un grand défi pour les développeurs.C’est pour permettre une écriture plus intuitive et directe d'applications réactives et sensibles au contexte que nous avons développé dans cette thèse un nouveau langage appelé INI. Pour observer les changements dans le contexte et y réagir, INI s’appuie sur deux paradigmes : la programmation événementielle et la programmation à base de règles. Événements et règles peuvent être définis en INI de manière indépendante ou en combinaison. En outre, les événements peuvent être reconfigurésdynamiquement au cours de l’exécution. Un autre avantage d’INI est qu’il supporte laconcurrence afin de gérer plusieurs tâches en parallèle et ainsi améliorer les performances et la réactivité des programmes. Nous avons utilisé INI dans deux études de cas : une passerelle M2M multimédia et un programme de suivi d’objet pour le robot humanoïde Nao. Enfin, afin d’augmenter la fiabilité des programmes écrits en INI, un système de typage fort a été développé, et la sémantique opérationnelle d’INI a été entièrement définie. Nous avons en outre développé un outil appelé INICheck qui permet de convertir automatiquement un sous-ensemble d’INI vers Promela pour permettre un analyse par model checking à l’aide de l’interpréteur SPIN. / Context-aware pervasive computing has attracted a significant research interest from both academy and industry worldwide. It covers a broad range of applications that support many manufacturing and daily life activities. For instance, industrial robots detect the changes of the working environment in the factory to adapt their operations to the requirements. Automotive control systems may observe other vehicles, detect obstacles, and monitor the essence level or the air quality in order to warn the drivers in case of emergency. Another example is power-aware embedded systems that need to work based on current power/energy availability since power consumption is an important issue. Those kinds of systems can also be considered as smart applications. In practice, successful implementation and deployment of context-aware systems depend on the mechanism to recognize and react to variabilities happening in the environment. In other words, we need a well-defined and efficient adaptation approach so that the systems' behavior can be dynamically customized at runtime. Moreover, concurrency should be exploited to improve the performance and responsiveness of the systems. All those requirements, along with the need for safety, dependability, and reliability pose a big challenge for developers.In this thesis, we propose a novel programming language called INI, which supports both event-based and rule-based programming paradigms and is suitable for building concurrent and context-aware reactive applications. In our language, both events and rules can be defined explicitly, in a stand-alone way or in combination. Events in INI run in parallel (synchronously or asynchronously) in order to handle multiple tasks concurrently and may trigger the actions defined in rules. Besides, events can interact with the execution environment to adjust their behavior if necessary and respond to unpredictable changes. We apply INI in both academic and industrial case studies, namely an object tracking program running on the humanoid robot Nao and a M2M gateway. This demonstrates the soundness of our approach as well as INI's capabilities for constructing context-aware systems. Additionally, since context-aware programs are wide applicable and more complex than regular ones, this poses a higher demand for quality assurance with those kinds of applications. Therefore, we formalize several aspects of INI, including its type system and operational semantics. Furthermore, we develop a tool called INICheck, which can convert a significant subset of INI to Promela, the input modeling language of the model checker SPIN. Hence, SPIN can be applied to verify properties or constraints that need to be satisfied by INI programs. Our tool allows the programmers to have insurance on their code and its behavior.

Page generated in 0.1724 seconds