I am aware of some work that involves modelling external devices to achieve verification with SAL or HOL: http://staffwww.dcs.shef.ac.uk/people/R.Taylor/Spurinna/