22926 מודלים ושיטות אפיון של מערכות מקביליות ותגובתיות
22926 מודלים ושיטות אפיון של מערכות מקביליות ותגובתיות
4 נקודות זכות
שיוך: תואר שני / מדעי המחשב
שיוך נוסף: מדעים / מדעי המחשב
שיוך נוסף: הנדסה / הנדסת תוכנה
תנאי קבלה: קבלה לתואר שני במדעי המחשב.1
פיתוח הקורס: פרופ' דוד הראל (אחראי אקדמי), ד"ר מרק טרכטנברוט
יועצים: פרופ' ארנה גרימברג, פרופ' עמירם יהודאי, פרופ' אורנה קופרמן
הקורס מציג מגוון גישות (אלגבריות וחזותיות) לאפיון ואנליזה של מערכות מקביליות מתקשרות (Concurrent Communicating Systems), תוך השוואה של הגישות האלה והצגה של עקרונותיהן במסגרת אחידה. הסטודנטים בקורס יוכלו להכיר מוטיבציה, מושגים ושיטות סימון המאפשרים למתכנני מערכות כאלה חשיבה ותיאור מדויקים, וגם הוכחת נכונותן. הקורס (שהוא תאורטי בעיקרו) מספק גם פתח ליישומים – דרך סדרת דוגמאות מתאימות, ותוך שימוש בכלי תוכנה המיישמים את הגישות הנלמדות ומאפשרים התנסות מעשית באפיון פורמלי ואנליזה של תהליכים.
נושאי הלימוד
חלק 1: תהליכים (processes), שקילויות (equivalances), אופרטורים
-
תהליכים ומערכות מעבר מתוויות (Labeled Transitions Systems – LTS)
-
שקילויות עבור LTS
-
אופרטורים ותכונותיהם (אופרטורים סדרתיים, גרסאות שונות של הרכבה מקבילית)
חלק 2: תחשיבי תהליכים
-
ביטויי תהליכים סדרתיים
-
תחשיב CCS (Calculus Communicating Systems) בסיסי
-
שפת אפיון תהליכים LOTOS והשוואתו עם CCS
-
מנגנוני העברת ערכי נתונים (value passing)
חלק 3: פורמליזמים חזותיים
-
Statecharts
-
רשתות Petri
-
Live Sequence Charts
חומר הלימוד כולל קובץ מאמרים ומדריך למידה.
1 סטודנט שאינו עומד בתנאי הקבלה יכול, במקרים מסוימים, להירשם לקורס. לפרטים נוספים עיינו בסעיף קבלה לקורסים בודדים בתכנית הלימודים לתואר שני במדעי המחשב.