Книга "Formal Methods. Industrial Use from Model to the Code" посвящена формальным методам анализа программ, которые были введены только в 1980-х годах. Эти методы позволяют анализировать поведение программного приложения, описанного на языке программирования. Однако до конца 1990-х годов формальные методы, такие как метод B, могли быть реализованы только в научных исследованиях и не могли использоваться в промышленных приложениях. Цель этой книги - представить опыт использования формальных методов (таких как доказательства и проверка моделей) на промышленных примерах в области транспорта. Авторы книги - люди, которые в настоящее время занимаются созданием и оценкой безопасных системного программного обеспечения. Книга включает в себя множество примеров, а также фотографии и архитектурные планы, что делает ее особенно полезной для практикующих специалистов. В книге представлены такие темы, как SAET-METEOR, метод B и инструменты, модельно-ориентированное проектирование с использованием Simulink, инструмент доказательства SIMULINK DESIGN VERIFIER, SCADE (среда разработки безопасных приложений), GATeL: платформа для верификации и проверки моделей SCADE, а также ControlBuild - средство разработки для инженеров управления.
Книга "Формальные методы. Промышленное использование от модели до кода" представляет собой сборник опыта использования формальных методов в промышленных примерах в области транспорта. Формальные методы - это техники анализа программирования, позволяющие анализировать поведение программного приложения, описанного на языке программирования. Хотя такие методы уже довольно стары, их внедрение в промышленные приложения началось только в 1980-х годах. В конце 1990-х годов формальные методы и метод B стали доступны для использования в промышленных условиях.
Эта книга основана на опыте специалистов, занимающихся разработкой и оценкой программного обеспечения, имеющего критическое значение для безопасности. Участие представителей промышленности позволяет избежать проблем конфиденциальности и предоставить новую полезную информацию, такую как фотографии, архитектурные планы, реальные примеры и т. д.
В книге рассматриваются следующие темы: SAET-METEOR, метод B и инструменты B, модельно-ориентированное проектирование с использованием Simulink, инструмент доказательства правильности Simulink Design Verifier, реализация и применение SCADE (среда разработки приложений с повышенными требованиями к безопасности), GATeL: платформа верификации и валидации моделей SCADE и ControlBuild.
Книга предназначена для студентов и исследователей, а также для специалистов, работающих в области промышленного программного обеспечения, и предоставляет ценный опыт и практическую информацию о применении формальных методов в промышленной среде.
Электронная Книга «Formal Methods. Industrial Use from Model to the Code» написана автором Jean-Louis Boulanger в году.
Минимальный возраст читателя: 0
Язык: Английский
ISBN: 9781118614389
Описание книги от Jean-Louis Boulanger
Although formal analysis programming techniques may be quite old, the introduction of formal methods only dates from the 1980s. These techniques enable us to analyze the behavior of a software application, described in a programming language. It took until the end of the 1990s before formal methods or the B method could be implemented in industrial applications or be usable in an industrial setting. Current literature only gives students and researchers very general overviews of formal methods. The purpose of this book is to present feedback from experience on the use of “formal methods” (such as proof and model-checking) in industrial examples within the transportation domain. This book is based on the experience of people who are currently involved in the creation and evaluation of safety critical system software. The involvement of people from within the industry allows us to avoid the usual problems of confidentiality which could arise and thus enables us to supply new useful information (photos, architecture plans, real examples, etc.). Topics covered by the chapters of this book include SAET-METEOR, the B method and B tools, model-based design using Simulink, the Simulink design verifier proof tool, the implementation and applications of SCADE (Safety Critical Application Development Environment), GATeL: A V&V Platform for SCADE models and ControlBuild. Contents 1. From Classic Languages to Formal Methods, Jean-Louis Boulanger. 2. Formal Method in the Railway Sector the First Complex Application: SAET-METEOR, Jean-Louis Boulanger. 3. The B Method and B Tools, Jean-Louis Boulanger. 4. Model-Based Design Using Simulink – Modeling, Code Generation, Verification, and Validation, Mirko Conrad and Pieter J. Mosterman. 5. Proving Global Properties with the Aid of the SIMULINK DESIGN VERIFIER Proof Tool, Véronique Delebarre and Jean-Frédéric Etienne. 6. SCADE: Implementation and Applications, Jean-Louis Camus. 7. GATeL: A V&V Platform for SCADE Models, Bruno Marre, Benjamin Bianc, Patricia Mouy and Christophe Junke. 8. ControlBuild, a Development Framework for Control Engineering, Franck Corbier. 9. Conclusion, Jean-Louis Boulanger.
