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