دسترسی نامحدود
برای کاربرانی که ثبت نام کرده اند
برای ارتباط با ما می توانید از طریق شماره موبایل زیر از طریق تماس و پیامک با ما در ارتباط باشید
در صورت عدم پاسخ گویی از طریق پیامک با پشتیبان در ارتباط باشید
برای کاربرانی که ثبت نام کرده اند
درصورت عدم همخوانی توضیحات با کتاب
از ساعت 7 صبح تا 10 شب
دسته بندی: ژنتیک ویرایش: 1 نویسندگان: John Rushby (auth.), Dennis Dams, Rob Gerth, Stefan Leue, Mieke Massink (eds.) سری: Lecture Notes in Computer Science 1680 ISBN (شابک) : 3540664998, 9783540664994 ناشر: Springer-Verlag Berlin Heidelberg سال نشر: 1999 تعداد صفحات: 293 زبان: English فرمت فایل : PDF (درصورت درخواست کاربر به PDF، EPUB یا AZW3 تبدیل می شود) حجم فایل: 2 مگابایت
کلمات کلیدی مربوط به کتاب جنبه های نظری و عملی بررسی مدل اسپین: 5 و ششمین کارگاه بین المللی SPIN ترنتو ، ایتالیا ، 5 ژوئیه 1999 تولوز ، فرانسه ، 21 و 24 سپتامبر 1999 مجموعه مقالات: منطق و معانی برنامه ها، مهندسی نرم افزار، زبان های برنامه نویسی، کامپایلرها، مترجمان
در صورت تبدیل فایل کتاب 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 به فرمت های PDF، EPUB، AZW3، MOBI و یا DJVU می توانید به پشتیبان اطلاع دهید تا فایل مورد نظر را تبدیل نمایند.
توجه داشته باشید کتاب جنبه های نظری و عملی بررسی مدل اسپین: 5 و ششمین کارگاه بین المللی SPIN ترنتو ، ایتالیا ، 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 در امکان ساخت ابزارهای اعتبار سنجی \" فشار دکمه\" نهفته است. وقتی فضای حالت 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.
Integrated Formal Verification: Using Model Checking with Automated Abstraction, Invariant Generation, and Theorem Proving....Pages 1-11
Runtime Efficient State Compaction in Spin....Pages 12-21
Distributed-Memory Model Checking with SPIN....Pages 22-39
Partial Order Reduction in Presence of Rendez-vous Communications with Unless Constructs and Weak Fairness....Pages 40-56
Divide, Abstract, and Model-Check....Pages 57-76
The Engineering of a Model Checker: the Gnu i-Protocol Case Study Revisited.....Pages 232-244
Embedding a Dialect of SDL in PROMELA....Pages 245-260
dSPIN: A Dynamic Extension of SPIN....Pages 261-276
Model Checking for Managers....Pages 92-107
Xspin/Project - Integrated Validation Management for Xspin....Pages 108-119
Analyzing Mode Confusion via Model Checking....Pages 120-135
Detecting Feature Interactions in the Terrestrial Trunked Radio (TETRA) Network Using Promela and Xspin....Pages 136-151
Java PathFinder A Translator from Java to Promela....Pages 152-152
VIP: A Visual Interface for Promela....Pages 153-153
Events in Property Patterns....Pages 154-167
Assume-Guarantee Model Checking of Software: A Comparative Case Study....Pages 168-183
A Framework for Automatic Construction of Abstract Promela Models....Pages 184-199
Model Checking Operator Procedures....Pages 200-215
Applying Model Checking in Java Verification....Pages 216-231
Formal Methods Adoption: What’s Working, What’s Not!....Pages 77-91