ارائه رویکردی صوری جهت مدل سازی ئ درستی یابی ویژگی خود سازی در سامانه های نهفته

در راستای افزایش پیچیدگی در سامانه های کامپیوتری ، امروزه سامانه های نهفته بزرگی پا به عرصه وجود گذاشته اند که از اتصال تعداد زیادی از سامانه هایکوچک نهفته تشکیل شده اند با هوشمند کردن ماشین ها ، می توان پیچیدگی روز افزون در سامانه های کامپیوتری را کاهش داد و به این سامانه ها ، ویژگی هایی همچون خود تنظیمی ، خود ترمیمی و همانند آن را ، به شکل کلی خود -* نامیده می شوند ، افزود. خود سازی یکی از ویژگی ها است که سامانه را قادر می سازد ساختار خود را از روی یک طرح با استفاده از واحد هایی بسازد و در هنگام اجرا به شکل پویا از درستی ساختار خود آگاه گردد. به این ترتیب ، یک موضوع مهم در ویژگی خود سازی در سامانه های نهفته ، اطمینان از درستی و سازگاری طرح اصلی است و اگر مشکلی در این طرح وجود داشته باشد ، می تواند به نتایج فاجعه باری منجر شود . این موضوع به ویژه در سامانه های نهفته بزرگ اهمیت بسزایی دارد ، زیرا هم دارای تعداد واحدهای سازنده زیادی هستند و هم اشکال زدایی به سهولت در آن ها امکان پذیر نیست. در این مقاله رویکردی جهت تامین درستی و سازگاری ویژگی خودسازی در سامانه های نهفته از طریق استفاده از روش های صوری ارائه می شود. به این منظور، ازمفهوم DNA مصنوعی که در برخی از سامانه های موجود نهفته برای خود سازی بکار رفته است، استفاده می شود.با هدف افزایش دقت و کاهش ابهام ها و ناسازگاری ها از یک سو و ایجاد زمینه خود کار سازی ازسوی دیگر، ابتدا یک مدل صوری بر مبنای این مفهوم ارائه شده و سپس درستی و سازگاری این مدل ازطریق درست یابی صوری بررسی می شود.برای نشان دادن کاربرد پذیری مدل صوری پیشنهاد شده، این مدل باکمک ابزار صوری Maude پیاده سازی و روی یک سامانه نمونه نهفته اعمال می گردد.

کلیدواژه ها:

خودسازی ، سامانه های نهفته ، توصیف صوری ، DNA مصنوعی