مقدمه‌ای بر روش‌های صوری عملی با استفاده از منطق زمانی ۲۰۱۱
An Introduction to Practical Formal Methods Using Temporal Logic 2011

اصطلاح “منطق زمانی” ممکن است پیچیده و دلهره‌آور به نظر برسد؛ اما در حالی که سناریوهای بالقوه پیچیده‌ای را توصیف می‌کنند، منطق‌های زمانی اغلب بر اساس چند مفهوم ساده و اساسی بنا شده‌اند – که در این کتاب برجسته شده‌اند. *مقدمه‌ای بر روش‌های صوری عملی با استفاده از منطق زمانی* مقدمه‌ای بر روش‌های صوری مبتنی بر منطق زمانی برای توسعه و آزمایش سیستم‌های محاسباتی پیچیده ارائه می‌دهد. این روش‌ها توسط بسیاری از ابزارها، تکنیک‌ها و نتایج توسعه‌یافته پشتیبانی می‌شوند که می‌توانند در طیف گسترده‌ای از سیستم‌ها اعمال شوند.

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

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

The name “temporal logic” may sound complex and daunting; but while they describe potentially complex scenarios, temporal logics are often based on a few simple, and fundamental, concepts – highlighted in this book. An Introduction to Practical Formal Methods Using Temporal Logic provides an introduction to formal methods based on temporal logic, for developing and testing complex computational systems. These methods are supported by many well-developed tools, techniques and results that can be applied to a wide range of systems.

Fisher begins with a full introduction to the subject, covering the basics of temporal logic and using a variety of examples, exercises and pointers to more advanced work to help clarify and illustrate the topics discussed. He goes on to describe how this logic can be used to specify a variety of computational systems, looking at issues of linking specifications, concurrency, communication and composition ability. He then analyses temporal specification techniques such as deductive verification, algorithmic verification, and direct execution to develop and verify computational systems. The final chapter on case studies analyses the potential problems that can occur in a range of engineering applications in the areas of robotics, railway signalling, hardware design, ubiquitous computing, intelligent agents, and information security, and explains how temporal logic can improve their accuracy and reliability.

• Models temporal notions and uses them to analyze computational systems
• Provides a broad approach to temporal logic across many formal methods – including specification, verification and implementation
• Introduces and explains freely available tools based on temporal logics and shows how these can be applied
• Presents exercises and pointers to further study in each chapter, as well as an accompanying website providing links to additional systems based upon temporal logic as well as additional material related to the book.