حسن حقیقی - استادیار دانشکده مهندسی برق و کامپیوتر دانشگاه شهید بهشتی
سلیمه جوادیان - دانشجوی دانشکده مهندسی برق و کامپیوتر دانشگاه شهید بهشتی
محمدمهدی جوانمرد - دانشجوی دانشکده مهندسی برق و کامپیوتر دانشگاه شهید بهشتی

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

توصیف صوری، تولید صوری برنامه ها، تئوری انواع ساختی، عدم قطعیت، برنامه های هم روند