Abstrakt. Vi ger en inkrementell, induktiv (IC3) procedur för att kontrollera täckningen av välstrukturerade övergångssystem. Vårt förfarande generaliserar IC3-proceduren för säkerhetsverifiering som framgångsrikt har tillämpats i finit-state hårdvaruverifiering på oändliga välstrukturerade övergångssystem. Vi visar att vår procedur är sund, komplett, och avslutar för nedåt-finita välstrukturerade övergångssystem - där varje stat har ett begränsat antal tillstånd under it-en klass som innehåller förlängningar av Petri nät, sändningsprotokoll, och förlust kanal system. Vi har implementerat vår algoritm för att kontrollera täckningen av Petri nät. Vi beskriver hur algoritmen effektivt kan implementeras utan användning av SMT-lösare. Våra experiment på standard Petri nettoriktmärken visar att IC3 är konkurrenskraftig med toppmoderna implementationer för täckning baserat på symbolisk bakåtanalys eller expandera-stor-och-kontroll algoritmer både i tid och rymdanvändning.
Inspirerad av framgången med IC3-algoritm i finit tillstånd modellkontroll, Kloos et al. I REF föreslogs ett stegvist, induktivt förfarande för att kontrollera täckningen av WSTS nedifrån och ned, som innehåller Petri-nät, sändningsprotokoll och förlustkanalsystem.
Incremental, Inductive Coverability
{'venue': 'ArXiv', 'journal': 'ArXiv', 'mag_field_of_study': ['Computer Science', 'Mathematics']}