Abstrakt. Statens rymdexplosion är ett grundläggande hinder för formell kontroll av konstruktioner och protokoll. Flera tekniker för att bekämpa detta problem har dykt upp under de senaste åren, bland vilka två är betydande: partiella ordningsnedskärningar och symbolisk rymdsökning. I asynkrona system är interleavings av oberoende samtidiga händelser likvärdiga, och endast en representativ interleaving behöver utforskas för att verifiera lokala egenskaper. Partiell ordning metoder utnyttja denna redundans och besöka endast en delmängd av de nåbara tillstånden. Symboliska tekniker, å andra sidan, fånga övergångsförhållandet mellan ett system och uppsättningen av nåbara stater som booleska funktioner. I många fall kan dessa funktioner representeras kompakt med hjälp av binära beslutsscheman (BDD). Traditionellt har de två teknikerna praktiserats av två olika skolor-partial-order metoder med räknande djup-första sökning för analys av asynkrona nätverksprotokoll, och symbolisk bredd-första sökning för analys av synkron hårdvara design. Vi kombinerar båda tillvägagångssätten och utvecklar en metod för att använda partiell-order reduktion tekniker i symbolisk BDD-baserad invariant kontroll. Vi presenterar teoretiska resultat för att bevisa metodens riktighet och experimentella resultat för att visa dess effektivitet.
Arbetet i REF tillämpar POR på symbolisk BDD-baserad invariant kontroll.
Partial-Order Reduction in Symbolic State-Space Exploration
{'venue': 'Formal Methods in System Design', 'journal': None, 'mag_field_of_study': ['Computer Science']}