השגיאות היקרות ביותר הן אלו שנוצרות מוקדם אך מתגלות מאוחר. כיום קשה מאוד לגלות את השגיאות האלו מכיוון שהן מסתתרות במסמכי דרישות ואפיון הכתובים בשפה טבעית. בפרואקטיב מודלינג אנחנו מתרגמים את המסמכים האלה למודלים פורמליים הניתנים לניתוח ובדיקה מתמטית. ניתוח כזה מגלה סתירות, חלקים לא מוגדרים היטב ולא סגורים ומגוון בעיות אחרות. בנוסף, בהנתן האפיון והתכנון של המערכת ניתן לבדוק באופן מתמטי שהתכנון אכן עונה לאפיון. אנחנו משתמשים במגוון שיטות פורמליות כדי לבנות את המודלים המתמטיים ולבצע את הניתוח. השפה העיקרית שאיתה אנחנו עובדים היא שפת Z. שפת Z נמצאת בשימוש בתעשייה מזה כ-20 שנה ושימשה בהצלחה לפיתוח מערכות תוכנה רבות. כמה דוגמאות מעניינות הן מערכת ניהול הטרנזקציות CICS של IBM, הארנק האלקטרוני Mondex, ומערכת האבטחה הביומטרית Tokeneer. שילוב שיטות פורמליות בתהליך הפיתוח אין צורך לשנות את תהליך הפיתוח הקיים כדי להשתמש בשירותים שלנו. הגישה שלנו היא הדרגתית ומודולרית, ומתקדמת במקביל לתהליך הפיתוח. איננו זקוקים לתיאור מלא של כל המערכת. אנחנו מייצרים ערך תוך כדי התהליך על ידי בדיקה של כל תת מערכת עוד במהלך שלבי האפיון והתכנון שלה. הניתוח המתמטי מתבצע על ידי המומחים שלנו והמסקנות מתורגמות לשפה טבעית. |
|
|
Verifying Specifications |