Lightweight Modelling, Automatic Analysis And Refinement Of A Library System

Alloy is a little language for formal specification and verification. It offers a declaration syntax compatible with graphical object models, and a set-based formula syntax powerful enough to express complex constraints and yet amenable to a fully automatic semantics analysis. [1]But how can Alloy requirement specification be refined to a suitable implementation? This is what we trying to solve in this paper. In this Paper, we first model a library system, then verify and validate the model. After the that analysis, we refine it down to the executable prototype direction through several stages: Sequential Model, Relational Table Model, Multithread and Simultaneous Model. This article find out ways of refinement. Due to time limitation, the last step is left to be done in the future.