Ljudnivån hos enhetsdrivrutinerna kan i allmänhet inte kontrolleras isolerat, utan måste ta hänsyn till hårdvaruenheternas reaktioner. I kritiska inbäddade system var gränssnitten ofta enkla "flyktiga" variabler, och gränssnittsspecifikationen var vanligtvis en lista över gränser för dessa variabler. Vissa nyare system använder "intelligenta" regulatorer som hanterar dynamiska arbetslistor i delat minne och utför direkta minnesåtkomster, alla asynkront från huvudprocessorn. Således är det omöjligt att verkligen verifiera enhetsdrivrutinen utan att ta hänsyn till den intelligenta enheten, eftersom felaktig programmering av enheten kan leda till ödesdigra konsekvenser, såsom minneszoner raderas. Vi har framgångsrikt verifierat en enhetsdrivrutin som extraherats från ett kritiskt industrisystem, asynkront kombinerat med en modell för en USB OHCI-styrenhet. Detta dokument studerar detta fall, samt introducerar en modell och analystekniker för denna asynkrona sammansättning.
Monniaux et al REF har verifierat en drivrutin med en USB OHCI styrenhet modell skriven i C med en statisk analysator.
Verification of device drivers and intelligent controllers: a case study
{'venue': "EMSOFT '07", 'journal': None, 'mag_field_of_study': ['Computer Science']}