Handbook of Model Checking

ویرایش:  
نویسندگان: Edmund M. Clarke,  Thomas A. Henzinger,  Helmut Veith,  Roderick Bloem (eds.)  
سری:  
ISBN (شابک) : 3319105744, 9783319105741 
ناشر: Springer 
سال نشر: 2018 
تعداد صفحات: 1201 
زبان: English 
فرمت فایل : PDF (درصورت درخواست کاربر به PDF، EPUB یا AZW3 تبدیل می شود) 
حجم فایل: 11 مگابایت 

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



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

< p> ویراستاران و نویسندگان این کتاب راهنما از جمله محققان برجسته جهان در این حوزه هستند و 32 فصل ارائه شده نمای کاملی از منشاء، نظریه و کاربرد بررسی مدل ارائه می‌دهند. به طور خاص، ویراستاران پیشرفت‌ها در این حوزه و فصل‌های کتاب راهنما را بر اساس دو موضوع تکراری که بخش عمده‌ای از دستور کار تحقیق را هدایت کرده‌اند، طبقه‌بندی می‌کنند: چالش الگوریتمی، یعنی طراحی الگوریتم‌های بررسی مدل که در مقیاس واقعی زندگی می‌کنند. چالش ها و مسائل؛ و چالش مدل‌سازی، یعنی گسترش فرمالیسم فراتر از ساختارهای کریپکی و منطق زمانی.

این کتاب برای محققان و دانشجویان فارغ‌التحصیل درگیر با توسعه روش‌های رسمی و ابزارهای تأیید ارزشمند خواهد بود.

Model checking is a computer-assisted method for the analysis of dynamical systems that can be modeled by state-transition systems. Drawing from research traditions in mathematical logic, programming languages, hardware design, and theoretical computer science, model checking is now widely used for the verification of hardware and software in industry.

The editors and authors of this handbook are among the world's leading researchers in this domain, and the 32 contributed chapters present a thorough view of the origin, theory, and application of model checking. In particular, the editors classify the advances in this domain and the chapters of the handbook in terms of two recurrent themes that have driven much of the research agenda: the algorithmic challenge, that is, designing model-checking algorithms that scale to real-life problems; and the modeling challenge, that is, extending the formalism beyond Kripke structures and temporal logic.

The book will be valuable for researchers and graduate students engaged with the development of formal methods and verification tools.