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

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

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

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

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

בדומה למקצועות הנדסיים אחרים כלי עיקרי בהנדסת תכנה הוא היכולת לבנות מודלים.

מודלים עוזרים בניתוח והבנת המערכת ומשמשים לתיעוד חד משמעי של מטרת המערכת והתכנון שלה.

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

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

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

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

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

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