Att kontrollera att programvaran är korrekt är en växande utmaning. I detta dokument presenterar vi en prototyp implementation av Partial Order Trace Analyzer (POTA), ett verktyg för att kontrollera körning spår av både meddelande passerar och delade minnesprogram med hjälp av temporal logik. Hittills har verktyg för runtime-verifiering använt den totala ordermodellen för ett utförande spår, medan POTA använder en partiell order modell. Den partiella ordermodellen gör det möjligt för oss att fånga upp eventuellt exponentiellt antal interleaveings och, i sin tur, gör det möjligt för oss att hitta fel som inte hittas med hjälp av en total ordermodell. Verifiering i partiell ordningsmodell lider dock av problemet med statsexplosion – antalet möjliga globala stater i ett program ökar exponentiellt med antalet processer. POTA använder en effektiv abstraktionsteknik som kallas beräkningsskärning. En bit av en beräkning (utförande spår) med avseende på en predikat är beräkningen med det minsta antalet globala stater som innehåller alla globala tillstånd av den ursprungliga beräkning som predikatet utvärderar till sant. Fördelen med denna teknik är att den lindrar problemet med statsexplosion genom att endast resonera på den del av den globala statsrymden som är av intresse. I POTA implementerar vi beräkningsalgoritmer för tidslogik som bygger på en delmängd av CTL. Den övergripande komplexiteten av att utvärdera en predikat i denna logik vid användning av beräkning slicing blir polynomial i antalet processer jämfört med exponentiell utan slicing. Vi illustrerar effektiviteten hos våra tekniker i POTA i testfall som det allmänna inter-ORB-protokollet (GIOP) [18]. POTA innehåller också en modul som översätter körspår till Promela [16] (inmatningsspråk SPIN). Denna modul gör det möjligt för oss att jämföra våra resultat på utförande spår med SPIN. I vissa fall kunde vi verifiera spår med 250 processer jämfört med endast 10 processer med SPIN.
JMPaX-verktyget ligger närmare vårt verktyg POTA REF på grund av den partiella orderspårningsmodellen.
Partial Order Trace Analyzer (POTA) for Distributed Programs
{'venue': 'In Proceedings of the Third Workshop on Runtime Verification (RV', 'journal': None, 'mag_field_of_study': ['Computer Science']}