Capturing and Predicting the Integration Process of an Embedded Software Company

In 2009 TomTom developed a model, called the MFM-model, which should reflect the maturity, feasibility and progression of a Personal Navigation Device software integration project. However, this model did not reflect all required aspects of the integration project and therefore was unable to correctly reflect the maturity, feasibility or...

RAFFS: Model checking a robust abstract flash file store

This thesis presents a case study in modeling and verifying a POSIX-like file store for Flash memory. This work fits in the context of Hoare’s verification challenge and, in particular, Joshi and Holzmann’s mini-challenge to build a verifiable file store. I have designed a simple file store and implemented it in the form of a Promela model. This...