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), 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).
- Fall 2012-2013: the project was initiated. A first very partial sketch of the model was elaborated using PVS. The main idea of the model is to interpret each user action as a state transformer. A state represents all Google Drive users, documents and folders in the world, and their relations (containment for documents and folders, ownership, level of access for users, documents and folders). Students did not attempt to carry proof obligations arising from type checking;
- Fall 2013-2014: the project was continued by another team. The conceptual model was refined, for instance by representing more access rights, and user actions. Some proof obligations were analyzed, and some proofs were carried out or started. As a result, some flaws in the previous model were detected and corrected.
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
- Completing the theory of Google Drive conceptual model: for example, deleting documents or folders has not been specified;
- Theory and proof elegance: clumsy proofs should be replaced with elegant ones, close to intuitive ideas;
- Make sure the PVS specification of Google Drive conceptual model is a theory of the facts: write a theory of examples and show that these theoretical examples map Google Drive experimental observations on the same examples;
- Exhibit and establish properties of Google Drive conceptual model, for instance: the state resulting from a sequence of actions does not depend upon their order in the sequence; alternatively, exhibit Google Drive flaws, and suggest improvements.
- Learn about PVS proof assistant;
- Learn about Google Drive environment;
- Understand previous work;
- Search for similar work on the Web;
- List what is missing from Google Drive PVS current theory wrt Google Drive concepts;
- Complete and improve theory, thus minimizing and simplifying proof obligations;
- Find natural and simple proofs of proof obligations;
- Write a theory of examples, develop proof strategies for mimicking execution of concrete actions;
- Observe that the examples yield the same results as actual experiments under Google Drive;
- Imagine properties of the conceptual model, write a corresponding theory, and prove it;
- If time permits, establish a formal model of Google Drive interfaces (see Perspective).
Means and Advice
- Set up a good communication environment, based on Google Drive and Google Groups: eventually register to existing IT30405 Google group, and/or create a new group dedicated to the project (and invite me);
- Share your main project folder with me and all team members;
- I will be available for help on PVS, Google Drive, and the project in general, either physically or through Google Hangout (through paul.gloess AT enseirb.fr identifier), and by phone;
- When it comes to specification, my advice is to quickly specify directly under PVS, rather than on a piece of paper or informal text document, because PVS actually helps you specify, by pointing out flaws, incoherence, through unprovable proof obligations;
- When it comes to proofs, my advice is to have a clear idea of the proof (not necessary too detailed), and write it down, before you start it under PVS, because there are so many ways to design clumsy (sometimes infinite) proofs with a proof assistant;
- Elegance and simplicity of the specification minimizes the number and/or complexity of proof obligations, and thus saves you a lot of tedious work.
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.
 Google Drive interface keeps changing: the future interface is often available to users for beta testing.