Most real-world programs interact with their environment in non-trivial ways, most often through the operating system. This poses significant problems for verification, which is easier to perform on so-called ‘closed’ programs which have no such interactions. A common method of dealing with this problem is by combining the program under verification with a suitable model of its environment. This model can vary widely in complexity; however, more realistic models lead to more satisfactory and relevant verification results. A major component of this model is the operating system. DiOS, then, is a pre-made model operating system, part of the DIVINE verification toolset.

Since DiOS was first implemented, support for data non-determinism in DIVINE has been significantly improved, but DiOS does not make use of these capabilities yet. Most importantly, the initial content of the file system is a fixed snapshot, and outside influences on its evolution are not modelled. The goal of this thesis is to rectify this shortcoming, by providing an implementation of non-deterministic file system component for DiOS. This component should make it possible to take advantage of both symbolic and abstract verification methods now available in DIVINE to improve veracity and flexibility of the modelled environment. The implementation should additionally include a re-usable component which encapsulates the interface for creating and constraining non-deterministic data between the rest of DiOS and the verifier.