Formal Methods: A Practical Tool For OS Implementors

Patrick Tullmann

University of Utah

Presented at HOTOS-VII, May 1997

Formal Methods: A Practical Tool For OS Implementors

Formal Methods and Operating Systems

Overview of FM Tools

Modeling IPC in Fluke

Our Approach

Issues

Conclusions

Translation Example

SPIN

Specific Results