Model Checking Software: 9th International SPIN Workshop Grenoble, France, April 11–13, 2002 Proceedings

مجموعه کارگاه آموزشی SPIN محققین و متخصصینی را گرد هم می‌آورد که علاقه‌مند به فناوری بررسی مدل وضعیت صریح هستند، زیرا برای تأیید سیستم‌های نرم‌افزاری به کار می‌رود. از سال 1995، زمانی که مجموعه کارگاه های SPIN ایجاد شد، کارگاه های آموزشی SPIN به صورت سالانه در Montr'eal (1995)، نیوبرانزویک (1996)، Enschede (1997)، پاریس (1998)، ترنتو (1999)، تولوز برگزار می شود. (1999)، استنفورد (2000) و تورنتو (2001). در حالی که اولین کارگاه SPIN یک رویداد مستقل بود، بعداً کارگاه‌ها به‌عنوان رویدادهای بیشتر یا بدون نزدیک به کنفرانس‌های بزرگ‌تر، به ویژه با CAV (1996)، TACAS (1997)، FORTE/PSTV (1998)، FLOC (1999)، کنگره جهانی (MO109t)، کنگره جهانی (MO109) برگزار شد. و ICSE (2001). امسال، SPIN 2002 به عنوان یک رویداد ماهواره ای ETAPS 2002، کنفرانس مشترک اروپایی در نظریه و عمل نرم افزار برگزار شد. هم‌محلی کارگاه‌های SPIN با کنفرانس‌ها بسیار موفق بوده و به انتشار فناوری بررسی مدل SPIN به مخاطبان گسترده‌تری کمک کرده است. از سال 1999، مجموعه مقالات کارگاه های SPIN در مجموعه "یادداشت های سخنرانی در علوم کامپیوتر" Springer-Verlag ظاهر شده است. تاریخچه کارگاه‌های موفق SPIN شاهدی بر بلوغ فناوری بررسی مدل، نه تنها در حوزه سخت‌افزار، بلکه به طور فزاینده‌ای در حوزه نرم‌افزاری است. در حالی که در سال‌های قبل الگوریتم‌ها و توسعه ابزار 1 پیرامون جستجوگر مدل SPIN تمرکز این سری کارگاه بود، این حوزه اخیراً گسترده شده است تا شامل رویکردهای عمومی برای بررسی مدل نرم‌افزار باشد. تحقیقات کنونی در این زمینه چندان بر روی تأیید کامل مدل‌های سیستم تمرکز نمی‌کند، بلکه به تجزیه و تحلیل کد منبع برای کشف خطاهای نرم‌افزار کمک می‌کند.

The SPIN workshop series brings together researchers and practitioners int- ested in explicit state model checking technology as it is applied to the veri?- tion of software systems. Since 1995, when the SPIN workshop series was instigated, SPIN workshops have been held on an annual basis at Montr´ eal (1995), New Brunswick (1996), Enschede (1997), Paris (1998), Trento (1999), Toulouse (1999), Stanford (2000), andToronto(2001). Whilethe?rstSPINworkshopwasastand-aloneevent,later workshopshavebeenorganizedasmoreorlesscloselya?liatedeventswithlarger conferences, in particular with CAV (1996), TACAS (1997), FORTE/PSTV (1998), FLOC (1999), World Congress on Formal Methods (1999), FMOODS (2000), and ICSE (2001). This year, SPIN 2002 was held as a satellite event of ETAPS 2002, the European Joint Conferences on Theory and Practice of Software. The co-location of SPIN workshops with conferences has proven to be very successful and has helped to disseminate SPIN model checking technology to wider audiences. Since 1999, the proceedings of the SPIN workshops have appeared in Springer-Verlag’s “Lecture Notes in Computer Science” series. The history of successful SPIN workshops is evidence for the maturing of model checking technology, not only in the hardware domain, but increasingly also in the software area. While in earlier years algorithms and tool development 1 around the SPIN model checker were the focus of this workshop series, the scopehasrecentlywidenedtoincludemoregeneralapproachestosoftwaremodel checking. Current research in this area concentrates not so much on completely verifyingsystemmodels,butratheronanalyzingsourcecodeinordertodiscover software faults.