The other night (coincidentally right before an initial interview with Microsoft) I ran across the Static Driver Verification project in the Windows Group at Microsoft. SDV is a tool that integrates a home grown model checker (SLAM) for drivers with a whole suite of specifications for Windows HW drivers. This is an amazing example of the potential benefits of formal verification in software when an appropriate focus is put on utility as well as theoretical interest.
The Microsoft Research group that produced SDV also wrote a tech report on their success in a technology transfer from a research project to an actual software tool usable by real developers both inside and outside of MS.
It makes me wonder whether or not a similar project could be undertaken for Linux. It seems that there would be a significant barrier from the severe lack of stable driver APIs, requiring a constant update of the formal specifications. Whatever spec language used would have to be easily maintainable by regular kernel developers as they update the interfaces in each release.
Subscribe to:
Post Comments (Atom)
No comments:
Post a Comment