سیدمرتضی بابامیر - استادیار گروه مهندسی کامپیوتر دانشگاه کاشان
سعید جلیلی - استادیار گروه مهندسی کامپیوتر دانشگاه تربیت مدرس

اگر نرمافزارهایی که سیستمهای حساس به ایمنی را کنترل و هدایت میکنند رفتار نامطلوب داشته باشند، میتوانند سیستم را با شکست روبرو کنند . ما در این مقاله ابتدا با استفاده از شبکههای پتری و حساب رخداد، رویکردی را برای تحلیل ایمنی رفتار نرم - افزار ارائه میدهیم و سپس با طرح مسئله پروتکل ارتباطی مطمئن در شبکه، چگونگی استفاده از رویکردمان را نشان میدهیم . رویکرد ما شامل چهار قدم است : (1) استفاده از روش رسمی شبکههای پتری برای توصیف رفتار امن نرمافزار، (2) ارائه طریقی برای استخراج مجموعه گزارههای منطقی پایا 1 از شبکههای پتری 2 و توصیف آنها با حساب رخداد 3 ، (3) توصیف نیازهای ایمنی با حساب رخداد و (4) استفاده از گزارههای منطقی پایا برای تحلیل رفتار نرمافزار در برابر نیازهای ایمنی . گزارههای منطقی پایا، که هسته تحلیلگر رفتار نرم - افزار را تشکیل میدهند، گزارههای همیشه برقراری هستند که رفتار مطلوب ( ارضا نیازهای ایمنی ) نرمافزار را نشان میدهند .

سیستمهای حساس به ایمنی، تحلیل پویا ، نیازهای ایمنی، گزارههای پایا