אימות תוכנה – הבדלי גרסאות

תוכן שנמחק תוכן שנוסף
Vinney (שיחה | תרומות)
הרחבה
Vinney (שיחה | תרומות)
אין תקציר עריכה
שורה 12:
הראשונה היא שיטת [[בדיקת מודל|בדיקות מודל]] - תהליך האימות מתבצע על מודל מתמטי המתאר את מערכת התוכנה, תוך הוכחת נכונות של תכונות הנדרשות על בסיס המודל הזה, תוך ניתוח המצבים והמעברים בינהם. על מנת להצליח בשיטה הזאת, המודל חייב להיות ''סופי'' (בעל מספר סופי של מצבים). השיטה הזאת מאוד מוגבלת מהבחינה המעשית, זאת בגלל [[בעיית התפוצצות מצבים]] שמאפיינת מערכות מעשיות רבות.
 
השיטה השניה היא שיטת ההיסק הלוגיההוכחה - בשיטה הזאת מתארים תכונות מסוימות של התכונה ב[[תחשיב פסוקים]] לוגי (בעזרת [[לוגיקה טמפולרית]], כדוגמאת [[CTL*|*CTL]]), ומראיםומוכיחים שהתוכנה (יותר נכון המודל שלה) מספקת את התכונות הנדרשות, בעזרת כלים מתמטיים אוטומטיים או אוטומטיים למחצה (Theorem Provers). גם השיטה הזאת מוגבלת בגלל [[בעיית התפוצצות מצבים]], זאת למרות שניתן לבטא בעזרת תחשיב לוגי גם תכונות עבור מודלים אינסופיים.
 
למרות שהמחקר בתחום הזה מתבצע תחת כובע [[מדעי המחשב]], השיטות האלה משמשות גם לאימות [[חומרה]], שם [[בעיית התפוצצות מצבים|בעיית התפוצצות המצבים]] חריפה פחות.