Les systèmes de preuves formelles ont connu ces dernières années des évolutions importantes. Des travaux récents, comme la preuve formelle du théorème des quatre couleurs ou celle du théorème des nombres premiers, ont montré que ces systèmes ont atteint un niveau de maturité leur permettant de s'attaquer à des problèmes mathématiques non triviaux. Malgré cela, l'utilisation des systèmes de preuves formelles en mathématique reste très limitée. Un des arguments qui est avancé pour expliquer cette situation est le manque de bibliothèques de preuves formelles. Cette thèse s'intéresse au développement de composants mathématiques pour la théorie des groupes finis. Elle entre dans le cadre du travail de formalisation du théorème de Feit-Thompson sur la classification des groupes finis. L'objectif principal dans ce travail est d'appliquer les techniques de génie logiciel pour faciliter la réutilisation et l'organisation des développements mathématiques formelles de grande échelle, comme la formalisation du théorème de Feit-Thompson. Cette thèse présente une première formalisation du théorème de Cayley-Hamilton sur les polynômes et les matrices. Elle présente aussi des développements sur la théorie des représentations des groupes finis qui est une composante nécessaire à la formalisation de la preuve du théorème de Feit-Thompson. En particulier, elle présente une formalisation de la théorie des modules sur un corps ou sur une algèbre ainsi qu'une formalisation du théorème de Maschke. Ces développements ont été faits dans le système Coq et avec l'extension SSReflect.

Face aux nouveaux cadres législatifs ou environnementaux dans lesquels ils doivent évoluer, les systèmes industriels actuels sont, en plus d'être contraints par des exigences classiques de productivité et de cout, sujets au respect de nouvelles exigences relatives à la sûreté, la sécurité ou au développement durable notamment. Pour répondre à ces exigences et améliorer la maitrise des performances de ses systèmes, EDF souhaite faire évoluer sa démarche d'Optimisation de la Maintenance Basée sur la Fiabilité vers une nouvelle méthode. Cette méthode nécessite en autre la proposition d'une approche outillée permettant de quantifier a priori les programmes de maintenance (CMPQ) sur ses systèmes par rapport aux indicateurs de performance attendus (KPIs). Cet outillage fait l'objet de cette thèse financée dans le cadre du GIS 3SGS - projet DEPRADEM 2. Après avoir généralisé les besoins d'EDF en regard de la CMPQ, nous proposons une identification de la connaissance générique nécessaire pour évaluer les KPI. Afin d'aboutir à un outil permettant l'automatisation de ces études de CMPQ, cette connaissance générique est ensuite modélisée sur la base de deux langages : le langage semi-formel SysML capitalisant, par l'intermédiaire de différents diagrammes, la connaissance statique, interactionnelle et comportementale ; et le langage AltaRicaDF, supportant un modèle dynamique permettant d'évaluer les KPIs par simulation stochastique. La création de ce modèle dynamique à partir des différents diagrammes est basée sur un mapping entre les concepts d'intérêt des deux langages. La démarche dans sa globalité est validée à la CMPQ d'un cas d'étude fourni par EDF : le système ARE.

The proliferation of services on the web is leading to the formation of service ecosystems wherein services interact with one another in ways not foreseen during their development or deployment. This means that over its lifetime, a service is likely to be reused across multiple interactions, such that in each of them a different interface is required from it. Implementing, testing, deploying, and maintaining adapters to deal with this multiplicity of required interfaces can be costly and error-prone. The problem is compounded in the case of services that do not follow simple request-response interactions, but instead engage in conversations comprising arbitrary patterns of message exchanges. A key challenge in this setting is service mediation: the act of retrofitting existing services by intercepting, storing, transforming, and (re-)routing messages going into and out of these services so they can interact in ways not originally foreseen. This thesis addresses one aspect of service mediation, namely service interface adaptation. This problem arises when the interface that a service provides does not match the interface that it is expected to provide in a given interaction. Specifically, the thesis focuses on the reconciliation of mismatches between behavioural interfaces, that is, interfaces that capture ordering constraints between message exchanges. We develop three complementary proposals. Firstly, we propose a visual language for specifying adapters for conversational services. The language is based on a an algebra of operators that are composed to define links between provided-required interfaces. These expressions are fed into an execution engine that intercepts, buffers, transforms and forwards messages to enact the adapter specification. Secondly, we endow such adapter specifications with a formal semantics defined in terms of Petri nets. The formal semantics is used to statically check the correctness of adapter specifications. Finally, we propose an alternative approach to service interface adaptation that does not require hard-wired links between provided and required interfaces. This alternative approach is based on the definition of mapping rules between message types, and is embodied in an adaptation machine. The adaptation machine sits between pairs of services and manipulates the exchanged messages according to a repository of mapping rules. The adaptation machine is also able to detect deadlocks and information loss at runtime.

Cette thèse explore les rapports entre la formalisation mathématique, ses implications dans les pratiques compositionnelles et ses répercussions sur l’interprétation analytique. Elle se base sur l’étude de Semi-Simple Variations pour piano (1956) de Milton Babbitt, de Nomos Alpha pour violoncelle (1965-1966) de Iannis Xenakis (1921/22-2001), et d’une sélection de textes théoriques publiés par les compositeurs autour de ces deux œuvres.L’argumentaire est divisé en trois parties. La première étudie les textes théoriques afin d’en dégager les éléments formalisés (ou résultant de la formalisation) ainsi que les indices permettant d’en retracer les implications dans les pratiques compositionnelles. Ces éléments sont précisés dans la deuxième partie via la reconstitution des traces laissées par les composantes formalisées dans les textes musicaux (« modèles théoriques »). Ce travail est mené sur les deux œuvres proposées à l’analyse puis élargi à d’autres œuvres. Les modèles théoriques de deux d’entre elles étaient jusque-là restés inédits : Three Compositions for Piano de Babbitt (1947-1948) ; et Akrata de Xenakis pour 16 vents (1964-1965). La troisième partie soumet Semi-Simple Variations et Nomos Alpha à deux analyses : la première étudie les modèles théoriques, directement liés aux univers formels, alors que la seconde examine les surfaces sonores et comment elles articulent et/ou contredisent les éléments dégagés au niveau des modèles. Tout en soulignant le rôle fondamental, quoique très différent, joué par la formalisation dans les univers compositionnels de Babbitt et de Xenakis, la distance séparant les modèles théoriques des surfaces sonores amènent à considérer l’apport des premiers dans l’interprétation analytique comme étant de nature avant tout heuristique. En tant que traces de la pensée du compositeur, les modèles théoriques peuvent néanmoins suggérer de nouvelles pistes et méritent d’être intégrés à des recherches futures. / This thesis explores the links between mathematical formalization, its implications in compositional practices, and its repercussions on the analytical interpretation. It is based on the study of Milton Babbitt’s Semi-Simple Variations for piano (1956), on Iannis Xenakis’ Nomos Alpha for violoncello (1965-1966), and on a selection of theoretical texts published by the composers around these two works. The argumentation is divided in three parts. The first studies the theoretical texts with the aim of extracting from them the components that are formalized (or result form formalization) as well as the indices pointing towards their implications in the compositional practices. These are then put into sharper view in the second part, through the reconstruction of the traces left by these components in the musical texts (“theoretical models”). This reconstruction is first conducted on the two main works considered before other works are considered. The theoretical models of two of them had until now remained unknown: Three Compositions for Piano by Babbitt (1947-1948) ; and Akrata for 16 winds (1964-1965) by Xenakis. The third part submits Semi-Simple Variations and Nomos Alpha to two analyses: one is aimed at the theoretical models, directly linked to the formal universes, the second examines the musical surfaces and at the way they articulate and/or contradict the elements observed in the models. While underlining the fundamental - though very different - role played by mathematical formalization in Babbitt’s and Xenakis’ compositional universes, the distance that separates the theoretical models from the musical surfaces brings one to consider the role of the former within the analytical enterprise as essentially heuristic. As traces of the composer’s thinking, the theoretical models may however suggest new approaches and deserve to be fully integrated in future research.

Cette thèse analyse le processus de formalisation de l’éthique dans les entreprises. L’objectif est de comprendre comment les entreprises transposent et matérialisent par des outils un concept aussi intangible et mal défini que celui de l’éthique des affaires. Une collecte de données qualitatives variées (entretiens, observation, données secondaires, archives) au sein de cinq firmes multinationales françaises a été réalisée et a fait l’objet d’une analyse inductive (Strauss et Corbin, 1990). Ce travail révèle alors que l’absence de définition complète et tangible d’une éthique pour les entreprises est un problème aisément contourné par une volonté de conformité. En simplifiant alors le processus en y intégrant uniquement des aspects légaux, les entreprises créent des incohérences internes telles que l’isomorphisme des outils éthiques, des luttes idéologiques et identitaires entre les designers de l’éthique mais également une gestion de l’éthique qui s’apparente à de la gestion des risques et de l’incertitude. A travers l’éthique, il est possible d’entrevoir une orientation judiciaire et légale du management appelée judiciarisation Ainsi, en s’intéressant à la manière dont ils sont pensés et conçus, cette thèse s’inscrit dans la lignée des nombreux travaux sur les outils de régulation de l’éthique et leur efficacité. / This thesis analyzes the formalization process of ethics within firms. The goal is to understand how companies transpose and materialize by tools an intangible and unclear concept such as business ethics. A collection of varied qualitative data (interviews, observation, secondary data, archives) within five French multinational corporations was conducted. An inductive qualitative study (Strauss and Corbin 1990) uncovered several characteristics of the formalization process of ethics. This works reveals why the vague definition of business ethics is not an issue for companies. As they wish to comply, they simplify the process by mainly considering ethics under a legal aspect. Doing so, companies create internal inconsistencies such as isomorphism of ethical tools, ideological and identical struggles between designers of ethics and a tendency to manage ethics as they manage risk and uncertainty. Through ethics, it is possible to foresee a judicial and legal orientation of management called ‘judicialization’. By studying how ethical tools are conceived and designed, this argument is in line with numerous studies on their regulatory power and effectiveness.

[pt] A tese de Church propõe que tanto a noção de computável quanto a de função recursiva (ou equivalentes: máquina de Turing, cálculo lambda) possuem a mesma extensão. Sua peculiaridade, de acordo com as interpretações mais consolidadas, deve-se ao fato de não poder ser matematicamente demonstrada, uma vez que uma das noções envolvidas, a de computável, possui um caráter informal. Neste trabalho, consideraremos diversas críticas à tese de Church, prestando especial atenção às críticas de caráter intuicionista. Acreditamos ter obtido dois resultados, um que diz respeito diretamente à tese de Church, e outro que diz respeito à lógica intuicionista. Quanto ao primeiro, propomos, na contramão de um realismo ingênuo, que os conceitos matemáticos não são imutáveis e que, por essa razão, uma maneira mais adequada de compreender a tese de Church seria levando em consideração a gênese intencional do conceito de computável. Quanto ao segundo resultado, que diz respeito à associação que o intuicionismo faz entre demonstração e verdade, propõe-se uma maneira coerente de conciliar a condição contingente e temporal de posse de uma demonstração com o caráter necessário e atemporal do valor de verdade de proposições matemáticas. / [fr] La thèse de Church suppose que les notions de fonction calculable et de fonction récursive (ou ses équivalents: machine de Turing, lambda-calcul, etc.) possèdent la même extension. Sa particularité, selon les interprétations les plus consolidées, tient au fait qu elle ne peut pas être démontrée mathématiquement, car l une des notions impliquées, celle du calculable, présente un caractère informel. Dans ce travail, nous examinerons plusieurs critiques de la thèse de Church, en accordant une attention particulière aux critiques de caractère intuitionniste. Nous pensons avoir obtenu deux résultats, l un qui se rapporte directement à la thèse de Church, et l autre qui concerne la logique intuitionniste. Quant au premier, nous proposons, contrairement à un réalisme naif, que les concepts mathématiques ne sont pas immuables et que, pour cette raison, une meilleure façon de comprendre la thèse de Church consisterait à prendre en compte la genèse intentionnelle du concept du calculable. Quant au deuxième résultat, qui traite de l association que l intuitionnisme effectue entre démonstration et vérité, nous proposons une manière cohérente de réconcilier la condition contingente et temporelle de possession de la démonstration avec le caractère nécessaire et intemporel de la valeur de vérité des propositions mathématiques.

Cette thèse s'articule autour de la formalisation de mathématiques dans l'assistant à la preuve Coq dans le but de vérifier des méthodes numériques. Plus précisément, elle se concentre sur la formalisation de concepts qui apparaissent dans la résolution des systèmes d'équations linéaires et non-linéaires. <p> Dans ce cadre, on a analysé la méthode de Newton, couramment utilisée pour approcher les solutions d'une équation ou d'un système d'équations. Le but a été de formaliser le théorème de Kantorovitch qui montre la convergence de la méthode de Newton vers une solution, l'unicité de la solution dans un voisinage, la vitesse de convergence et la stabilité locale de la méthode. L'étude de ce théorème a nécessité la formalisation de concepts d'analyse multivariée. En se basant sur ces résultats classiques sur la méthode de Newton, on a montré qu'arrondir à chaque étape préserve la convergence de la méthode, avec une corrélation bien déterminée entre la précision des données d'entrée et celle du résultat. Dans un travail commun avec Nicolas Julien nous avons aussi formellement étudié les calculs avec la méthode de Newton effectués dans le cadre d'une bibliothèque d'arithmétique réelle exacte. <p> Pour les systèmes linéaires d'équations, on s'est intéressé aux systèmes qui ont une matrice associée à coefficients intervalles. Pour résoudre de tels systèmes, un problème important qui se pose est de savoir si la matrice associée est régulière. On a fourni la vérification formelle d'une collection de critères de régularité pour les matrices d'intervalles.

Cette étude porte sur les différentes formalisations du sens linguistique dans le cadre de la théorie Sens-Texte (TST) ; elle s’intéresse notamment à la représentation sémantique, la représentation la plus importante dans la modélisation du sens d’énoncés et d’unités lexicales de la langue. Cette étude a trois objectifs : premièrement, décrire trois formalisations de la représentation sémantique existant dans la TST – les réseaux sémantiques, les définitions lexicographiques et les définitions de la BDéf (des définitions très formalisées) ; deuxièmement, identifier les disparités et les décalages entre les formalisations choisies ; troisièmement, proposer des modifications aux formalisations existantes pour réduire au maximum ces disparités. / This study explores the different formalisations of linguistic meaning as encountered in the Meaning-Text Theory (MST) framework. Its main interest is semantic representation, which is the most important representation in the modeling of the meaning of utterances and lexical units. This study has three objectives: first, describing three existing formalisations of semantic representation in the MST – semantic networks, lexicographical definitions, and BDéf definitions (definitions that are extremely formalized); second, identifying the discrepancies between these formalisations; finally, proposing modifications to these formalisations in order to reduce the disparities as much as possible.

Les profils permettent de customiser UML pour un domaine particulier. Cette customisation se fait par l’ajout de concepts (stéréotypes) relatifs au domaine, l’ajout de contraintes sur ces concepts ainsi que la résolution de points de variation sémantiques. Il existe un processus établit et documenté dans l’état de l’art permettant de construire la syntaxe de ces langages basés sur UML. En revanche, ce processus ne couvre pas l’aspect formalisation de la sémantique et les propositions issues de l’état de l’art ne présentent pas d’approches systématiques pour traiter ce problème.La formalisation de la sémantique est un point essentiel de la construction d’un langage car elle permet de donner le sens des constructions syntaxiques. Pour être efficace, la formalisation de la sémantique d’un langage doit être menée conjointement à une action de normalisation. L’intérêt d’avoir une sémantique formelle et standard pour un langage est qu’elle permet aux modèles définis dans ce langage d’être exploités (analyse, exécution, simulation, etc.) de manière équivalente entre les outils. Cette équivalence permet aux utilisateurs d’observer des interprétations identiques d’un même modèle entre différents outils et donc d’avoir une compréhension commune du modèle et de la sémantique associée. Dans le contexte des profils, les actions de normalisations menées par l’OMG se concentrent exclusivement sur la syntaxe et la formalisation de la sémantique est négligée. Nous proposons de répondre à ce problème en nous appuyant sur les spécifications fUML et PSCS qui définissent une sémantique normative pour un sous-ensemble d’UML.Dans un premier temps, nous définissons deux méthodologies alternatives s’appuyant sur ces standards permettant de formaliser la sémantique d’exécution d’un profil UML. Dans la première méthodologie la sémantique d’exécution d’un profil est formalisée au niveau du modèle de domaine. La forme exécutable d’un modèle applicatif profilé est obtenue par transformation de modèle. Dans la seconde méthodologie, la sémantique est définie directement pour le profil. Le modèle qui la formalise est une extension du modèle sémantique de fUML/PSCS formalisée avec fUML. Les modèles sémantiques obtenus sont conformes à fUML ce qui les rend par construction exécutables et directement exploitables dans n’importe quel outil implantant les normes UML et fUML. Dans un deuxième temps, nous comparons nos approches sur la base de trois critères : l’effort de modélisation requis pour produire le modèle sémantique, la préservation de la sémantique de base d’UML définie par fUML/PSCS et la possibilité d’identifier rapidement les relations entre les stéréotypes et leurs sémantiques. Cette comparaison, nous permet de montrer la capacité de notre seconde méthodologie à prendre en compte des extensions clefs de la sémantique de base d’UML dans le contexte des profils. Ces éléments clefs sont : la délégation du contrôle, l’instanciation et les communications. L’ensemble de nos contributions ont été outillées dans le contexte de l’outil d’exécution de modèles MOKA qui est intégré au modeleur UML/SysML Papyrus. / UML profiles enable the UML to be tailored to a particular domain. To do so, a profile adds domain specific concepts (i.e., stereotypes) and constraints to UML and disambiguates specific semantic variation points. The design process for abstract syntax of profiles is well documented in the literature. However, specification of the semantics is neglected. According to our researches, there are no proposals in the state-of-the-art that define a systematic approach to solve this problem.Semantic formalization is a key point of language design. It enables to formally define the meaning of syntactic elements. In order to be efficient, the formalization activity must be realized in parallel with a standardization activity. The interest to have a language with a formal standardized semantic is to enable models defined using this latter to be interpreted (analysis, execution, simulation) in equivalent way between tools implementing the semantics. This equivalence enables users to observe similar interpretations of the same model between different tools and therefore to have a shared understanding of this model and the associated semantic.In the context of UML profiles, normalization activities leaded by the OMG are focused on the syntax. The semantic formalization aspect is neglected. We propose to address this problem by relying on fUML and PSCS OMG (Object Management Group) specifications. These standards formalize execution semantics for a subset of UML (classes, composite structures, and activities).Firstly, we define two methodologies relying on these standards to formalize execution semantics of UML profiles execution semantics. The first methodology defines the execution semantics for the domain model underlying the profile. The executable form of an applicative model defined using the profile is obtained by model transformation. In the second methodology, semantics are defined directly for the profile by extending the semantic model of fUML/PSCS using fUML. By being conform to fUML, the semantic model is by construction executable and can be directly used in any tools implementing the UML and fUML standards.Secondly, we compare our approaches against the following criteria: the modelling effort required to build the semantic model, the capability of the methodology to preserve the UML semantics (i.e., the one defined by fUML/PSCS) and the capability to identify clearly the relationships between the stereotypes and their semantics. This comparison enables us to demonstrate the capacity of the second methodology to define key extensions of the UML semantics in the context of a profile. These latter are: the control delegation, the instantiation, and the communications. The contributions have been implemented in our model execution framework Moka which is integrated in the open-source UML/SysML modeling tool Papyrus.

L’objet principal de cette thèse concerne le Dossier Patient Informatisé (DPI) dans les hôpitaux, et plus particulièrement les difficultés d’usage après la phase d’implémentation. Notre démarche visait à concevoir, à partir des connaissances académiques en Système d’Information, une méthode permettant aux acteurs de terrain d’agir sur une problématique spécifique. Concrètement nous cherchions à savoir comment améliorer les situations de « misfit », c’est à dire les situations dans lesquelles les professionnels de santé considèrent l’usage du DPI comme inadapté à leur métier. Pour ce faire, nous avons cherché à comprendre le bilan mitigé du DPI dans la littérature en utilisant les travaux d’Adler & Borys (1996) sur le caractère dual de la formalisation du travail induite par la technologie (habilitante ou coercitive). Une technologie habilitante permet de positionner un utilisateur comme source de solutions, alors qu’une technologie coercitive tend à le considérer comme source de problèmes. Dans le premier manuscrit portant sur l’autonomie des professionnels de santé face au système d’information hospitalier, nous avons conclu sur la nécessité d’une formalisation de type habilitante pour améliorer l’usage du DPI. Dans le deuxième manuscrit, nous avons montré que dans les exemples d’expériences négatives du Dossier Patient Informatisé rapportés dans la littérature, il était possible de mettre en évidence les différents aspects d’une formalisation coercitive. Pour argumenter sur le caractère dual de la formalisation du travail induite par le DPI, nous avons rapporté dans le troisième manuscrit une étude empirique illustrative. Nos données montrent que pour un même DPI, dans un même hôpital, il peut exister des îlots de formalisation habilitante. En sortant du seul domaine d’application de la santé, nous avons approfondi les travaux sur la conceptualisation du misfit entre processus d’affaires et Système d’Entreprise (SE) de Strong & Volkoff de 2010, en utilisant les concepts d’affordance et d’actualisation d’affordance utilisés par les mêmes auteurs en 2013 et 2014. Le quatrième manuscrit présente donc un modèle original permettant d’analyser l’usage des technologies de l’information pour un processus d’affaires donné sous la forme d’une combinaison d’actualisations, de non-actualisation ou d’actualisations partielles de multiples affordances du système d’entreprise par de multiples acteurs. Dans une perspective réaliste critique, le misfit est alors la perception par un individu ou un groupe d’individus que cette combinaison ne répond pas à l’ensemble ou à une partie des objectifs du processus de façon satisfaisante. Nous rapportons ensuite comment, dans le cadre d’une recherche-action, nous avons utilisé ce modèle pour améliorer l’usage d’un DPI en post-implémentation dans un hôpital. L’analyse d’une situation de misfit selon notre méthode permet une recombinaison, en recherchant une suite cohérente d’ajustements techniques et organisationnels acceptables pour toutes les parties prenantes et dont l’agencement permet bien la disparition du misfit initial, mais aussi de l’ensemble des misfits révélés pendant l’analyse. Cette recombinaison aboutit alors à une formalisation du travail présentant toutes les caractéristiques d’une formalisation habilitante.La discussion de la thèse aborde les conditions du succès de la méthode, le choix des situations sur lesquelles l’appliquer et les perspectives de recherche qui en découlent. / The main focus of this thesis is the Electronic Patient Record (EPR) in hospitals, and more particularly the difficulties of use after the implementation phase. Our approach aimed to design, with the academic knowledge of Information Systems, a method allowing field actors to act on this specific issue. In concrete terms, we were looking for ways to improve "misfit" situations, i.e. situations in which health professionals consider the use of EPR to be unsuitable for their profession. To do this, we sought to understand the mixed record of EPR use reported in the professional literature, by using the dual nature (enabling or coercive) of technology-induced work formalization (Adler & Borys, 1996). Enabling technology allows a user to be positioned as a source of solutions, while coercive technology tends to consider them as a source of problems. In the first manuscript on the autonomy of health professionals in relation to the hospital information system, we concluded that an enabling formalization is needed to improve the use of EPR. In the second manuscript, we showed that in the examples of negative experiences of the EPR reported in the literature, it was possible to highlight the different aspects of coercive formalization. To argue on the dual nature of the formalization of work induced by EPR, we have reported in the third manuscript an illustrative empirical study. Our data show that for the same EPR, in the same hospital, there may be islets of enabling formalization.Moving beyond the health field of application alone, we have further developed Strong & Volkoff's 2010 conceptualization of the misfit between business process and Enterprise System (ES), using the concepts of affordance and affordance-actualization used by the same authors in 2013 and 2014.The fourth manuscript therefore presents an original model for analyzing the use of information technology for a given business process in the form of a combination of actualizations, non-actualizations or partial actualizations of multiple affordances of the enterprise system by multiple actors. From a critical realistic perspective, misfit is then the perception by an individual or group of individuals that this combination does not satisfactorily meet all or some of the objectives of the process.We then report on how we used this model to improve the use of EPR in post-implementation in an action research project. The analysis of a misfit situation according to our method allows a recombination, by seeking a coherent sequence of technical and organizational adjustments acceptable to all stakeholders and whose arrangement allows the disappearance of the initial misfit, but also of all the misfits revealed during the analysis. This recombination then leads to a formalization of the work that has all the characteristics of an enabling formalization.The discussion of the thesis addresses the conditions for the success of the method, the choice of situations on which to apply it and the resulting research perspectives.