سیدجواد میرعابدینی - استادیار گروه مهندسی کامپیوتر، دانشگاه آزاد اسلامی واحد تهران مرکز
آروند ربیعی - دانشجوی کارشناسی ارشد ، مهندسی نرم افزار ، دانشگاه آزاد اسلامی واحد ار
مصطفی امینی - دانشجوی کارشناسی ارشد ، مهندسی نرم افزار ، دانشگاه آزاد اسلامی واحد ار
امیر اسماعیلی - دانشجوی کارشناسی ارشد ، مهندسی نرم افزار ، دانشگاه آزاد اسلامی واحد ار

یکی از سیستم های حساس به ایمنی که مورد استفاده ی بیماران دیابتی قرار می گیرد سیستم پمپ انسولین همراه یا CIIP است . یکی از مهمترین ویژگی های سیستم های حساس به ایمنی این است که ایمنی محیط خود را تضمین نمایند، زیرا رخ دادن خطا در این سیستم ها اثرات جبران ناپذیری دربر خواهد داشت؛ بنابراین این سیستم ها باید به یک شیوه ی ایمن طراحی شوند. زیرا همواره هر نرم افزاری دارای یکسری نقص های بالقوه خواهد بود. لذا ما در این مقاله با بهره گیری از یک رویکرد ترکیبی ، با استفاده از یک روش رسمی بصری و یک روش رسمی متنی، راستی آزمای جدیدی برای سیستم CIIP طراحی می کنیم و از این طریق ویژگی ایمن بودن این سیستم را افزایش می دهیم. به همین منظور ، برای توصیف رفتار طبیعی سیستم از یک رهیافت سه لایه ای استفاده خواهیم کرد. برای توصیف بهتر راستی آزمای سیستم نیز، خواسته ای امنیتی را به سه دسته مجزا از هم تقیسم کرده و سپس آنها را توصیف می کنیم.

سیستم پمپ انسولین همراه، راستی آزما، راستی آزما پویا ، شبکه ی پتری زماندار ، زبان Z ، سیستم حساس به ایمنی