Our growing dependence on increasingly complex computer and software systems necessitates the development of formalisms, techniques, and tools for assessing functional properties of these systems. One such technique that has emerged in the last twenty years is model checking, which systematically (and automatically) checks whether a model of a given system satisfies a desired property such as deadlock freedom, invariants, or request-response properties. This automated technique for verification and debugging has developed into a mature and widely used approach with many applications. Principles of Model Checking offers a comprehensive introduction to model checking that is not only a text suitable for classroom use but also a valuable reference for researchers and practitioners in the field. The book begins with the basic principles for modeling concurrent and communicating systems, introduces different classes of properties (including safety and liveness), presents the notion of fairness, and provides automata-based algorithms for these properties. It introduces the temporal logics LTL and CTL, compares them, and covers algorithms for verifying these logics, discussing real-time systems as well as systems subject to random phenomena. Separate chapters treat such efficiency-improving techniques as abstraction and symbolic manipulation. The book includes an extensive set of examples (most of which run through several chapters) and a complete set of basic results accompanied by detailed proofs. Each chapter concludes with a summary, bibliographic notes, and an extensive list of exercises of both practical and theoretical nature.
ترجمه فارسی (ترجمه ماشینی)
وابستگی فزاینده ما به سیستمهای رایانهای و نرمافزاری که به طور فزاینده پیچیدهتر میشوند، توسعه فرمالیسمها، تکنیکها و ابزارهایی را برای ارزیابی ویژگیهای عملکردی این سیستمها ضروری میکند. یکی از این تکنیکها که در بیست سال گذشته پدیدار شده است، بررسی مدل است، که به طور سیستماتیک (و خودکار) بررسی میکند که آیا یک مدل از یک سیستم معین ویژگی مورد نظر مانند آزادی بنبست، متغیرها، یا ویژگیهای درخواست پاسخ را برآورده میکند یا خیر. این تکنیک خودکار برای تأیید و اشکال زدایی به یک رویکرد بالغ و پرکاربرد با کاربردهای بسیاری تبدیل شده است. اصول بررسی مدل مقدمه ای جامع برای بررسی مدل ارائه می دهد که نه تنها متنی مناسب برای استفاده در کلاس درس است، بلکه یک مرجع ارزشمند برای محققان و متخصصان در این زمینه است. این کتاب با اصول اولیه مدلسازی سیستمهای همزمان و ارتباطی آغاز میشود، کلاسهای مختلف ویژگیها (از جمله ایمنی و زنده بودن) را معرفی میکند، مفهوم عدالت را ارائه میکند و الگوریتمهای مبتنی بر خودکار را برای این ویژگیها ارائه میکند. این منطقهای زمانی LTL و CTL را معرفی میکند، آنها را با هم مقایسه میکند، و الگوریتمهایی را برای تأیید این منطقها پوشش میدهد، در مورد سیستمهای بلادرنگ و همچنین سیستمهایی که در معرض پدیدههای تصادفی هستند بحث میکند. فصلهای جداگانهای چنین تکنیکهای بهبود کارایی را مانند انتزاع و دستکاری نمادین در نظر میگیرند. این کتاب شامل مجموعه گسترده ای از مثال ها (که اکثر آنها در چندین فصل هستند) و مجموعه کاملی از نتایج اساسی همراه با شواهد دقیق است. هر فصل با خلاصه، یادداشت های کتابشناختی، و فهرست گسترده ای از تمرین ها با ماهیت عملی و نظری به پایان می رسد.
نقد و بررسیها
هنوز بررسیای ثبت نشده است.