بسیاری از سیستم‏‏ های امروزی نمی توانند خود را با تغییرات در نیازمندی ها یا نقص های مؤلفه ها وفق دهند. برای نگهداری از این سیستم ها نیاز به افراد متخصص و صرف هزینه ی زیاد است. به همین دلیل در سال های اخیر تلاش شده است تا سیستم هایی ساخته شوند که بتوانند به طور پویا خود را با محیط اجراییشان وفق دهند. یک نوع از این سیستم ها، سیستم های خودتطبیق هستند. بین سیستم های خودتطبیق و سیستم های نرم افزاری رایج تفاوت های زیادی است. این تفاوت ها باعث شده اند که جامعه ی مهندسی نرم افزار به دنبال روش های جدید برای توسعه ی این سیستم ها باشد. یکی از این روش ها روش های صوری هستند. مطالعات زیادی در زمینه ی کاربرد روش های صوری در سیستم های خودتطبیق انجام گرفته است. با استخراج نکاتی که کمتر مورد توجه قرار گرفته اند، مسیر ما برای ادامه ی این تحقیق در پایان نامه مشخص می شود. کلمات کلیدی: سیستم های خودتطبیق، پردازش خودمختار، چرخه خودتطبیقی، سیستم های چندعامله، مدل سازی صوری، وارسی صوری .