Behavioural analysis of an I2C Linux driver

D. Bosnacki, A.H.J. Mathijssen, Y.S. Usenko

Onderzoeksoutput: Boek/rapportRapportAcademic

1 Citaat (Scopus)
367 Downloads (Pure)

Samenvatting

We present an analysis of the behaviour of an I2C Linuxdriver, by means of model checking with the mCRL2 toolset and static analysis with UNO.We have reverse engineered the source code to obtain the structure and interactions of the driver. Based on these results, we have semi-automatically created an mCRL2 model of the behaviour of the driver, on which we have checked mutual exclusion properties. This revealed non-trivial potential errors, like unprotected usage of shared memory variables due to inconsistent locking and disabling/enabling of interrupts. We also applied UNO on the instrumented source code and were able to find the same errors. These defects were confirmed by the developers.
Originele taal-2Engels
Plaats van productieEindhoven
UitgeverijTechnische Universiteit Eindhoven
Aantal pagina's16
StatusGepubliceerd - 2009

Publicatie series

NaamComputer science reports
Volume0909
ISSN van geprinte versie0926-4515

Vingerafdruk Duik in de onderzoeksthema's van 'Behavioural analysis of an I2C Linux driver'. Samen vormen ze een unieke vingerafdruk.

Citeer dit