دانلود کتاب Handbook of model checking – کتابچه راهنمای بررسی مدل

• توضیحات
• نظرات (0)

Abstract: 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. ‘This handbook is an authoritative, comprehensive description of the state of the art in model checking. It belongs on the bookshelf of every researcher and practitioner in computer-aided verification.’ [Moshe Y. Vardi, George Distinguished Service Professor in Computational Engineering, Rice University] ‘With chapters written by the worlds leading experts from academia and industry, this authoritative book on model checking should be on the shelf of every computer science graduate student and every hardware and software engineer. As the scale and complexity of digital systems grow, and they must work in the presence of uncertainty in the physical world, verification techniques such as model checking will become increasingly important to ensure system reliability, safety, and security.’ [Jeannette Wing, Corporate Vice President, Microsoft Research]

————————————————————–

ترجمه ماشینی :

بررسی مدل یک روش به کمک کامپیوتر برای تجزیه و تحلیل سیستم های دینامیکی است که می تواند توسط سیستم های انتقال حالت مدل شود. بررسی مدل با برگرفته از سنت‌های تحقیقاتی در منطق ریاضی، زبان‌های برنامه‌نویسی، طراحی سخت‌افزار و علوم کامپیوتر نظری، اکنون به طور گسترده برای تأیید سخت‌افزار و نرم‌افزار در صنعت استفاده می‌شود. ویراستاران و نویسندگان این کتاب راهنما از جمله محققان پیشرو در این حوزه هستند و 32 فصل ارائه شده دیدگاه کاملی از منشاء، نظریه و کاربرد ارائه می کنند. بررسی مدل به طور خاص، ویراستاران پیشرفت‌ها در این حوزه و فصول کتاب راهنما را بر اساس دو موضوع تکراری طبقه‌بندی می‌کنند که بخش عمده‌ای از دستور کار تحقیق را هدایت کرده است: چالش الگوریتمی، یعنی طراحی الگوریتم‌های بررسی مدل که در مقیاس واقعی زندگی می‌کنند. چالش ها و مسائل؛ و چالش مدلسازی، یعنی گسترش فرمالیسم فراتر از ساختارهای کریپکی و منطق زمانی. این کتاب برای محققان و دانشجویان فارغ التحصیل درگیر با توسعه روش‌های رسمی و ابزار تأیید ارزشمند خواهد بود. این کتاب راهنمای جامع و معتبری از وضعیت هنر در بررسی مدل است. این کتاب در قفسه کتاب هر محقق و متخصص در راستی‌آزمایی به کمک رایانه قرار دارد. [Moshe Y. Vardi، جورج استاد خدمات ممتاز در مهندسی محاسبات، دانشگاه رایس] «با فصل‌هایی که توسط متخصصان برجسته جهان از دانشگاه و صنعت نوشته شده است، این کتاب معتبر در مورد بررسی مدل باید در قفسه هر دانشجوی فارغ‌التحصیل علوم کامپیوتر و هر دانشجو قرار گیرد. مهندس سخت افزار و نرم افزار. همانطور که مقیاس و پیچیدگی سیستم های دیجیتال رشد می کند، و آنها باید در حضور عدم قطعیت در دنیای فیزیکی کار کنند، تکنیک های راستی آزمایی مانند بررسی مدل برای اطمینان از قابلیت اطمینان، ایمنی و امنیت سیستم اهمیت فزاینده ای پیدا می کند. [Jeannette Wing، معاون شرکت، تحقیقات مایکروسافت]. بیشتر بخوانید…