Behavioral modeling

DRANK

In this second chapter we will explain the basics of behavioral modeling with Alloy. As running example we will explore the design of a simple file sharing web application, where a user can upload files making them available for others to download, provided that they have access to a unique single-use token that was associated with shared files. Moreover, uploaded files can be deleted, but the user can for a while undo this action: deleted files are moved to a trash bin from where they can be restored. Upon explicit user request or after a certain period of time, the trash bin is automatically emptied, making all files in it no longer available.More specifically, in this chapter we will show how Alloy can be used in the following design tasks:Formally specify, at a very abstract level, the structure and behavior of this web app.Validate this specification by simulation, namely using the Alloy Analyzer to check that it allows some of the expected behaviors.Verify that this specificatio…