L'hybridation des mécanismes de méthodes incomplètes et des techniques de programmation par contraintes est souvent basée sur des combinaisons de type maître-esclave, dédiées à la résolution de classes de problèmes spécifiques. Dans cette thèse, nous nous intéressons à la définition d'un modèle théorique uniforme, basé sur les itérations chaotiques de K.R. Apt qui définissent un cadre mathématique pour l'itération d'un ensemble fini de fonctions sur des domaines abstraits munis d'un ordre partiel. Ce cadre permet<br />de prendre en compte une hybridation entre les méthodes incomplètes et les méthodes complètes. Dans ce contexte, la résolution s'apparente à un calcul de point fixe d'un ensemble de fonctions de réductions spécifiques. Notre cadre générique permet alors d'envisager des stratégies de combinaisons et d'hybridation de manière plus fine et d'étudier leurs propriétés. Nous avons employé un cadre général approprié pour modéliser la résolution des problèmes d'optimisation et nous présentons des résultats<br />expérimentaux qui mettent en avant les atouts de telles<br />combinaisons en regard d'une utilisation indépendante des techniques de résolution.

In this thesis, we propose architecture for a SaaS model in Cloud that would provide service to the financial investors who are not familiar with various mathematical models. Such finance models are used to evaluate financial instruments, for example, to price a derivative that is currently being traded before entering into a contact. An investor may approach CSP to price a particular derivative and specify the time, budget and accuracy constraints. Based on these constraints specified by investors, the service provider will compute the option value using our proposed FSM. To evaluate our proposed model, we compared pricing results with the classical model that provides a closed-form solution for option pricing to meet the accuracy constraints. After establishing the accuracy of our pricing results, we further ensured that the SLA between the FSP and the investors is honoured by meeting the constraints put forth by the investor who uses the Cloud service.

In this thesis, we propose architecture for a SaaS model in Cloud that would provide service to the financial investors who are not familiar with various mathematical models. Such finance models are used to evaluate financial instruments, for example, to price a derivative that is currently being traded before entering into a contact. An investor may approach CSP to price a particular derivative and specify the time, budget and accuracy constraints. Based on these constraints specified by investors, the service provider will compute the option value using our proposed FSM. To evaluate our proposed model, we compared pricing results with the classical model that provides a closed-form solution for option pricing to meet the accuracy constraints. After establishing the accuracy of our pricing results, we further ensured that the SLA between the FSP and the investors is honoured by meeting the constraints put forth by the investor who uses the Cloud service.

(Brief abstract written by the author in 2011 since I don't have the original to hand.) This thesis introduced much of the theory for Hoare's CSP, including the failures and failures-divergences model and methods of proving properties of processes based on metric, order and topological structures. The final chapter investigates the structures underlying operational semantics.

Stuttgart, Univ., Fakultät Informatik, Diplomarb., 1998.

Parmi les technologies disponibles de production d’électricité décarbonée et compétitive, les centrales solaires à concentration ponctuelle permettent d’atteindre les meilleurs rendements. Le développement commercial est actuellement orienté vers les tours à récepteur tubulaire ou surfacique. L’enjeu majeur consiste à faire fonctionner ces récepteurs à des températures supérieures à 800°C de manière cyclique, ce qui nécessite l’emploi de matériaux à hautes performances stables dans le temps. Les alliages ou céramiques réfractaires présentent des propriétés adaptées, mais l’évolution de leur endommagement est encore mal connue. Afin d’étudier ce comportement, un dispositif expérimental basé sur la technique d’émission acoustique a été développé. Cette technique permet d’estimer in situ la sévérité, le type, et la position d’un endommagement. Une méthode de test originale a été élaborée de manière à identifier une stratégie expérimentale de vieillissement pertinente. / Among the available technologies for carbon-free and competitive electricity production, solar tower power plants can achieve the best efficiency. Commercial development is currently focused on tubular or surface receivers, as they allow a low-intricacy design. The major challenge is to cyclically operate these receivers at temperatures above 800°C, which involves the use of durable and high performance materials. Refractory alloys and ceramics have adequate properties, but their damage evolution under these specific conditions is still poorly understood. An innovative set up based on the acoustic emission technique has been designed and realized with a view to scrutinize these materials in situ behavior. Indeed, acoustic emission enables to estimate the severity, the type, and the position of a damage appearing under concentrated solar irradiation tests. Besides, an original numerical method has been developed to identify the suitable test conditions for relevant experimental aging.

Cette thèse se focalise sur l'étude de cohérences locales fortes afin de résoudre des problèmes d'optimisation sur des réseaux de fonctions de coûts (ou réseaux de contraintes pondérées). Ces méthodes fournissent le minorant nécessaire pour des approches de type "Séparation-Evaluation". Nous étudions dans un premier temps la cohérence d'Arc virtuelle (VAC), une des plus fortes cohérences d'arcs du domaine, qui est établie via l'établissement de la cohérence d'arc dure dans une séquence de réseaux de contraintes classiques. L'algorithme itératif pour établir VAC est amélioré via l'introduction d'une incrémentalité accrue, exploitant la cohérence d'arc dynamique. La nouvelle méthode est aussi capable de maintenir VAC efficacement pendant la recherche lorsque les réseaux de contraintes pondérées sont dynamiquement modifiés par les opérations de branchement. Dans une seconde partie, nous nous intéressons à des cohérences de domaines plus fortes, inspirées de cohérences similaires dans les réseaux de contraintes classiques (cohérence de chemin inverse, réduite ou Max-réduite). Pour chaque cohérence dure, plusieurs cohérences souples ont été proposées pour les réseaux de contraintes pondérées. Les nouvelles cohérences fournissent un minorant plus fort que celui des cohérences d'arc souples en traitant les triplets de variables connectées deux à deux par des fonctions de coûts binaires. Dans cette thèse, nous étudions les propriétés des nouvelles cohérences, les implémentons et les testons sur une variété de problèmes. / This thesis focuses on strong local consistencies for solving optimization problems in cost function networks (or weighted constraint networks). These methods provide the lower bound necessary for Branch-and-Bound search. We first study the Virtual arc consistency, one of the strongest soft arc consistencies, which is enforced by iteratively establishing hard arc consistency in a sequence of classical Constraint Networks. The algorithm enforcing VAC is improved by integrating the dynamic arc consistency to exploit its incremental behavior. The dynamic arc consistency also allows to improve VAC when maintained VAC during search by efficiently exploiting the changes caused by branching operations. Operations. Secondly, we are interested in stronger domain-based soft consistencies, inspired from similar consistencies in hard constraint networks (path inverse consistency, restricted or Max-restricted path consistencies). From each of these hard consistencies, many soft variants have been proposed for weighted constraint networks. The new consistencies provide lower bounds stronger than soft arc consistencies by processing triplets of variables connected two-by-two by binary cost functions. We have studied the properties of these new consistencies, implemented and tested them on a variety of problems.

This thesis describes a theoretical study and an industrial application in the area of formal systems development, verification and formal testing using the specification language CSP-CASL. The latter is a comprehensive specification language which allows to describe systems in a combined algebraic / process algebraic notation. To this end it integrates the process algebra CSP and the algebraic specification language CASL. In this thesis we propose various formal development notions for CSP-CASL capable of capturing informal vertical and horizontal software development which we typically find in industrial applications. We provide proof techniques for such development notions and verification methodologies to prove interesting properties of reactive systems. We also propose a theoretical framework for formal testing from CSP-CASL specifications. Here, we present a conformance relation between a physical system and a CSP-C ASL specification. In particular we study the relationship between CSP-CASL development notions and the implemented system. The proposed theoretical notions of formal system development, property verification and formal testing for CSP-CASL, have been successfully applied to two industrial application: an electronic payment system called EP2 and the starting system of the BR725 Rolls- Royce jet engine control software.

Syfte: Sambandet mellan Corporate Social Performance (CSP) och Financial Performance (FP) har studerats av många forskare och resultaten har varit motstridiga. Samtidigt har fler och fler länder börjat göra hållbarhetsrapportering obligatorisk men lite forskning har gjorts om vilken påverkan obligatorisk hållbarhetsrapportering har på FP. Mot bakgrund av de nya lagarna och motsägelsefull forskning har vi valt att undersöka sambandet mellan tre CSP-dimensioner (miljö, social och företagsstyrning) och FP i obligatorisk och frivillig hållbarhetsrapportering. Metod: Metoden som används i denna studie har ett deduktivt tillvägagångssätt från en positivistisk forskningsfilosofi. Två grupper av data undersöks, från Europa och USA. Företagen från de två grupperna granskas ur ett longitudinellt perspektiv över 12 år. Totalt undersöks 700 företag, 338 från Europa och 362 från USA. Uppgifterna samlades genom databasen Thomson Reuters Datastream och analyserades genom SPSS (Statistical Package for Social Sciences). Resultat och slutsats: Resultaten visar skillnaden mellan obligatorisk och frivillig hållbarhetsrapportering. Europeiska företag visar i genomsnitt ett negativt samband mellan CSP-dimensionerna Miljö och Social och FP medan amerikanska företag visar ett positivt förhållande mellan CSP-dimensionerna och FP. Både europeiska och amerikanska företag visar ett positivt samband mellan CSP-dimensionen Företagsstyrning och FP. Examensarbetets bidrag: Resultaten visar att det verkar finnas en skillnad i förhållandet mellan CSP och FP beroende på rapporteringsformatet. CSP-dimensionerna Miljö och Social visar en skillnad medan Företagsstyrning är samma för Europa och USA. Resultaten visar inverkan som rapporteringsformatslagar kan ha på företagens FP. Detta kan i sin tur bidra till att skapa praktisk information om hur hållbarhetsrapportering kan användas på ett positivt sätt för både hållbarhet och företag.Förslag till fortsatt forskning: Flera förslag om framtida forskning görs. Ett förslag är att observera data med hänsyn till varje år och se om ett mönster syns. Det kan vara att obligatorisk hållbarhetsrapportering påverkar FP på olika sätt under flera år. Ett annat förslag är att undersöka olika branscher eftersom de kan uppleva påverkan av obligatorisk och frivillig rapportering på olika sätt.

The increase of computer systems complexity has led to a direct increase in the difficulty of verifying their correctness. For mastering this complexity, formal methods can be used in the development of systems providing techniques for both design and verification. Regarding concurrent and distributed systems, the necessity of a formal approach is more prominent given the substantial increase in complexity due to the countless number of interactions between their constituent systems. Unfortunately, however, current methods are not capable of dealing with the automated analysis of such systems in general, even if we consider only classical properties such as deadlock freedom; the state explosion problem is the main reason for this ineffectiveness. This work is a contribution in this direction. Particularly, considering networks of CSP processes, this work proposes a local strategy for deadlock analysis based on the notion of process refinement. The locality of this strategy prevents the state explosion problem generated by the interaction of constituent systems, which represents a major asset of our strategy. We define a refinement assertion for checking conflict freedom between pairs of processes in the network; this can be used for the local verification of networks with an acyclic communication topology. Concerning networks with a cyclic communication topology, we propose three patterns that prevent deadlocks: the resource allocation, the client/server and the async dynamic. These patterns impose behavioural and structural restrictions to prevent deadlocks. The behavioural restrictions are also captured by refinement assertions, which enable one to automatically verify these conditions using a refinement checker. Besides this, we develop four case studies to evaluate the efficiency of our strategy in practice: a ring buffer, a dining philosopher, and two variations of a leadership election algorithm. One of the variations of the leadership election algorithm consists of a model used in practice by the B&O Company, an industrial partner. In this study, we compare our strategy with two other techniques for deadlock freedom verification, the SSD algorithm of the Deadlock Checker tool and the built-in deadlock freedom assertion of FDR. This study demonstrates how our strategy can be used and that it might be a useful alternative to analysing complex industrial systems for deadlock freedom. / Submitted by Luiz Felipe Barbosa (luiz.fbabreu2@ufpe.br) on 2015-03-10T16:54:41Z No. of bitstreams: 2 DISSERTAÇÃO Pedro Ribeiro Gonçalves Antônio.pdf: 921372 bytes, checksum: 64def1c3ae98cbca7868d944c1f786f2 (MD5) license_rdf: 1232 bytes, checksum: 66e71c371cc565284e70f40736c94386 (MD5) / Made available in DSpace on 2015-03-11T17:34:41Z (GMT). No. of bitstreams: 2 DISSERTAÇÃO Pedro Ribeiro Gonçalves Antônio.pdf: 921372 bytes, checksum: 64def1c3ae98cbca7868d944c1f786f2 (MD5) license_rdf: 1232 bytes, checksum: 66e71c371cc565284e70f40736c94386 (MD5) Previous issue date: 2014-03-31 / Com o aumento da complexidade dos sistemas computacionais, houve também um aumento da dificuldade na tarefa de verificação de sistemas. Para lidar com essa complexidade, métodos formais podem ser usados no desenvolvimento de sistemas, fornecendo técnicas para a modelagem e verificação. No contexto de sistemas concorrentes e distribuídos, a necessidade de uma abordagem formal é ainda mais proeminente, dadas as inúmeras possibilidades de interação entre seus sistemas componentes. Entretanto, infelizmente, os métodos atuais não se encontram, de forma geral, completamente aptos a lidar com a análise automática desses sistemas, mesmo em se tratando de propriedades clássicas como a ausência de deadlocks. A explosão do espaço de estados a ser analisado é o principal fator para essa ineficácia por parte desses sistemas. O trabalho apresentado é uma contribuição nesta direção. Considerando o conceito de redes de processos CSP, o presente trabalho propõe uma estratégia local para a análise de deadlocks baseada na noção de refinamento de processos. A localidade dessa estratégia previne a explosão de espaço de estados causada pela interação de sistemas componentes, o que constitui uma vantajosa característica da nossa estratégia. O trabalho define uma expressão de refinamento capturando o conceito de ausência de conflito, que pode ser usado para verificar localmente que uma rede de processos com uma topologia de comunicação acíclica é livre de deadlocks. Para as redes com topologia cíclica, o trabalho sistematiza e formaliza três padrões comportamentais que impedem deadlocks: o alocação de recursos, o cliente/servidor e o assíncrono dinâmico. Esses padrões impõem restrições comportamentais e estruturais para prevenir deadlocks. Essas restrições comportamentais também são capturadas através de expressões de refinamento, o que possibilita a verificação automática dessas condições com o uso de um verificador de refinamento. Além disso, são apresentados quatro estudos de caso usados para avaliar o desempenho da nossa técnica na prática: um buffer circular, um jantar dos filósofos e duas variações de um algoritmo para eleição de líder. Uma dessas variações consiste num modelo usado na prática pela empresa B&O, um parceiro industrial. Nesse estudo, avaliamos a nossa técnica em comparação com outras duas técnicas para verificação de ausência de deadlocks, o algoritmo SSD da ferramenta Deadlock Checker e a asserção de verificação de deadlocks padrão do verificador de modelos FDR. Esse estudo demonstra como a nossa estratégia é aplicada e que ela pode ser uma alternativa vantajosa para a verificação de sistemas complexos.