Applying Event and Machine Decomposition to a Flash-Based Filestore in Event-B