Distribuerade it-fysiska system (DCPS), såsom flygteknik och marktransportsystem, är mycket svåra att utforma och verifiera, på grund av asynkron kommunikation, nätverksförseningar och urskalv. Deras modellkontrollverifiering blir vanligtvis ogenomförbar på grund av den enorma tillståndsexplosion som orsakas av systemets samstämmighet. Metoden Multirate PALS ("fysiskt asynkron, logiskt synkron") har föreslagits för att minska konstruktionen och kontrollen av en DCPS till den mycket enklare uppgiften att utforma och verifiera dess underliggande synkrona version, där komponenter kan fungera med olika perioder. I detta dokument presenteras en metod för att formellt modellera och kontrollera multirate DCPS med hjälp av multirate PALS. I synnerhet förklarar denna metod hur man hanterar systemets fysiska miljö i Multirate PALS. Vi illustrerar vår metodik med en multirate DCPS som består av ett flygplan som manövreras av en pilot, som vänder flygplanet till en angiven vinkel genom ett distribuerat styrsystem. Vår formella analys med hjälp av Real-Time Maude avslöjade att den ursprungliga designen inte uppnådde en jämn svängmanöver, och ledde till en omdesign av systemet. Vi använder sedan modellkontroll och multirate PALS för att bevisa att det omdesignade systemet uppfyller de önskade korrekthetsegenskaperna, medan modellkontroll av motsvarande asynkron modell är ogenomförbar. Detta visar att multirate PALS inte bara är effektivt för formell DCPS-verifiering, utan också kan användas effektivt i DCPS-designprocessen.
Bae m.fl. Ref kombinerade modellkontroll och multirate PALS (fysiskt asynkron, logiskt synkron) metod för första gången för att verifiera ett flygplan svängning styrsystem.
Designing and verifying distributed cyber-physical systems using Multirate PALS: An airplane turning control system case study
{'venue': 'Sci. Comput. Program.', 'journal': 'Sci. Comput. Program.', 'mag_field_of_study': ['Computer Science']}