دانلود کتاب Theoretical and Practical Aspects of SPIN Model Checking: 5th and 6th International SPIN Workshops Trento, Italy, July 5, 1999 Toulouse, France, September 21 and 24, 1999 Proceedings (به فارسی: جنبه های نظری و عملی بررسی مدل اسپین: پنجمین و ششمین کارگاه بین المللی اسپین ترنتو، ایتالیا، 5 ژوئیه 1999 تولوز، فرانسه، 21 و 24 سپتامبر 1999 مجموعه مقالات) نوشته شده توسط «John Rushby (auth.) – Dennis Dams – Rob Gerth – Stefan Leue – Mieke Massink (eds.)»
اطلاعات کتاب جنبه های نظری و عملی بررسی مدل اسپین: پنجمین و ششمین کارگاه بین المللی اسپین ترنتو، ایتالیا، 5 ژوئیه 1999 تولوز، فرانسه، 21 و 24 سپتامبر 1999 مجموعه مقالات
موضوع اصلی: ژنتیک
نوع: کتاب الکترونیکی
ناشر: Springer-Verlag Berlin Heidelberg
نویسنده: John Rushby (auth.) – Dennis Dams – Rob Gerth – Stefan Leue – Mieke Massink (eds.)
زبان: English
فرمت کتاب: pdf (قابل تبدیل به سایر فرمت ها)
سال انتشار: 1999
تعداد صفحه: 282
حجم کتاب: 3 مگابایت
کد کتاب: 3540664998 , 9783540664994
نوبت چاپ: 1
توضیحات کتاب جنبه های نظری و عملی بررسی مدل اسپین: پنجمین و ششمین کارگاه بین المللی اسپین ترنتو، ایتالیا، 5 ژوئیه 1999 تولوز، فرانسه، 21 و 24 سپتامبر 1999 مجموعه مقالات
افزایش اطمینان طراح به اینکه یک نرم افزار یا سخت افزار منطبق با مشخصات آن است، به یک هدف کلیدی در فرآیند طراحی برای سیستم های نرم افزاری و سخت افزاری تبدیل شده است. رویکردهای بسیاری برای رسیدن به این هدف توسعه یافته است، از جمله مشخصات دقیق، تأیید رسمی، اعتبارسنجی خودکار و آزمایش. بررسی مدل حالت محدود، همانطور که توسط بررسی کننده مدل حالت صریح SPIN پشتیبانی می‌شود، از محبوبیت دائمی در تأیید ویژگی خودکار سیستم‌های مبتنی بر پیام همزمان برخوردار است. SPIN در بخش‌های بزرگی توسط جرارد هومان پیاده‌سازی شده و نگهداری می‌شود و به‌طور رایگان از طریق ftp fromnetlib.bell-labs.comor از آدرس http://cm.bell-labs.com/cm/cs/what/ در دسترس است. spin/Man/README.html. زیبایی بررسی مدل nite-state در امکان ساخت ابزارهای اعتبارسنجی push-button نهفته است. وقتی فضای حالت nite باشد، پیمایش فضای حالت در نهایت با یک حکم قطعی در مورد خاصیتی که در حال تأیید اعتبار است خاتمه می یابد. به همان اندازه مفید این واقعیت است که در صورت احراز ویژگی، بررسی‌کننده مدل یک مثال متقابل را برمی‌گرداند، ویژگی که شناسایی خطا را بسیار تسهیل می‌کند. فضا بزرگ است و نوع ویژگی‌هایی که می‌توانند تأیید شوند محدود به منطقی با بیان نسبتاً محدود است.
Increasing the designer’s con dence that a piece of software or hardwareis c- pliant with its speci cation has become a key objective in the design process for software and hardware systems. Many approaches to reaching this goal have been developed, including rigorous speci cation, formal veri cation, automated validation, and testing. Finite-state model checking, as it is supported by the explicit-state model checkerSPIN,is enjoying a constantly increasingpopularity in automated property validation of concurrent, message based systems. SPIN has been in large parts implemented and is being maintained by Gerard Ho- mann, and is freely available via ftp fromnetlib.bell-labs.comor from URL http://cm.bell-labs.com/cm/cs/what/spin/Man/README.html. The beauty of nite-state model checking lies in the possibility of building push-button” validation tools. When the state space is nite, the state-space traversal will eventually terminate with a de nite verdict on the property that is being validated. Equally helpful is the fact that in case the property is inv- idated the model checker will return a counterexample, a feature that greatly facilitates fault identi cation. On the downside, the time it takes to obtain a verdict may be very long if the state space is large and the type of properties that can be validated is restricted to a logic of rather limited expressiveness.
