روش‌های صوری: کاربرد صنعتی از مدل تا کد ۲۰۱۳
Formal Methods: Industrial Use from Model to the Code 2013

اگرچه تکنیک‌های برنامه‌نویسی تحلیل صوری قدمتی طولانی دارند، اما معرفی روش‌های صوری تنها به دهه 1980 بازمی‌گردد. این تکنیک‌ها به ما امکان می‌دهند رفتار یک برنامه نرم‌افزاری را که به زبان برنامه‌نویسی توصیف شده است، تجزیه و تحلیل کنیم. در اواخر دهه 1990 بود که روش‌های صوری یا روش B توانستند در کاربردهای صنعتی پیاده‌سازی شوند یا در یک محیط صنعتی قابل استفاده باشند.

ادبیات موجود، تنها دیدگاه‌های کلی بسیار عمومی از روش‌های صوری را به دانشجویان و محققان ارائه می‌دهد. هدف این کتاب ارائه بازخورد تجربی در مورد استفاده از “روش‌های صوری” (مانند اثبات و بررسی مدل) در نمونه‌های صنعتی در حوزه حمل و نقل است.

این کتاب بر اساس تجربه افرادی است که در حال حاضر در ایجاد و ارزیابی نرم‌افزار سیستم‌های حیاتی ایمنی دخیل هستند. مشارکت افراد از داخل صنعت به ما این امکان را می‌دهد که از مشکلات معمول محرمانگی که ممکن است بوجود آیند، جلوگیری کنیم و در نتیجه اطلاعات مفید جدید (عکس‌ها، نقشه‌های معماری، نمونه‌های واقعی و غیره) را ارائه دهیم.

مباحث پوشش داده شده توسط فصل‌های این کتاب شامل SAET-METEOR، روش B و ابزارهای B، طراحی مبتنی بر مدل با استفاده از Simulink، ابزار اثبات‌گر صحت طراحی Simulink، پیاده‌سازی و کاربردهای SCADE (محیط توسعه برنامه‌های حیاتی ایمنی)، GATeL: یک پلتفرم V&V برای مدل‌های SCADE و ControlBuild است.

فهرست مطالب

1. از زبان‌های کلاسیک تا روش‌های صوری، ژان لویی بولانژه.
2. روش صوری در بخش ریلی اولین کاربرد پیچیده: SAET-METEOR، ژان لویی بولانژه.
3. روش B و ابزارهای B، ژان لویی بولانژه.
4. طراحی مبتنی بر مدل با استفاده از Simulink – مدل‌سازی، تولید کد، تأیید و اعتبارسنجی، میرکو کنراد و پیتر جی. موسترمن.
5. اثبات ویژگی‌های سراسری با کمک ابزار اثبات‌گر صحت طراحی SIMULINK، ورونیک دولبار و ژان فردریک اتین.
6. SCADE: پیاده‌سازی و کاربردها، ژان لویی کامو.
7. GATeL: یک پلتفرم V&V برای مدل‌های SCADE، برونو مار، بنجامین بیانک، پاتریشیا مویی و کریستوف یونکه.
8. ControlBuild، یک چارچوب توسعه برای مهندسی کنترل، فرانک کوربیه.
9. نتیجه‌گیری، ژان لویی بولانژه.

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.