Designing Reliable Distributed Systems: A Formal Methods Approach Based on Executable Modeling in Maude

ویرایش: 1 
نویسندگان: Peter Csaba Ölveczky (auth.)  
سری: Undergraduate Topics in Computer Science 
ISBN (شابک) : 9781447166863, 9781447166870 
ناشر: Springer-Verlag London 
سال نشر: 2017 
تعداد صفحات: 326 
زبان: English 
فرمت فایل : PDF (درصورت درخواست کاربر به PDF، EPUB یا AZW3 تبدیل می شود) 
حجم فایل: 4 مگابایت 

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



این کتاب درسی تست شده در کلاس درس مقدمه ای در دسترس برای طراحی، مدل سازی رسمی و تجزیه و تحلیل سیستم های کامپیوتری توزیع شده ارائه می دهد. این کتاب از Maude، یک زبان مبتنی بر منطق بازنویسی و ابزار شبیه‌سازی و بررسی مدل استفاده می‌کند که فرمالیسم مدل‌سازی ساده و شهودی را ارائه می‌کند که برای مدل‌سازی سیستم‌های توزیع‌شده در یک سبک برنامه‌نویسی شی‌گرا و کاربردی جذاب است.

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

این کتاب درسی مستقل برای پشتیبانی از دوره‌های کارشناسی در مورد روش‌های رسمی و سیستم‌های توزیع‌شده طراحی شده است و برای هر دانشجویی که به‌دنبال آشنایی خواننده‌پسند با مشخصات رسمی، منطق و سیستم‌های استنتاج، و تکنیک‌های بررسی مدل خودکار است، ارزشمند خواهد بود.

This classroom-tested textbook provides an accessible introduction to the design, formal modeling, and analysis of distributed computer systems. The book uses Maude, a rewriting logic-based language and simulation and model checking tool, which offers a simple and intuitive modeling formalism that is suitable for modeling distributed systems in an attractive object-oriented and functional programming style.

Topics and features: introduces classical algebraic specification and term rewriting theory, including reasoning about termination, confluence, and equational properties; covers object-oriented modeling of distributed systems using rewriting logic, as well as temporal logic to specify requirements that a system should satisfy; provides a range of examples and case studies from different domains, to help the reader to develop an intuitive understanding of distributed systems and their design challenges; examples include classic distributed systems such as transport protocols, cryptographic protocols, and distributed transactions, leader election, and mutual execution algorithms; contains a wealth of exercises, including larger exercises suitable for course projects, and supplies executable code and supplementary material at an associated website.

This self-contained textbook is designed to support undergraduate courses on formal methods and distributed systems, and will prove invaluable to any student seeking a reader-friendly introduction to formal specification, logics and inference systems, and automated model checking techniques.

Front Matter ....Pages i-xviii
 Introduction  (Peter Csaba Ölveczky)....Pages 1-8
Front Matter ....Pages 9-9
 Equational Specification in Maude  (Peter Csaba Ölveczky)....Pages 11-58
 Operational Semantics of Equational Specifications  (Peter Csaba Ölveczky)....Pages 59-66
 Termination  (Peter Csaba Ölveczky)....Pages 67-84
 Confluence  (Peter Csaba Ölveczky)....Pages 85-91
 Equational Logic  (Peter Csaba Ölveczky)....Pages 93-108
 Models of Equational Specifications  (Peter Csaba Ölveczky)....Pages 109-124
Front Matter ....Pages 125-125
 Modeling Distributed Systems in Rewriting Logic  (Peter Csaba Ölveczky)....Pages 127-144
 Executing Rewriting Logic Specifications in Maude  (Peter Csaba Ölveczky)....Pages 145-154
 Concurrent Objects in Maude  (Peter Csaba Ölveczky)....Pages 155-182
 Modeling Communication in Maude  (Peter Csaba Ölveczky)....Pages 183-198
 Modeling and Analyzing Transport Protocols  (Peter Csaba Ölveczky)....Pages 199-210
 Distributed Algorithms  (Peter Csaba Ölveczky)....Pages 211-232
 Analyzing a Cryptographic Protocol  (Peter Csaba Ölveczky)....Pages 233-248
 System Requirements  (Peter Csaba Ölveczky)....Pages 249-262
 Formalizing and Checking Requirements  (Peter Csaba Ölveczky)....Pages 263-282
 Real-Time and Probabilistic Systems  (Peter Csaba Ölveczky)....Pages 283-298
Back Matter ....Pages 299-313