År 1995 bröt HyTech ny mark som ett potentiellt kraftfullt verktyg för att verifiera hybridsystem. Men på grund av praktiska och systematiska begränsningar är det endast tillämpligt på relativt enkla system. Vi tar itu med de största problemen med HyTech med PHAVer, ett nytt verktyg för exakt verifiering av säkerhetsegenskaper hos hybridsystem med bitvis konstanta gränser på derivaten, så kallad linjär hybridautomata. Affin dynamik hanteras av on-the-fly över approximation och partitionering av tillståndet utrymme baserat på användartillhandahållna begränsningar och dynamiken i systemet. PHAVer har exakt aritmetik i ett robust genomförande som, baserat på Parma Polyhedra Library, stöder godtyckligt stora tal. För att tvinga fram terminering och hantera komplexiteten i polyhedralberäkningarna föreslår vi metoder för att konservativt begränsa antalet bitar och begränsningar av polyhedra. Experimentella resultat för ett navigeringsriktmärke och en tunneldiodkrets visar hur effektivt tillvägagångssättet är.
PHAVer REF kan hantera en klass av system som kallas linjär hybrid automata som har affin dynamik.
PHAVer: algorithmic verification of hybrid systems past HyTech
{'venue': 'International Journal on Software Tools for Technology Transfer', 'journal': 'International Journal on Software Tools for Technology Transfer', 'mag_field_of_study': ['Computer Science']}