Abstrakt. Vi presenterar en översikt över Java PathExplorer körtidsverifieringsverktyget, kort sagt kallat JPAX. JPaX kan övervaka genomförandet av ett Java-program och kontrollera att det överensstämmer med en uppsättning användartillhandahållna egenskaper formulerade i temporal logik. JPaX kan dessutom analysera programmet för konvergensfel såsom dödläge och dataraser. Konvergensanalysen kräver ingen specifikation av användaren. Verktyget underlättar automatisk instrumentering av ett programs bytekod, som när den utförs avger en händelseström, körspåret, till en observatör. Observatören skickar den inkommande händelseströmmen till en uppsättning observatörsprocesser, där var och en utför en specialiserad analys, såsom tidslogikverifiering, dödlägesanalys och datakapplöpningsanalys. Temporal logik specifikationer kan formuleras av användaren i Maude omskrivning logik, där Maude är en hög hastighet omskrivning system för ekvationslogik, men här utökad med körbar temporal logik. Maude omskrivarmotorn aktiveras sedan som en händelsedriven övervakningsprocess. Alternativt kan tidsspecifikationer översättas till automatiserade eller algoritmer som effektivt kan kontrollera händelseströmmen. JPaX kan användas under programtestning för att få ökad information om programutföranden, och kan eventuellt också tillämpas under drift på säkerhetskritiska system.
PathExplorer (PAX) är ett körtidsverifieringsverktyg av Havelund och Roşu REF som använder linjär tidslogik (LTL).
An Overview of the Runtime Verification Tool Java PathExplorer
{'venue': 'Formal Methods in System Design', 'journal': None, 'mag_field_of_study': ['Computer Science']}