I detta dokument presenterar vi den formella modellering och automatisk parameteriserad verifiering av en distribuerad flygtrafikledning protokoll kallas Small Aircraft Transport System (SATS). Varje flygplan är modellerat som en tidsinställd automaton med (eventuellt obundna) räknare. SATS beskrivs sedan som sammansättningen av sådana N-flygplan, där N är en parameter från de naturliga talen. Vi verifierar flera säkerhetsegenskaper för godtyckliga N, varav det viktigaste är separation försäkran, vilket säkerställer att inga två flygplan någonsin kan kollidera. Verifieringsmetoden bygger på att man beräknar mängden bakåtåtkomliga tillstånd från uppsättningen osäkra stater till en fast punkt och kontrollerar tomheten i skärningspunkten mellan dessa nåbara stater och den ursprungliga uppsättningen stater. Vi använde verktyget Model Checker Modulo Theories (MCMT), som implementerar denna teknik. 2012 IEEE/ACM Tredje internationella konferensen om cyberfysiska system 978-0-7695-4695-7/12 26,00
Johnson och Mitra REF använder parameteriserad verifiering för att garantera att ett protokoll för distribuerad flygtrafiklandning (SATS) är fritt från kollisioner.
Parametrized Verification of Distributed Cyber-Physical Systems: An Aircraft Landing Protocol Case Study
{'venue': '2012 IEEE/ACM Third International Conference on Cyber-Physical Systems', 'journal': '2012 IEEE/ACM Third International Conference on Cyber-Physical Systems', 'mag_field_of_study': ['Computer Science']}