Les techniques formelles réalisent des modèles de spécifications et/ou de conception et servent principalement à l'analyse statique de code, à la démonstration du respect de propriété et à la bonne gestion des calculs sur les flottants. Différents domaines tels les systèmes de transport, la production d'énergie ou la santé prennent en compte l'implémentation de ces méthodes pour satisfaire les exigences de sécurité élevées des systèmes critiques. Leur mise en œuvre dans le cadre d'une application industrielle (application de grande taille, contrainte de coût et de délais, etc.) ne peut se faire que par l'emploi d'outils suffisamment matures et performants. Cet ouvrage collectif présente des exemples concrets d'utilisation des techniques formelles comme la méthode B, SCADE, MaTeLo, ControlBuild, SparkAda et POLYSPACE et des techniques de vérification associées. Il en identifie aussi les avantages et les difficultés.

La mise en place d’un logiciel sans défaut reste primordiale pour plusieurs domaines qui requièrent des applications dites de sécurité comme les transports. La réalisation d’un modèle formel est l’approche la plus efficace pour atteindre l'objectif du zéro défaut, que ce soit en termes de temps ou de maîtrise de la complexité. Ce modèle permet d’analyser et de vérifier le comportement d’un logiciel. Cet ouvrage présente la méthode B, une méthode formelle s’appuyant sur la preuve de propriétés qui, sur la base d’une spécification et de la notion de raffinement, permet d’aller jusqu’à la production automatique de code. Différents outils découlant de cette méthode ainsi que des exemples concrets d’utilisations industrielles de différentes tailles sont aussi exposés dans des domaines tels que l’avionique ou les systèmes manufacturiers.

At present the literature gives students and researchers of the very general books on the formal technics. The purpose of this book is to present in a single book, a return of experience on the used of the “formal technics” (such proof and model-checking) on industrial examples for the transportation domain. This book is based on the experience of people which are completely involved in the realization and the evaluation of safety critical system software based. The implication of the industrialists allows to raise the problems of confidentiality which could appear and so allow to supply new useful information (photos, plan of architecture, real example).

This book presents real-world examples of formal techniques in an industrial context. It covers formal methods such as SCADE and/or the B Method, in various fields such as railways, aeronautics, and the automotive industry. The purpose of this book is to present a summary of experience on the use of “formal methods” (based on formal techniques such as proof, abstract interpretation and model-checking) in industrial examples of complex systems, based on the experience of people currently involved in the creation and assessment of safety critical system software. The involvement of people from within the industry allows the authors to avoid the usual confidentiality problems which can arise and thus enables them to supply new useful information (photos, architecture plans, real examples, etc.).

La bonne qualité des données est aujourd'hui la clé de voûte de toute organisation. La gestion et l'amélioration de cette qualité sont des tâches coûteuses et difficiles, mais néanmoins incontournables. Cet ouvrage propose une étude des différents outils et démarches qui assistent les spécialistes de la qualité et de la gouvernance des données. À travers les expériences de la communauté francophone animée par l'association ExQI (Excellence Qualité, Information), il présente, avec pédagogie et pragmatisme, un panorama des concepts-clés de la gestion de la qualité des données et leurs déclinaisons dans les entreprises (Business Intelligence, Data QualityManagement, Key Performance Indicator, Model Driven Engineering, Master Data Management, etc.). Des solutions théoriques et techniques performantes sont détaillées et de nombreux retours d'expérience permettent d'illustrer les bonnes pratiques à adopter. Mêlant contributions industrielles et académiques, cet ouvrage est un outil de référence en langue française sur la qualité et la gouvernance des données en entreprise.

Certifiable Software Applications 3: Downward Cycle describes the descending phase of the creation of a software application, detailing specification phases, architecture, design and coding, and important concepts on modeling and implementation. For coding, code generation and/or manual code production strategies are explored. As applications are coded, a presentation of programming languages and their impact on certifiability is included. - Describes the descending phase of the creation of a software application, detailing specification phases, architecture, design and coding - Presents valuable programming examples - Includes a presentation of programming languages and their impact on certifiability

Les systèmes embarqués rendent un nombre de services grandissant et font partie de notre vie quotidienne : ascenseurs, transports, téléphonie, médecine, énergie, industrie, etc. Ainsi, si l’on parle de plus en plus de systèmes embarqués, il s’agit avant tout d’un ensemble complet et intégré (matériel + logiciel). Le point central de leur développement est leur interaction avec leur environnement et les conséquences associées en termes de sécurité et de fiabilité. Cet ouvrage dresse un état de l’art du développement des systèmes embarqués. Il se concentre particulièrement sur leur modélisation et leur analyse. Il s’agit d’opérations cruciales qui détermineront la fiabilité du futur système. L’apparition récente des techniques basées sur l’ingénierie des modèles pourrait révolutionner le développement de ces systèmes en assurant une continuité entre le niveau conceptuel et l’implémentation de la partie logicielle. L’ouvrage expose trois approches parmi les plus utilisées : SysML (aspects ingénierie système), UML/MARTE et AADL (conception/analyse).