דילוג לתוכן ראשי

קורסים

  • מבוא להנדסת תוכנה (10014)
    • תקציר הקורס:

    תקציר:

    המחשב הדיגיטלי הראשון נבנה עבור צבא ארה"ב בשנת 1946. שפות תכנות מחשבים עיליות החלו להיווצר בסוף שנות החמישים של המאה הקודמת.

    המחשבים דיגיטליים היו בני פחות מרבע מאה וכבר עמדנו בפני תופעה שכונתה "משבר תוכנה". המשבר נוצר לא רק בגלל שהתוכנה המיוצרת לא תפקדה כראוי,

    אלא בגלל הבעיות הקשורות לאופן שבו התוכנה פותחה והביקוש הגובר לתוכנות גדולות ומורכבות. משבר התוכנה מאופיין בבעיות רבות:

    היעדר דרישות מוגדרות היטב ושינויים תכופים לדרישות; אומדני לוחות הזמנים ועלויות הפיתוח לרוב אינם מדויקים; התפוקה של מפתחי תוכנה לא עומדת בקצב הביקוש לשירותים שלהם;

    איכות התוכנה לפעמים אינה מספקת. הנדסת תוכנה פותחה בפתרון לבעיות המאפיינות את משבר התוכנה, והיא מקיפה את מחזור החיים השלם של תוכנה.
  • מידול מערכות תכנה (10148)
    • תקציר הקורס:

    תקציר:

    הקורס מחולק לשני חלקים. בחלק הראשון נלמד איך לתאר מערכות תגובתיות כמכונות מצבים (transition systems) ואיך לתאר תכונות בטיחות וחיות בעזרת נוסחאות בלוגיקה טמפורלית. נשתמש בכלי NuSMV כדי לבדוק באופן אוטומטי האם התכונות הרצויות מתקיימות. בחלק השני נלמד איך לתאר מערכות עתירות מידע בעזרת לוגיקה רלציונית ואיך לנסח תכונות מבניות (structural invariants) והתנהגותיות בעזרת הלוגיקה הרלציונית והכלי Alloy analyzer.
  • סמינר בהנדסת תוכנה (10400)
    • תקציר הקורס:

    תקציר:

    המונח שיטות פורמליות מתייחס לשפות ולשיטות המאפשרות מידול מדויק של מערכות ברמות שונות של הפשטה, לגבש עבורן דרישות, ולנתח באופן מהימן את מילוין של דרישות אלו.

    שיטות פורמליות משמשות בהנדסת תוכנה כדי לאפשר אפיונים מדויקים וחד משמעיים, תכנון קפדני ואימות פורמלי של מערכות, מה שמפחית את הסבירות לטעויות שעלולות להוביל לכשלים ביישומים קריטיים.

    סמינר זה מציג בפני הסטודנטים שיטות פורמליות, תוך שימת דגש על חשיבותן של שיטות אלו בהבטחת תקינות תוכנה, אמינות ואבטחה.

    בסמינר נעסוק בנושאים שונים בשיטות פורמליות לאורך מחזור החיים של פיתוח התוכנה.