Abstract-Modern datorsystem bildas ofta av flera komponenter som interagerar med varandra genom användning av delade resurser (t.ex. CPU, nätverksbandbredd, lagring). I detta dokument betraktar vi ett representativt scenario för ett sådant system i samband med tillämpningen av Internet of Things. Systemet består av ett nätverk av självanpassade kameror som delar en kommunikationskanal, sänder strömmar av ramar till en central nod. Kamerorna kan ändra en kvalitetsparameter för att anpassa mängden kodad information och för att påverka deras bandbreddskrav och användning. Ett kritiskt designval för ett sådant system är schemaläggning av kanalåtkomst, dvs. hur man bestämmer den mängd kanalkapacitet som ska användas av var och en av kamerorna när som helst. Två huvudfrågor måste beaktas vid valet av ett system för tilldelning av bandbredd: i) kameraanpassning och schemaläggning av nätverksåtkomst kan störa varandra, ii) bandbreddsdistribution bör utlösas endast när det är nödvändigt, för att begränsa ytterligare omkostnader. I detta dokument föreslås det första formellt verifierade händelseaktiverade anpassningssystemet för bandbreddstilldelning, som är utformat för att minimera extra omkostnader i nätet. Önskade egenskaper hos systemet verifieras med hjälp av modellkontroll. I dokumentet beskrivs också experimentella resultat som uppnåtts med hjälp av ett genomförande av programmet.
Vårt tidigare dokument REF kombinerar anpassningsstrategin för kamerorna och bandbreddstilldelningen, vilket verifierar egenskaperna hos det övergripande systemet utan störningar.
Event-Driven Bandwidth Allocation with Formal Guarantees for Camera Networks
{'venue': '2017 IEEE Real-Time Systems Symposium (RTSS)', 'journal': '2017 IEEE Real-Time Systems Symposium (RTSS)', 'mag_field_of_study': ['Computer Science']}