Abstrakt. Vi tar itu med problemet med automatisk verifiering av tidsmässiga egenskaper hos oändliga tillstånd reaktiva system. Vi presenterar några förbättringar av en verifieringsmetod baserad på specialisering av begränsningar logik program (CLP). För det första omformulerar vi verifieringsmetoden som ett tvåfasförfarande: (1) I den första fasen är en CLP-specifikation av ett oändligt tillståndssystem specialiserad med avseende på systemets ursprungliga tillstånd och den tidsmässiga egenskap som ska verifieras, och (2) i den andra fasen utvärderas det specialiserade programmet med hjälp av en nedifrån-och-upp-strategi. I detta dokument föreslår vi några nya strategier för att genomföra programspecialisering under den första fasen. Vi utvärderar effektiviteten av dessa nya strategier, liksom av några gamla strategier, genom att presentera resultaten av experiment som utförs på flera oändliga tillståndssystem och tidsmässiga egenskaper. Slutligen jämför vi implementeringen av vår specialiseringsbaserade verifieringsmetod med olika begränsningsbaserade modellkontrollverktyg. De experimentella resultaten visar att vår metod är effektiv och konkurrenskraftig med avseende på de metoder som används i dessa andra verktyg.
Till dessa begränsande logiska program tillämpar vi en variant av den specialiseringsteknik som presenteras i REF.
Program specialization for verifying infinite state systems: An experimental evaluation
{'venue': 'In LOPSTR’10', 'journal': None, 'mag_field_of_study': ['Computer Science']}