Recent technological advances have resulted in increasingly larger databases. The fast and efficient useful analysis and interpretation of this data to improve business intelligence is critical to the success of all organisations. This thesis presents a new framework that utilises a new multilayer mining theory and is based on business intelligence methods, data mining techniques, online analytical processing (OLAP) and online transactional processing (OLTP). Existing decision making modelling approaches for executive information systems have three main shortcomings and limitations to different degrees: a) problems in accessing new types and new structures of data sources; b) failing to provide organizational insight and panorama; and c) generating excessive amount of trivial information. The hypothesis of this research is that a new proactive Multidimensional Multilayer Mining Management Model (5M) framework which is proposed in this thesis will overcome the shortcomings listed above. The 5M framework is made up of 6 components: (a) multilayer mining structures; (b) measurable objectives conversion models; (c) operational transaction databases; d) object-model data marts; (e) data cubes and (f) core analysis engine which analyse the multidimensional cubes, multilayer mining structures and the enterprise key performance indicators. The 5M framework was evaluated by developing an implementation of an instance of the framework called the Ebusiness Analytical Framework (EBAF). The 5M framework and the subsequent EBAF framework were built by carrying out action research and a case study in an ebusiness company where it was subject to implementation, reflection, adaptation and improvement in order to fulfil the requirements of the hypothesis and that of a real business. EBAF implemented all 6 components of the 5M framework using the Visual Studio environment and using various algorithms, tools and programming languages. The programming languages used included MDX, DMX, SQL, VB.Net and C#. Further empirical case studies can be carried out to evaluate the effectiveness and efficiency of the 5M framework.

Les systèmes informatiques envahissent notre vie quotidienne et sont devenus des éléments essentiels de chacun de nos instants de vie. La technologie de l'information est un secteur d'activités offrant des opportunités considérables pour l'innovation et cet aspect paraît sans limite. Cependant, des systèmes à logiciel intégré ont donné des résultats décevants. Selon les constats, ils étaient non fiables, parfois dangereux et ne fournissaient pas les résultats attendus. La faiblesse des pratiques de développement constitue la principale raison des échecs de ces systèmes. Ceci est dû à la complexité des logiciels modernes et au manque de connaissances adéquates et propres. Le développement logiciel fournit un cadre contribuant à simplifier la conception de systèmes complexes, afin d'en obtenir une meilleure compréhension et d'assurer une très grande qualité à un coût moindre. Dans les domaines de l'automatique, de la surveillance médicale, de l'avionique..., les systèmes embarqués hautement critiques sont candidats aux erreurs pouvant conduire à des conséquences graves en cas d'échecs. La thèse vise à résoudre ce problème, en fournissant un ensemble de techniques, d'outils et un cadre pour développer des systèmes hautement critiques, en utilisant des techniques formelles à partir de l'analyse des exigences jusqu'à la production automatique de code source, en considérant plusieurs niveaux intermédiaires. Elle est structurée en deux parties: d'une part des techniques et des outils et d'autre part des études de cas. La partie concernant des techniques et des outils présente une structure intégrant un animateur de modèles en temps-réel, un cadre de correction de modèles et le concept de charte de raffinement, un cadre de modélisation en vue de la certification, un modèle du coeur pour la modélisation en boucle fermée et des outils de générations automatiques de code. Ces cadres et outils sont utilisés pour développer les systèmes critiques à partir de l'analyse des exigences jusqu'à la production du code, en vérifiant et en validant les étapes intermédiaires en vue de fournir un modèle formel correct satisfaisant les propriétés souhaitées attendues au niveau le plus concret. L'introduction de nouveaux outils concourt à améliorer la vérification des propriétés souhaitées qui ne sont pas apparentes aux étapes initiales du développement du système. Nous évaluons les propositions faites au travers de cas d'études du domaine médical et du domaine des transports. De plus, le travail de cette thèse a étudié la représentation formelle des protocoles médicaux, afin d'améliorer les protocoles existants. Nous avons complètement formalisé un protocole réel d'interprétation des ECG, en vue d'analyser si la formalisation était conforme à certaines propriétés relevant du protocole. Le processus de vérification formelle a mis en évidence des anomalies dans les protocoles existants. Nous avons aussi découvert une structure hiérarchique pour une interprétation efficace permettant de découvrir un ensemble de conditions qui peuvent être utiles pour diagnostiquer des maladies particulières à un stade précoce. L'objectif principal du formalisme développé est de tester la correction et la consistance du protocole médical / Software systems are pervasive in all walks of our life and have become an essential part of our daily life. Information technology is one major area, which provides powerful and adaptable opportunities for innovation, and it seems boundless. However, systems developed using computer-based logic have produced disappointing results. According to stakeholders, they are unreliable, at times dangerous, and fail to provide the desired outcomes. Most significant reasons of system failures are the poor development practices for system development. This is due to the complex nature of modern software and lack of adequate and proper understanding. Software development provides a framework for simplifying the complex system to get a better understanding and to develop the higher fidelity quality systems at lower cost. Highly embedded critical systems, in areas such as automation, medical surveillance, avionics, etc., are susceptible to errors, which can lead to grave consequences in case of failures. This thesis intends to contribute to further the use of formal techniques for the development computing systems with high integrity. Specifically, it addresses that formal methods are not well integrated into established critical systems development processes by defining a new development life-cycle, and a set of associated techniques and tools to develop highly critical systems using formal techniques from requirements analysis to automatic source code generation using several intermediate layers with rigorous safety assessment approach. The approach has been realised using the Event-B formalism. This thesis has mainly two parts: techniques and tools and case studies. The techniques and tools section consists of development life-cycle methodology, a framework for real-time animator, refinement chart, a set of automatic code generation tools and formal logic based heart model for close loop modeling. New development methodology, and a set of associated techniques and tools are used for developing the critical systems from requirements analysis to code implementation, where verification and validation tasks are used as intermediate layers for providing a correct formal model with desired system behavior at the concrete level. Introducing new tools help to verify desired properties, which are hidden at the early stage of the system development. We also critically evaluate the proposed development methodology and developed techniques and tools through case studies in the medical and automotive domains. In addition, the thesis work tries to address the formal representation of medical protocols, which is useful for improving the existing medical protocols. We have fully formalised a real-world medical protocol (ECG interpretation) to analyse whether the formalisation complies with certain medically relevant protocol properties. The formal verification process has discovered a number of anomalies in the existing protocols. We have also discovered a hierarchical structure for the ECG interpretation efficiently that helps to find a set of conditions that can be very helpful to diagnose particular disease at the early stage. The main objective of the developed formalism is to test correctness and consistency of the medical protocol

Les logiciels critiques nécessitent l’obtention d’une évaluation de conformité aux normesen vigueur avant leur mise en service. Cette évaluation est obtenue après un long travaild’analyse effectué par les évaluateurs de logiciels critiques. Ces derniers peuvent être aidéspar des outils utilisés de manière interactive pour construire des modèles, en faisant appel àdes analyses de flots d’information. Des outils comme SPARK-Ada existent pour des sous-ensembles du langage Ada utilisés pour le développement de logiciels critiques. Cependant,des langages émergents comme ceux de la famille ML ne disposent pas de tels outils adaptés.La construction d’outils similaires pour les langages ML demande une attention particulièresur certaines spécificités comme les fonctions d’ordre supérieur ou le filtrage par motifs. Cetravail présente une analyse de flot d’information pour de tels langages, spécialement conçuepour répondre aux besoins des évaluateurs. Cette analyse statique prend la forme d’uneinterprétation abstraite de la sémantique opérationnelle préalablement enrichie par desinformations de dépendances. Elle est prouvée correcte vis-à-vis d’une définition formellede la notion de dépendance, à l’aide de l’assistant à la preuve Coq. Ce travail constitue unebase théorique solide utilisable pour construire un outil efficace pour l’analyse de toléranceaux pannes. / Critical software needs to obtain an assessment before commissioning in order to ensure compliance tostandards. This assessment is given after a long task of software analysis performed by assessors. Theymay be helped by tools, used interactively, to build models using information-flow analysis. Tools likeSPARK-Ada exist for Ada subsets used for critical software. But some emergent languages such as thoseof the ML family lack such adapted tools. Providing similar tools for ML languages requires specialattention on specific features such as higher-order functions and pattern-matching. This work presentsan information-flow analysis for such a language specifically designed according to the needs of assessors.This analysis is built as an abstract interpretation of the operational semantics enriched with dependencyinformation. It is proved correct according to a formal definition of the notion of dependency using theCoq proof assistant. This work gives a strong theoretical basis for building an efficient tool for faulttolerance analysis.