شماره ركورد
10575
شماره راهنما(اين فيلد مربوط به كارشناس ميباشد لطفا آن را خالي بگذاريد)
10575
پديد آورنده
الهه قصاباني
عنوان
درستييابي امنيتي برنامههاي همروند از طريق بررسي مدل بدون حالت كد
مقطع تحصيلي
كارشناسي ارشد
رشته تحصيلي
كامپيوتر- گرايش نرمافزار (سيستمهاي توزيعي)
سال تحصيل
مهر ماه 1391
تاريخ دفاع
مهر ماه 1391
استاد راهنما
دكتر محمد عبداللهي ازگمي
چكيده
بررسي مدل بدون حالت يك فن مؤثر براي درستييابي برنامههاي بزرگ و پيچيده است كه از لحاظ كاربردپذيري نسبت به بررسي مدل حالت كامل، براي دنياي نرمافزار مناسبتر است. بررسي مدل بدون حالت كد يك گرايش جديد در بررسي مدل است كه به جاي تفسير و اجراي مدل توصيف شده از روي برنامه، كد برنامه را در محيط اجراي واقعي زبان برنامهنويسي درستييابي ميكند.
در اين پاياننامه يك ابزار توزيعشده و موازي براي درستييابي كدهاي زبانهاي برنامهنويسي با استفاده از فن بررسي مدل بدون حالت طراحي و پيادهسازي شده است. توجه ما به طور خاص معطوف به درستييابي خصوصيات امنيتي برنامههاي همروند (چندنخي) بوده است. از اين رو ابزار طراحي شده به صورت خودكار قادر به شناسايي بنبست، قفل زنده، شرايط مسابقه، نقض ادعا و درستييابي امنيت جريان اطلاعات است. از طرف ديگر اين ابزار قادر به درستييابي فرمولهاي منطق زماني خطي (LTL) نيز هست.
نوآوريهاي اين پاياننامه در دو حوزه است. نخست، الگوريتمهايي طراحي شدهاند كه توسط آنها براي اولين بار قادر شدهايم كه فرمولهاي LTL را در بررسي مدل بدون حالت درستييابي كنيم. دوم، ما براي اولين بار با استفاده از بررسي مدل بدون حالت كد، درستييابي خصوصيت امنيت جريان اطلاعات را انجام دادهايم. با روشي كه ارائه شده است، ما براي اولين بار، قادر به درستييابي عملي جديدترين تعريف ارائه شده از عدم مداخله در برنامههاي همروند هستيم. يك نمونه اوليه از يك ابزار را با زبان اِرلنگ براي درستييابي برنامههاي نوشته شده به زبان C و كتابخانه چندنخي POSIX پيادهسازي نمودهايم. ابزار با استفاده از مثالهايي آزمون شده و الگوريتمها و مؤلفههاي آن نيز ارزيابي و از طريق فن بررسي مدل بهطور صوري درستييابي شدهاند.
واژههاي كليدي: بررسي مدل كد، بررسي مدل بدون حالت، درستييابي برنامههاي همروند، درستييابي خصوصيات امنيتي.