تولید قوانین راستی آزمایی از توصیف های آتاماتای زماندار

تولید قوانین راستی آزمایی نرم افرار از روی توصیف مسئله، از مسائل مطرح در مهندسی نرم افزار است. از آنجا که آتاماتای زماندار یکی از روش های رسمی و توانمند در توصیف یک مسئله با قیود زمانی است، ما در این مقاله به ارائه روشی می-پردازیم که به وسیله آن می توان از توصیف های آتاماتای زماندار، قوانین راستی آزمایی را تولید کرد. این قوانین برای راستی آزمایی رفتار نرم افزاری که از روی توصیف مسئله ساخته می شود، استفاده می شود تا رفتار مخاطره آمیز نرم افزار را اعلام کند. روش ما سه مرحله دارد: (۱) برای هر مولفه آتاماتای زماندار که مجموعه ای از حالات و گذارهای بامعنای آتاماتا را مشخص می کند، یک گزاره بر حسب حساب رخداد تولید می کنیم، (۲) گراف دسترسی حالات آتاماتای زماندار به دست می آوریم که در آن ترکیب مخاطره آمیز حالات مشخص شده است، (۳) برای هر ترکیب مخاطره آمیز حالات، یک گزاره بر حسب حساب رخداد با توجه به گزاره های بند ۱ تعیین  می کنیم. این گزاره ها، قوانین راستی آزمایی را تشکیل می دهند. در خاتمه با طرح یک مسئله، استفاده از روش فوق الذکر را در تولید قوانین راستی آزمایی نشان می دهیم.

کلمات کلیدی

• آتاماتای زماندار
• راستی آزمایی وارسی نرم افزار
• نرم افزار حساس به ایمنی