Formal Methods: Industrial Use from Model to the Code

ویرایش:  
نویسندگان: Jean-Louis Boulanger (ed.)  
سری:  
ISBN (شابک) : 9781848213623, 9781118561898 
ناشر: Wiley-ISTE 
سال نشر: 2012 
تعداد صفحات: 364 
زبان: English 
فرمت فایل : PDF (درصورت درخواست کاربر به PDF، EPUB یا AZW3 تبدیل می شود) 
حجم فایل: 10 مگابایت 

قیمت کتاب (تومان) : 32,000



اگرچه تکنیک‌های برنامه‌نویسی تحلیل رسمی ممکن است بسیار قدیمی باشند، معرفی روش‌های رسمی فقط به دهه 1980 برمی‌گردد. این تکنیک‌ها ما را قادر می‌سازند تا رفتار یک نرم‌افزار را که در یک زبان برنامه‌نویسی توصیف شده است، تجزیه و تحلیل کنیم. تا پایان دهه 1990 طول کشید تا روش‌های رسمی یا روش B بتوانند در کاربردهای صنعتی پیاده‌سازی شوند یا در محیط‌های صنعتی قابل استفاده باشند.
مطابقات کنونی فقط دیدگاه‌های کلی بسیار کلی از روش‌های رسمی را به دانشجویان و محققان می‌دهد. هدف این کتاب ارائه بازخورد تجربه در مورد استفاده از "روش های رسمی" (مانند اثبات و بررسی مدل) در نمونه های صنعتی در حوزه حمل و نقل است.
این کتاب بر اساس تجربه افرادی است که در حال حاضر در ایجاد و ارزیابی نرم افزار سیستم حیاتی ایمنی شرکت دارند. مشارکت افراد در داخل صنعت به ما امکان می دهد از مشکلات معمول محرمانگی که ممکن است ایجاد شود اجتناب کنیم و بنابراین ما را قادر می سازد اطلاعات مفید جدیدی (عکس ها، نقشه های معماری، نمونه های واقعی و غیره) ارائه کنیم.
موضوعات تحت پوشش فصول این کتاب شامل SAET-METEOR، روش B و ابزارهای B، طراحی مبتنی بر مدل با استفاده از Simulink، ابزار اثبات طراحی Simulink، پیاده‌سازی و کاربردهای SCADE (محیط توسعه برنامه‌های حیاتی ایمنی)، GATeL: A V&V Platform برای مدل‌های SCADE و ControlBuild.

محتوا

1. از زبان‌های کلاسیک تا روش‌های رسمی، ژان لوئیس بولانژر.
2. روش رسمی در بخش راه آهن اولین کاربرد پیچیده: SAET-METEOR، Jean-Louis Boulanger.
3. روش B و ابزار B، ژان لوئیس بولانگر.
4. طراحی مبتنی بر مدل با استفاده از سیمولینک – مدل‌سازی، تولید کد، تأیید، و اعتبارسنجی، میرکو کنراد و پیتر جی. موسترمن.
5. اثبات خواص جهانی با کمک ابزار اثبات SIMULINK DESIGN VERIFIER، Veronique Delebarre و Jean-Frederic Etienne.
6. SCADE: پیاده سازی و کاربردها، ژان لوئی کامو.
7. GATEL: یک پلتفرم V&V برای مدل‌های SCADE، برونو مار، بنجامین بیانک، پاتریشیا موی و کریستوف جونک.
8. ControlBuild، یک چارچوب توسعه برای مهندسی کنترل، فرانک کوربیه.
9. نتیجه‌گیری، ژان لوئیس بولانگر.

محتوا:
فصل 1 از زبان‌های کلاسیک تا روش‌های رسمی (صفحه‌های 1-54): Jean?louis Boulanger
فصل 2 روش رسمی در بخش راه‌آهن اولین کاربرد پیچیده : SAET?METEOR (صفحات 55-125): Jean?Louis Boulanger
فصل 3 روش B و ابزار B (صفحات 127-157): Jean?Louis Boulanger
مدل فصل 4؟ طراحی مبتنی بر سیمولینک - مدلسازی ، تولید کد، تأیید، و اعتبارسنجی (صفحات 159-181): میرکو کنراد و پیتر جی. موسترمن
فصل 5 اثبات خواص جهانی با کمک ابزار اثبات SIMULINK DESIGN VERIFIER (صفحات 183-223): Veronique Delebarre و Jean?Frederic Etienne
فصل 6 SCADE: پیاده سازی و کاربردها (صفحه های 225-271): Jean?Louis Camus
فصل 7 GATeL: یک پلت فرم V&V برای مدل های SCADE (صفحات 273-285): برونو مار، بنجامین بینک ، پاتریشیا موی و کریستف یونکه
فصل 8 ControlBuild، چارچوب توسعه ای برای مهندسی کنترل (صفحات 287-324): فرانک کوربیه
فصل 9 ادامه جمع بندی (صفحات 325-343): ژان لوئیس بولانجر

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, Veronique Delebarre and Jean-Frederic 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.

Content:
Chapter 1 From Classic Languages to Formal Methods (pages 1–54): Jean?louis Boulanger
Chapter 2 Formal Method in the Railway Sector the First Complex Application: SAET?METEOR (pages 55–125): Jean?Louis Boulanger
Chapter 3 The B Method and B Tools (pages 127–157): Jean?Louis Boulanger
Chapter 4 Model?Based Design Using Simulink – Modeling, Code Generation, Verification, and Validation (pages 159–181): Mirko Conrad and Pieter J. Mosterman
Chapter 5 Proving Global Properties with the Aid of the SIMULINK DESIGN VERIFIER Proof Tool (pages 183–223): Veronique Delebarre and Jean?Frederic Etienne
Chapter 6 SCADE: Implementation and Applications (pages 225–271): Jean?Louis Camus
Chapter 7 GATeL: A V&V Platform for SCADE Models (pages 273–285): Bruno Marre, Benjamin Bianc, Patricia Mouy and Christophe Junke
Chapter 8 ControlBuild, a Development Framework for Control Engineering (pages 287–324): Franck Corbier
Chapter 9 Conclusion (pages 325–343): Jean?Louis Boulanger