Abstract
The paper deals with the issue of the verification of communication protocols based on integration of formal methods chosen (coloured Petri nets). A method is proposed, that uses the coloured petri net for protocol specification, and transformation rules for a translation of the specification into a Petri net while preserving the semantics of the specification. Coloured Petri nets are well-known formal method for their analytical power to deal with a problem of protocol verification: invariant, reachability, deadlock and liveness analysis. Elements of theory behind the method are sketched in a short way. The method is illuminated by an example: RSVP Resource Reservation Protocol
چکیده
مقاله در مورد مشکلات تایید پروتکل های ارتباطی مبنی بر ادغام رسمی متد های انتخابی(شبکه های پتری رنگی) بحث می‌کند. متدی ارائه شده است، که از شبکه های رنگی پتری برای مشخصات پروتکل و انتقال قوانین استفاده می کند، جهت انتقال مشخصات به یک شبکه پتری در حالی که مشخصات معنایی حفظ می‌شود. شبکه های پتری رنگی یک متد رسمی شناخته شده برای تحلیل مشکل تایید پروتکل است: ثابت، قابل دسترسی، بن بست و آنالیز زنده بودن. عناصر تئوری متد در یک روش کوتاه مطرح شده است. این متد با یک مثال بیان می شود: پروتکل رزرو منابع RSVP.
کلمات کلیدی : تایید پروتکل، شبکه‌های پتری رنگی، RSVP
1-مقدمه
تایید عملکرد و آنالیزهای اجرایی برای طراحی پروتکل های موثر و کارآمد بسیار قابل توجه است. تایید عملکرد بر روی چک کردن طراحی پروتکل تمرکز دارد و معمولا با یک مدل رسمی مشخص می شود، الزامات عملکردی پروتکل‌های شبکه به دقت و کافی برآورد می‌شود.در حالیکه آنالیزهای اجرای روی ارزیابی طراحی پروتکل تمرکز دارد. هر دوی آنها نیاز به مدلهای قطعی به عنوان مشخصه‌ای انتزاعی از رفتارهای پروتکل کاربردی یا ویژگی‌های اجرایی، و همچنین به عنوان پایه های مربوط به آنالیزها دارند. به هر حال، در بیشتر پروژه های مهندسی پروتکل و تحقیقات مربوط به آن، تایید عملکرد و آنالیزهای اجرایی با مدلهای مستقل تطبیق می‌دهند به عنوان مثال اتومات‌های محدود برای تایید کاربردی و مدل فرایندی تصادفی برای ارزیابی اجرایی. نقطه ضعف اصلی استفاده از این دو مدل نا همگن این است که آنالیز اجرایی معتبر نیست حتی اگر به درستی رفتارهای عملکردی پروتکل‌ها مشخص شده باشد؛ بهبود عملکرد با تضمین قابلیت درستی و صحت آن نمی‌تواند صدق کند. بنابراین، استفاده از مدلهای مرتبط برای تائید عملکردی و آنالیز اجرایی ارزش مطالعات عمیق در این زمینه را دارد. در سال‌‌‌های اخیر، مطالعات اندکی در این زمینه انجام شده است. اغلب این مطالعات برروی استفاده مستقیم از فناوری‌های تائید برای حمایت کردن از آنالیز اجرایی بدون توجه به درستی تایید عملکردی و تنها با استفاده از یک مدل احتمالی رسمی متمرکز شده است...