انجمن کامپیوتر ایران

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