Uppaal چیست؟

 Uppaal چیست؟



Uppaal چیست؟: برای نمایش گرافیکی ماشین های خودکار زمانی از ابزار UPPAAL استفاده می شود. UPPAAL ابزاری برای ارزیابی سیستم های بلادرنگ است که به طور مشترک توسط دانشگاه هایAalborg   و Uppsala طراحی شده است. این ابزار با موفقیت در مطالعاتی پیرامون پروتکل های ارتباطی برای برنامه های چند رسانه ای به کار برده شد. UPPAAL برای ارزیابی سیستم هایی طراحی شده است که قابل مدل سازی با متغیرهای صحیح، انواع ساختار داده ای و کانال های هم زمانی هستند. وارسی کننده مدل UPPAAL از تئوری ماشین خودکار زمانی پشتیبانی می کند. زبان پرس و جوی آن برای مشخص کردن خصوصیات مورد بررسی زیر مجموعه ای از CTL است. در  UPPAAL یک سیستم به عتوان شبکه ای از چندین ماشین خودکار زمانی موازی مدل می شود. زبان مدل سازی آن ترکیبات اضافی مثل متغیرهای صحیح کران دار و فوریت را ارائه می دهد (Uppaal چیست؟).

 Uppaal چیست؟


در UPPAAL کانال های نرمال و فوری متمایز وجود دارد. لبه های همگام شده توسط کانال نرمال وقتی که با گارد فعال شده باشند می توانند در زمان اختیاری گرقته شوند، اما لبه های همگام شده با کانال فوری باید به محض ممکن شدن گرفته شوند وقتی که یک لبه فوری فعال شود اجازه هیج توقفی در هیج زمانی وجود ندارد. مدل به کار رفته در UPPAAL شبکه ای از ماشین های خودکار زمانی همگام شده با کانال ها می باشد. بیان ویژگی ها در UPPAAL هدف اصلی وارسی کننده عدل، ارزیابی مدل در نیازمندی های مشخص شده است. نیازمندی ها باید به طور رسمی با یک زبان مشخصی بیان شود. زبان پرس و جو مشابه CTL شامل فرمول مسیر و فرمول حالت است. فرمول حالت، حالت های منحصر به فردی را توصیف می کند در حالی که فرمول مسیر بر روی مسیرها یا تعقیب های مدل بیان می شود. فرمول مسیر می تواند در دسترسی پذیری، امنیت و زنده ماندن رده بندی شود. در UPPAAL بن بست با یک فرمول حالت مخصوص بیان می شود. فرمولی شامل لغت  Deadlock بوده و برای تمام حالت های این بست برقرار میشود. یک حالت بن بست است اگر هیچ انتقال فعال خروجی از آن وجود نداشته باشد (Uppaal چیست؟).

دسترسی پذیری


ویژگی دسترسی پذیری ویژگی ساده ای است که سوال می کند: آیا با شروع از حالت اولیه مسیری وجود دارد که سرانجام φ در طول مسیر یرقرار شود. به عنوان نمونه وقتی مدلی از پروتکل های ارتباطی شامل یک فرستنده و گیرنده باشد، این ویژگی سوال می کند که آیا برای یک قرستنده امکان ارسال و یا برای دریافت کننده امکان دریافت وجود دارد. در UPPAAL  این ویژگی را با استفاده از نحو E<>φ می نویسیم (Uppaal چیست؟).

امنیت


ویژگی امنیت به این معنی است که بعضی اتفاقات بد هرگز رخ ندهد. در UPPAAL این ویژگی فرمول بندی شده است. یعضی اتفاقات خوب به طور ثابت درست است. φ را یک فرمول حالت در نظر می گیریم. بیان می کنیم که  φباید در تمام حالت های دسترس پذیر با فرمولی مسیر Aφ درست باشد، در حالیکه E◊φ می گوید باید یک مسیر حداکتری وجود داشته باشد که φ همیشه درست باشد. در UPPAAL یه ترتیب می نویسیم A[]φ  و E [] φ .

زنده ماندن


منظور از ویژگی زنده ماندن این است که بعضی اتفاقات سرانجام رخ می دهد. زنده ماندن در شکل ساده خود با فرمول مسیر A◊φ بیان می شود به این معنا که φ عاقبت برقرار می شود. شکل کاربردی تر آن ویژگی نتیجه گرفتن یا پاسخ است با نوشتن φ → ω که خوانده می شود هر وقت φ برقرار شود پس عاقبت ω برقرار خواهد شد. در UPPAAL این ویژگی ها به ترتیب به این صورت نوشته می شوند: A<>φ و φ −→ω. همچنین بیان این که در صورت برقرار بودن شرط خاصی φ برقرار است با استفاده از imply تعریف می شود (Uppaal چیست؟).