skip // else ignore message
برای مطالعه بیشتر به ]۲۹[ الی ]۳۲[ مراجعه کنید.

LOTOS
LOTOS^[40] توسط سازمان ISO برای بیان فرمال استاندارد های مربوط به OSI ساخته شد. این زبان به عنوان به عنوان یک FDT^[41] تحت استاندارد ISO/IEC 8807 در سال ۱۹۸۹ ارائه گردید^[۴۲].
LOTOS یک زبان توصیف فرمال مبتنی بر روابط جبری است که برای توصیف سیستم های موازی و توزیع شده مناسب می باشد ]۱۵[. در واقع دو بخش اصلی تشکیل دهنده LOTOS عبارتست از ADT^[43] و جبر پروسه ها. به دلیل پشتیبانی از گونه های داده ای انتزاعی، این زبان می تواند تبادل اطلاعات و در نتیجه رابطه بین اجرا را به خوبی توصیف نماید. همچنین به دلیل جبری بودن، خواص عملکردی سیستم را توصیف می نماید. به علاوه، پشتیبانی از عملگرهای temporal باعث می شود که این زبان توانایی توصیف خواص رفتاری و جنبه های زمانی سیستم ها را نیز داشته باشد.

مقدمه ای بر جبر پروسه ها^[۴۴] ]۱۶[
در این جبر، اجزای سیستم به صورت پروسه های انتزاعی نمایش داده می شوند که با یکدیگر ارتباط دارند. پروسه ها به صورت جعبه سیاه دیده می شوند که تنها رفتار خارجی آنها مورد بررسی قرار می گیرد. همچنین پروسه ها به کمک مکانیزم interaction point با یکدیگر رابطه برقرار می کنند. در LOTOS به این نقاط event gate یا به اختصار gate گفته می شود (شکل ۲٫۳).
شکل ۲٫۳٫ نقطه gate در جبر پروسه ها ]۴[
Event نشان دهنده یک همگامی^[۴۵] بین دو یا چند پروسه است. به طور کلی سه نوع event تعریف شده اند:
Pure synchronization: هیچ مقداری بین پروسه ها تبادل نمی شود.
Value establishment: مقادیر ارائه شده توسط یک یا چند پروسه از سوی بقیه مورد پذیرش نیست.
Value negotiation: مقادیر از سوی یک یا چند پروسه مورد قبول است.
همچنین یک عبارت رفتاری^[۴۶] انتخابی از بین مجموعه ای از event ها است که برای یک محیط مطرح می گردد. در شرایطی که امکان همگام سازی بین eventهای پیشنهاد شده در یک محیط وجود نداشته باشد یک بن بست^[۴۷] رخ داده است. همچنین اگر هیچ پیشنهادی در محیط مطرح نشده باشد یک livelock رخ می دهد (مانند یک حلقه بینهایت).
همچنین LOTOS مفهوم ترتیب زمانی eventها را نیز به قواعد جبری موجود اضافه نموده است. این زبان از عملگرهای temporal برای ترکیب عبارات رفتاری و به دست آوردن عبارات رفتاری پیچیده تر استفاده می کند. در عین حال این عملگرها از قواعد خوش تعریف پیروی می نمایند که تفسیر صریح و یکسانی را برای افراد ممکن می سازد.
به عنوان خلاصه ای از خصوصیات LOTOS، می توان آنرا تعریف فرمالی از ترکیب داده و کنترل، بر مبنای جبر پروسه ها دانست که همزمانی^[۴۸] یکی خصوصیات ذاتی آن است. همچنین قواعد LOTOS به دلیل عملیاتی بودن قابل تفسیر و اجرا^[۴۹] می باشد و ماژولار است ]۱۷[.
در ادامه مثالی از مدلسازی مساله تولید کننده- مصرف کننده^[۵۰] با این زبان آورده شده است. در این مساله سه ماژول تولید کننده، مصرف کننده و کانال که وظیفه هماهنگ سازی این دو را به عهده دارد حضور دارند. لازم به ذکر است که تغییراتی در صورت مساله به وجود آمده تا خصوصیات LOTOS بهتر نشان داده شود. ازآن جمله، تولید کننده می تواند دو خروجی را به صورت همزمان یا غیر همزمان تولید نماید و سپس متوقف شود. همچنین مصرف کننده پس از مصرف ترتیبی یا همزمان آنها متوقف می گردد (شکل ۲٫۴).
شکل ۲٫۴٫ مدل تولید کننده- مصرف کننده به کمک LOTOS ]17[
برای کنترل پیچیدگی مساله، در ابتدا عمل تجزیه^[۵۱] را روی این سه بخش انجام داده و هر یک را به عنوان یک پروسه مستقل تشریح می کنیم. سپس آنرا را با هم ترکیب می نمائیم.
با توجه به تعاریف pc1 و pc2 به عنوان کانال های تولید کننده و cc1 و cc2 به عنوان کانال های مصرف کننده و همچنین عملگرهای انتخاب ([]) و فعال سازی^[۵۲] (>>) می توان پروسه های فوق را به صورت زیر تعریف نمود:
پروسه تولید کننده:
process Producer [pc1, pc2] : exit :=
pc1; pc2; exit
endproc
پروسه کانال:
process Channel [ pc1, pc2, cc1, cc2] : exit :=
pc1;
(
pc2; cc1; exit
[]
cc1; pc2; exit
)
>> cc2; exit
endproc
پروسه مصرف کننده:
process Consumer [cc1, cc2] : exit :=
cc1; cc2; exit
endproc
در این بین می توان جزئیات اجرایی بیشتر مانند عملکرد داخلی هریک از پروسه ها را با عملگرهای بیشتری مدل نمود به عنوان مثال مساله گم شدن یکی از ورودی ها به کانال به شکل زیر قابل توصیف است:
process Channel [pc1, pc2, cc1, cc2] : exit :=
pc1; ( pc2 ; cc1; exit [] cc1; pc2; exit [] i; pc2; exit )
>> ( cc2; exit [] i; exit)
Endproc