MODEX - 10 V 2005, Mateusz Srebrny

Tworzenie modelu [ang. model extraction]

• Konstrukcja modelu dla oprogramowania
• Jak najwieksza automatyzacja

Tradycyjne podejscie do tworzenia modelu

• Model niezwiazany z implementacja
• Model tworzony przez osobny zespol
• Model oparty na dokumentacji i protokolach
• Nie moze wykrywac bledow programistycznych
• Bardzo dlugi proces
• W czasie tworzenia modelu oprogramowanie ewoluuje

Tworzenie modelu z kodu zrodlowego

• Slam (Microsoft), programy w C, BeBop
• Bandera (Kansas State University), programy w Javie, promela
• JavaPathfinder (NASA), programy w Javie, poczatkowo promela, teraz wbudowany model-ckecker

Modex

• Gerrard J. Holzmann i Margaret H. Smith (Bell Laboratories)
• programy w C, promela
• zaprojektowany do weryfikacji glownie kodu wielowatkowego
• FeaVer opakowuje

Mozliwosci

• asercje z C (assert(expr), assert_r(expr), assert_p(expr0, expr1))
• bledy indeksowania statycznie alokowanych tablic
• bledy NULLowych wskaznikow
• bledy zapetlen ([ang. livelocks])
• bledy zakleszczen ([ang. deadlocks])
• spawdzanie wlasnosci LTLowych (tez ω-regular)

Tworzony model

• Definiujemy procesy (kod zrodlowego i/lub kod w promeli ([ang. test driver])
• Definiujemy jak procesy sie komunikuja (zastepujac komunikacje ze zrodla wstawkami promelowymi)
• Wybieramy ktore obiekty skladaja sie na stan w modelu

Kontekst weryfikacji [ang. verification test harness]

• Tworzenia modelu sterowane plikiem .prx
• "If built correctly it will be largely immune to changes in the source code of application" [Holzmann2001]

Przyklady

• dystybucja: http://cm.bell-labs.com/cm/cs/what/modex/modex.tar.gz
• threads: threads.c, threads.prx, import
• pointers: pointers.c, pointers.prx, import
• bounds: bounds.c, bounds.prx, import
• bad_mutex: bad_mutex.c, bad_mutex.prx, import
• abp: abp.c, abp.prx, import
• abp2: abp2.c, abp2.prx, import

Bibliografia