En éducation, on constate un besoin de mettre à profit l’évolution continue des technologies de l'information et des communications pour développer de nouvelles applications. Ainsi, un nouveau type d'apprentissage à distance a été créé. Il s'agit de l'apprentissage mobile qui peut fournir aux apprenants l'autonomie d'apprentissage maximale. De plus, il offre aux autres acteurs du processus d'apprentissage, comme les enseignants et les gestionnaires, des méthodes plus souples d'enseignement et de gestion. Malgré sa croissance rapide, il existe de nombreux problèmes qui doivent être résolus afin que cette forme d'apprentissage puisse prendre sa place dans les systèmes de formation utilisant la technologie. L'inconvénient majeur de l'apprentissage mobile est l'absence de standard ainsi que le manque de prise de conscience sur la façon dont il peut être bien intégré dans le processus d'apprentissage. Le défi le plus critique est la formulation d'un standard qui décrit le développement d'un système efficace d'apprentissage mobile et la définition précise de ses acteurs et de ses composants. L'objectif principal de cette thèse était de formaliser un modèle global et générique pour l'apprentissage mobile afin de bien comprendre ses divers composants et aussi pour guider les chercheurs ultérieurs dans le domaine de l'apprentissage mobile. La méthodologie d'ingénierie des connaissances, CommonKADS, a été employée pour aider à réaliser les objectifs de recherche. La modélisation proposée consiste en trois étapes consécutives, contexte, concept et artefact, et est illustrée par une expérience réelle d'apprentissage mobile au niveau universitaire. Les résultats montrent comment appliquer les modèles proposés pour concevoir une application d’apprentissage mobile et permettent de vérifier la possibilité d’intégrer une telle application dans un processus d’apprentissage formel. Cette thèse fait le lien entre la description théorique d’applications d’apprentissage mobile et leur mise en œuvre. Chaque modèle proposé peut être considéré en soi comme un exemple. Leurs descriptions génériques peuvent servir de point de départ pour de plus amples recherches, pouvant facilement s’adapter aux futures évolutions des appareils mobiles. / In education, the need to get the maximum benefit from recent development of computer and telecommunications technologies arises. A new kind of distance education mode i.e. mobile learning has been emerged. Mobile learning can provide learners with the maximum learning autonomy. It can also provide the other players in the learning process such as instructors and learning administrators with more flexible teaching and managing methods. Despite of the fact that m-learning is a fast growing technology, it faces many problems which have to be solved in order to allow it taking its rightful place in the field of technology-based learning. The main m-learning drawback is the absence of standard in addition to the lack of awareness about how it can be well integrated in the learning process. The most critical challenge facing us is the formulation of a standard describing how to develop an efficient m-learning system and how to define its actors and components precisely. The principal objective of this dissertation is to formalize a generic comprehensive model for m-learning in order to understand the m-learning different components and also to guide subsequent researchers in the m-learning domain. CommonKADS knowledge engineering methodology is employed in order to help in realizing the research objectives. The proposed modeling process goes through three consecutive stages; context, concept, and artifact modeling. Afterwards, it is illustrated by a real m-learning experience at higher education level. Results show how to apply the proposed models in order to design an entire mobile learning system and to verify the possibility to integrate that system in a formal learning process. This dissertation constructs the link between the theoretic description of mobile learning and its implementation. Each model can be considered as a standalone reference. Furthermore, the generic description of the proposed models represent a good starting point for further research, and can also be adapted with future evolutions in mobile and telecommunication technologies.

Tableau d'honneur de la Faculté des études supérieures et postdorales, 2014-2015 / L’apprentissage automatique correspond à la science de l’apprentissage à partir d’exemples. Des algorithmes basés sur cette approche sont aujourd’hui omniprésents. Bien qu’il y ait eu un progrès significatif, ce domaine présente des défis importants. Par exemple, simplement sélectionner la fonction qui correspond le mieux aux données observées n’offre aucune garantie statistiques sur les exemples qui n’ont pas encore été observées. Quelques théories sur l’apprentissage automatique offrent des façons d’aborder ce problème. Parmi ceux-ci, nous présentons la modélisation bayésienne de l’apprentissage automatique et l’approche PACbayésienne pour l’apprentissage automatique dans une vue unifiée pour mettre en évidence d’importantes similarités. Le résultat de cette analyse suggère que de considérer les réponses de l’ensemble des modèles plutôt qu’un seul correspond à un des éléments-clés pour obtenir une bonne performance de généralisation. Malheureusement, cette approche vient avec un coût de calcul élevé, et trouver de bonnes approximations est un sujet de recherche actif. Dans cette thèse, nous présentons une approche novatrice qui peut être appliquée avec un faible coût de calcul sur un large éventail de configurations d’apprentissage automatique. Pour atteindre cet objectif, nous appliquons la théorie de Bayes d’une manière différente de ce qui est conventionnellement fait pour l’apprentissage automatique. Spécifiquement, au lieu de chercher le vrai modèle à l’origine des données observées, nous cherchons le meilleur modèle selon une métrique donnée. Même si cette différence semble subtile, dans cette approche, nous ne faisons pas la supposition que le vrai modèle appartient à l’ensemble de modèles explorés. Par conséquent, nous disons que nous sommes agnostiques. Plusieurs expérimentations montrent un gain de généralisation significatif en utilisant cette approche d’ensemble de modèles durant la phase de validation croisée. De plus, cet algorithme est simple à programmer et n’ajoute pas un coût de calcul significatif à la recherche d’hyperparamètres conventionnels. Finalement, cet outil probabiliste peut également être utilisé comme un test statistique pour évaluer la qualité des algorithmes sur plusieurs ensembles de données d’apprentissage. / Machine learning is the science of learning from examples. Algorithms based on this approach are now ubiquitous. While there has been significant progress, this field presents important challenges. Namely, simply selecting the function that best fits the observed data was shown to have no statistical guarantee on the examples that have not yet been observed. There are a few learning theories that suggest how to address this problem. Among these, we present the Bayesian modeling of machine learning and the PAC-Bayesian approach to machine learning in a unified view to highlight important similarities. The outcome of this analysis suggests that model averaging is one of the key elements to obtain a good generalization performance. Specifically, one should perform predictions based on the outcome of every model instead of simply the one that best fits the observed data. Unfortunately, this approach comes with a high computational cost problem, and finding good approximations is the subject of active research. In this thesis, we present an innovative approach that can be applied with a low computational cost on a wide range of machine learning setups. In order to achieve this, we apply the Bayes’ theory in a different way than what is conventionally done for machine learning. Specifically, instead of searching for the true model at the origin of the observed data, we search for the best model according to a given metric. While the difference seems subtle, in this approach, we do not assume that the true model belongs to the set of explored model. Hence, we say that we are agnostic. An extensive experimental setup shows a significant generalization performance gain when using this model averaging approach during the cross-validation phase. Moreover, this simple algorithm does not add a significant computational cost to the conventional search of hyperparameters. Finally, this probabilistic tool can also be used as a statistical significance test to evaluate the quality of learning algorithms on multiple datasets.

Tableau d’honneur de la Faculté des études supérieures et postdoctorales, 2015-2016 / En apprentissage automatique, l’approche PAC-bayésienne permet d’obtenir des garanties statistiques sur le risque de votes de majorité pondérés de plusieurs classificateurs (nommés votants). La théorie PAC-bayésienne «classique», initiée par McAllester (1999), étudie le cadre d’apprentissage inductif, sous l’hypothèse que les exemples d’apprentissage sont générés de manière indépendante et qu’ils sont identiquement distribués (i.i.d.) selon une distribution de probabilité inconnue mais fixe. Les contributions de la thèse se divisent en deux parties. Nous présentons d’abord une analyse des votes de majorité, fondée sur l’étude de la marge comme variable aléatoire. Il en découle une conceptualisation originale de la théorie PACbayésienne. Notre approche, très générale, permet de retrouver plusieurs résultats existants pour le cadre d’apprentissage inductif, ainsi que de les relier entre eux. Nous mettons notamment en lumière l’importance de la notion d’espérance de désaccord entre les votants. Bâtissant sur une compréhension approfondie de la théorie PAC-bayésienne, acquise dans le cadre inductif, nous l’étendons ensuite à deux autres cadres d’apprentissage. D’une part, nous étudions le cadre d’apprentissage transductif, dans lequel les descriptions des exemples à classifier sont connues de l’algorithme d’apprentissage. Dans ce contexte, nous formulons des bornes sur le risque du vote de majorité qui améliorent celles de la littérature. D’autre part, nous étudions le cadre de l’adaptation de domaine, dans lequel la distribution génératrice des exemples étiquetés de l’échantillon d’entraînement diffère de la distribution générative des exemples sur lesquels sera employé le classificateur. Grâce à une analyse théorique – qui se révèle être la première approche PAC-bayésienne de ce cadre d’apprentissage –, nous concevons un algorithme d’apprentissage automatique dédié à l’adaptation de domaine. Nos expérimentations empiriques montrent que notre algorithme est compétitif avec l’état de l’art. / In machine learning, the PAC-Bayesian approach provides statistical guarantees on the risk of a weighted majority vote of many classifiers (named voters). The “classical” PAC-Bayesian theory, initiated by McAllester (1999), studies the inductive learning framework under the assumption that the learning examples are independently generated and are identically distributed (i.i.d.) according to an unknown but fixed probability distribution. The thesis contributions are divided in two major parts. First, we present an analysis of majority votes based on the study of the margin as a random variable. It follows a new conceptualization of the PAC-Bayesian theory. Our very general approach allows us to recover several existing results for the inductive PAC-Bayesian framework, and link them in a whole. Among other things, we highlight the notion of expected disagreement between the voters. Building upon an improved understanding of the PAC-Bayesian theory, gained by studying the inductive framework, we then extend it to two other learning frameworks. On the one hand, we study the transductive framework, where the learning algorithm knows the description of the examples to be classified. In this context, we state risk bounds on majority votes that improve those from the current literature. On the other hand, we study the domain adaptation framework, where the generating distribution of the labelled learning examples differs from the generating distribution of the examples to be classified. Our theoretical analysis is the first PAC-Bayesian approach of this learning framework, and allows us to conceive a new machine learning algorithm for domain adaptation. Our empirical experiments show that our algorithm is competitive with other state-of-the-art algorithms.

Ce mémoire présente une nouvelle approche pour la réalisation de modèles biophysiques de neurone. Dans un premier temps, nous avons développé un modèle électrique compartimental selon le formalisme de Hodgkin-Huxley avec le logiciel NEURON. En second lieu, nous avons procédé à la réalisation de la modélisation biochimique avec des systèmes d’équations différentielles représentant des réactions d’action de masse et des réactions enzymatiques. La modélisation biochimique se fait tant dans un modèle par compartiments avec des équations différentielles ordinaires que dans un modèle spatial avec des équations différentielles partielles. VCell nous a permis de réaliser ce type de modélisation. Le modèle hybride développé présente deux points de jonction entre les formalismes des modèles électrique et biochimique pris indépendemment. Au premier point de jonction, les courants calciques calculés avec les équations de type Hodgkin-Huxley sont convertis en concentration d’ions de calcium. Ce calcium est un messager secondaire pour de nombreuses voies de signalisation cellulaire. Une élévation de la concentration de calcium modifie la dynamique des réactions biochimiques. Le deuxième point de jonction est l’impact de l’activité de kinases sur les propriétés électriques de canaux ioniques. Par la phosphorylation, certaines kinases viennent moduler la réponse électrique du neurone. En intégrant tous ces effets biophysiques et biochimiques dans une même méthodologie de modélisation, nous pouvons modéliser des processus cellulaires complexes dans les neurones. Le cross-talk synaptique est un phénomène physiologique observé, qui consiste en une augmentation de l’excitabilité membranaire suite à l’interaction entre les signaux électrique et biochimique et une communication entre les épines dendritiques du neurone. Cette interaction représente un excellent cas d’étude pour développer et valider notre méthodologie. Cette méthodologie porte sur l’interaction entre le calcium, la MAPK et les canaux KV4.2. Le calcium vient activer la MAPK par l’intermédiaire de différentes molécules. La MAPK vient ensuite phosphoryler les canaux KV4.2 qui sont possiblement responsables d’une augmentation observée de l’excitabilité membranaire. / This master’s thesis presents a new modeling technique for biophysical models of individual neurons that integrates their electrical and biochemical behaviors. First of all, we developped an electrical compartmental model. This model is based on the Hodgkin-Huxley formalism and developped in NEURON, a modeling software tool for neuroscience. Then, we developped a biochemical model. This second model is a system of differential equations based on mass action reations and enzymatic reactions. We implemented two versions of this model, one as a compartmental model with ordinary differential equations (ODE) and the other as a spatial model with partial differential equations (PDE). We used the software tool VCell for the biochemical modeling. The hybrid model combining the electrical and biochemical behaviors has two connection points between the electrical and biochemical models. At the first junction, the calcium curents calculated by the Hodgkin-Huxley equations are converted into a concentration of calcium ions. This calcium is a secondary messenger for numerous cellular signaling pathways and a rise of the calcium concentration modifies the biochemical reaction dynamic. The second junction is the kinases activity on the ionic channel electrical properties. Through phosphorylation, the kinases modulate the electrical response of the neuron. By integrating all these biophysical and biochemical effects in the same methodology, we can build a complex cellular process models. The synaptic crosstalk is a physiological event which leads to a local increase of the membrane excitability that is due to the interaction between electrical and biochemical signals. This interaction represents an excellent case study for the development and the validation of our methodology. Our model includes the regulation of calcium, MAPK the channel KV4.2.

De nos jours, nous assistons à l'émergence d'un écosystème informatique au sein de l'entreprise due à la cohabitation de plusieurs types de systèmes et d'équipements informatique. Cette diversité ajoute de la complexité dans la gestion de la sécurité informatique en général et le contrôle d'accès en particulier. En effet, plusieurs systèmes informatiques implémentent le contrôle d'accès en se basant sur des modèles comme le MAC1, DAC2, RBAC3 entre autres. Ainsi, chaque système a sa propre stratégie donc son propre de modèle de contrôle d'accès. Cela crée une hétérogénéité dans la gestion des droits d'accès. Pour répondre à ce besoin de gestion du contrôle d'accès, nous avons, dans ce mémoire, présenté la conception d'une ontologie et d'un outil de gestion automatique des droits d'accès dans un environnement hétérogène. Cet outil se base sur notre ontologie qui permet d'introduire une abstraction sur les modèles de contrôle d'accès implémentés dans les différents systèmes à analyser. Ainsi, les administrateurs de sécurité disposent un outil pour valider l'ensemble des droits d'accès dans leurs écosystèmes informatique. / Today, we are seeing the emergence of an IT ecosystem within companies due to the coexistence of several types of systems and computer equipements. This diversity adds complexity in management of computer security in general and particulary in access control. Indeed, several computer systems implement access control techniques based on models like MAC4, DAC5, RBAC6 among others. Each system has its own strategy based on its own access control model. This creates a heterogeneity in the management of access rights. To respond to this need related to the management of access control, we presented the design of an ontology and we developped an automated management tool of access rights in a heterogeneous environment. This tool is based on our ontology which introduces an abstraction on access control models implemented in different systems that we want analyze. Thus, security administrators have a tool to validate all access rights in their IT ecosystems.

Dans des domaines comme l'aéronautique, l'énergie, le médical ou encore les technologies de l'information en général, les besoins de formuler des arguments de sûreté, sécurité, confidentialité, etc. sont de plus en plus présents. Or, la représentation et l'évaluation de ces arguments n'est pas une chose aisée et fait l'objet de nombreux débats depuis les dix dernières années particulièrement. Une structure argumentative est une modélisation d'un argument ayant comme but d'expliciter les liens (l'argument) reliant une affirmation modélisant une propriété d'un système aux preuves qui la supportent. Les deux principaux défis reliés aux structures argumentatives sont les langages de représentation et les méthodes permettant d'évaluer le niveau de confiance que l'on peut attribuer à l'argument modélisé. S'intéressant à ces deux problématiques, ce mémoire investigue d'une part des langages permettant de représenter des structures argumentatives, et d'une autre part la théorie de l'évidence de Dempster-Shafer. En particulier, ce mémoire présente les langages GSN et TCL, la correspondance entre ces deux langages ainsi que de possibles extensions permettant d'en augmenter l'expressivité. La théorie de l'évidence de Dempster-Shafer y est aussi présentée et y fait l'objet d'une extension qui évite de traiter les cas limites comme des cas particuliers. La théorie de l'évidence de Dempster-Shafer permet de construire un modèle de confiance global à partir d'évaluations locales. Ces dernières sont obtenues en évaluant chaque composante d'une structure argumentative de façon indépendante. Des approches de construction des structures argumentatives ainsi que d'évaluation de leurs éléments sont développées et appliquées dans le cas de deux exemples provenant de deux contextes différents : la conformité avec l'exemple de l'ISO-27001 et la sûreté avec l'exemple d'une pompe à perfusion.

La sécurité des systèmes d’information est l’une des préoccupations les plus importantes du domaine de la science informatique d’aujourd’hui. Les particuliers et les entreprises sont de plus en plus touchés par des failles de sécurité et des milliards de dollars ont été perdus en raison de cyberattaques. Cette thèse présente une approche formelle basée sur la réécriture de programmes permettant d’appliquer automatiquement des politiques de sécurité sur des programmes non sécuritaires. Pour un programme P et une politique de sécurité Q, nous générons un autre programme P’ qui respecte une politique de sécurité Q et qui se comporte comme P, sauf si la politique est sur le point d’être violée. L’approche présentée utilise l’algèbre [symbol] qui est une variante de [symbol] (Basic Process Algebra) étendue avec des variables, des environnements et des conditions pour formaliser et résoudre le problème. Le problème de trouver la version sécuritaire P’ à partir de P et de Q se transforme en un problème de résolution d’un système linéaire pour lequel nous savons déjà comment extraire la solution par un algorithme polynomial. Cette thèse présente progressivement notre approche en montrant comment la solution évolue lorsqu’on passe de l’algèbre de [symbol] à [symbol]. / The security of information systems is one of the most important preoccupations of today’s computer science field. Individuals and companies are more and more affected by security flaws and billions of dollars have been lost because of cyber-attacks. This thesis introduces a formal program-rewriting approach that can automatically enforce security policies on non-trusted programs. For a program P and a security policy Q, we generate another program P’ that respects the security policy Q and behaves like P except when the enforced security policy is about to be violated. The presented approach uses the [symbol] algebra that is a variant of the BPA (Basic Process Algebra) algebra extended with variables, environments and conditions to formalize and resolve the problem. The problem of computing the expected enforced program [symbol] is transformed to a problem of resolving a linear system for which we already know how to extract the solution by a polynomial algorithm. This thesis presents our approach progressively and shows how the solution evolves when we move from the [symbol] algebra to the [symbol] algebra.

La contribution principale de ce document est de suggérer une nouvelle méthode pour mesurer le degré de similarité entre politiques de sécurité écrites en XACML. Ceci est réalisé en deux étapes : premièrement, la politique de sécurité XACML est formalisée en SPL, deuxièmement les résultats obtenus vont servir pour mesurer la distance entre politiques. Le choix de la distance à utiliser dépend des types de prédicats (catégoriques ou numériques). De ce fait, un tableau synthétique a été prévu pour repartir les différentes métriques qui sont calculées dans ce document selon leurs prédicats. Un prototype a été codé en PHP et implémenté pour valider notre contribution. Des recommandations ont été émises en conclusion pour enrichir l’approche proposée. / The main contribution of this paper is to suggest a new method to measure the similarity between security policies written in XACML. This is done in two steps: first the safety policy is formalized in SPL, secondly the results will be used to measure the distance between policies. The choice of the distance to use depends on the types of predicates (categorical or numeric). Thus, a synthetic table is provided to link the different metrics that are calculated in accordance with their predicate. A prototype has been coded in PHP and implemented to validate our contribution. Recommendations were issued in conclusion to enrich the proposed approach.

Les applications de l’analyse du comportement humain ont subit de rapides développements durant les dernières décades, tant au niveau des systèmes de divertissements que pour des applications professionnelles comme les interfaces humain-machine, les systèmes d’assistance de conduite automobile ou des systèmes de protection des piétons. Cette thèse traite du problème de reconnaissance de piétons ainsi qu’à l’estimation de leur orientation en 3D. Cette estimation est faite dans l’optique que la connaissance de cette orientation est bénéfique tant au niveau de l’analyse que de la prédiction du comportement des piétons. De ce fait, cette thèse propose à la fois une nouvelle méthode pour détecter les piétons et une manière d’estimer leur orientation, par l’intégration séquentielle d’un module de détection et un module d’estimation d’orientation. Pour effectuer cette détection de piéton, nous avons conçu un classificateur en cascade qui génère automatiquement une boîte autour des piétons détectés dans l’image. Suivant cela, des régions sont extraites d’un nuage de points 3D afin de classifier l’orientation du torse du piéton. Cette classification se base sur une image synthétique grossière par tramage (rasterization) qui simule une caméra virtuelle placée immédiatement au-dessus du piéton détecté. Une machine à vecteurs de support effectue la classification à partir de cette image de synthèse, pour l’une des 10 orientations discrètes utilisées lors de l’entrainement (incréments de 30 degrés). Afin de valider les performances de notre approche d’estimation d’orientation, nous avons construit une base de données de référence contenant 764 nuages de points. Ces données furent capturées à l’aide d’une caméra Kinect de Microsoft pour 30 volontaires différents, et la vérité-terrain sur l’orientation fut établie par l’entremise d’un système de capture de mouvement Vicon. Finalement, nous avons démontré les améliorations apportées par notre approche. En particulier, nous pouvons détecter des piétons avec une précision de 95.29% et estimer l’orientation du corps (dans un intervalle de 30 degrés) avec une précision de 88.88%. Nous espérons ainsi que nos résultats de recherche puissent servir de point de départ à d’autres recherches futures. / The application of human behavior analysis has undergone rapid development during the last decades from entertainment system to professional one, as Human Robot Interaction (HRI), Advanced Driver Assistance System (ADAS), Pedestrian Protection System (PPS), etc. Meanwhile, this thesis addresses the problem of recognizing pedestrians and estimating their body orientation in 3D based on the fact that estimating a person’s orientation is beneficial in determining their behavior. In this thesis, a new method is proposed for detecting and estimating the orientation, in which the result of a pedestrian detection module and a orientation estimation module are integrated sequentially. For the goal of pedestrian detection, a cascade classifier is designed to draw a bounding box around the detected pedestrian. Following this, extracted regions are given to a discrete orientation classifier to estimate pedestrian body’s orientation. This classification is based on a coarse, rasterized depth image simulating a top-view virtual camera, and uses a support vector machine classifier that was trained to distinguish 10 orientations (30 degrees increments). In order to test the performance of our approach, a new benchmark database contains 764 sets of point cloud for body-orientation classification was captured. For this benchmark, a Kinect recorded the point cloud of 30 participants and a marker-based motion capture system (Vicon) provided the ground truth on their orientation. Finally we demonstrated the improvements brought by our system, as it detected pedestrian with an accuracy of 95:29% and estimated the body orientation with an accuracy of 88:88%.We hope it can provide a new foundation for future researches.

Un programme est dit non interférent si les valeurs de ses sorties publiques ne dépendent pas des valeurs de ses entrées secrètes. Des études ont montré que par l'analyse du flot d'information, on peut établir et contrôler cette propriété ou des propriétés qui lui sont étroitement liées. Dans ce travail, nous examinons en détail les modèles d'analyse de flot d'information existants, et esquissons une nouvelle approche dans un paradigme concurrent. La première partie de ce mémoire présente les différentes formulations de la non-interférence et un survol des grandes familles de mécanismes d'analyse de flot d'information. En second lieu, nous présentons en détail quelques mécanismes récents d'analyse sensibles aux flots, applicables à la programmation séquentielle. Mécanismes statiques pour certains, dynamiques ou hybrides pour d'autres. Dans la troisième partie, nous explorons deux modèles récents de sécurisation des flots d'information dans un programme concurrent. Les deux modèles ont en commun la particularité de proposer des traitements pour sécuriser l'interaction entre les programmes et l'ordonnanceur. Nous terminons par une esquisse de notre nouvelle approche, basée sur l'analyse des dépendances entre les variables d'un programme concurrent. / A program is said to be noninterfering if the values of its public (or low) outputs do not depend on the values of its secret (or high) inputs. Various researchers have demonstrated how this property (or closely related properties) can be achieved through information flow analysis. In this work, we present in detail some existing models of information flow analysis, and sketch a new approach of analysis for concurrent programming. The first part of this thesis presents the different formulations of non-interference, and an overview of the main types of information flow analysis. In the second part, we examine in detail some recent static and dynamic (hybrid) flow-sensitive analysis models, for a simple imperative language. In the third part, we explore two recent models of secure information flow in concurrent programs, which develop a novel treatment of the interaction between threads and the scheduler to prevent undesired interleaving. We end with a sketch of the foundations for another approach, based on the analysis of dependencies between variables of concurrent programs.