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

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

منطق محاسباتی احتمالی محدودیت ، وارسی مدل ، درستی یابی ، ماشین محدودیت احتمالی ، سیستم های احتمالی ، ریو