Google Drive Formal Model

student project proposal

Google Drive is a widely used cloud file system that allows users to share documents and folders of any kind, and also collaborate in real time on Google format documents (texts, sheets, presentations, drawings, …).

This project is concerned with document, folder and user management aspects of Google Drive only: collaborative aspects will be discarded. The goal is to establish and test a formal model of the retained aspects, exhibit and prove some of its properties, and make sure the model is a theory of the facts.

Although we are mainly interested in conceptual aspects of Google Drive, a useful complementary perspective could be to elaborate a formal model of Google Drive interface(s)[1], and relate an interface to the conceptual model, if time permits.

Context and History

Two student teams started some work on the project, in the context of a GL (S9) class on program specification and proof, and PVS proof assistant (see References below).

The resulting PVS theory is still fairly incomplete, and the few attempted proofs are far too clumsy. A good conceptual model and more elegant PVS theory should yield much simpler proof obligations, and more elegant proofs as well.

No attempt was made to confront the theory to the facts.


Continue previous work, with emphasis on


Means and Advice

Interface Model Perspective

This is optional, and should be considered only if time permits.

It would be interesting and useful to study a generic model of Google Drive interfaces, that is, screen organization, menus, effects of mouse clicks or keyboard input, …

Google is constantly changing Google Drive interfaces, often offering users to switch to the “new interface” (for testing purposes) while conserving the possibility to go back to current interface for a while. It is interesting to see that the “new interface” often forgets important aspects of Google Drive concepts, until Google finds out through user feedback.

However, user feedback is not always the best way to go, because most users do not really understand the important underlying concepts (that they rely upon without knowing), and will primarily be concerned with more cosmetic aspects.

An interface model should be a refinement of the conceptual model theory, implementing all actions. Formally showing that a new interface is a complete refinement of the conceptual model would be valuable.

Even if the new interface is complete wrt the conceptual model, how well does it perform, compared to the previous one? An interesting idea would be to be able to compare interfaces, maybe by using a measure of the minimal number of clicks necessary to perform some action on Google Drive environment.



[1] Google Drive interface keeps changing: the future interface is often available to users for beta testing.