摘要：In this paper we describe a methodology to trans-late BON (architectural) designs to Alloy specifi-cations. The main virtue of this process is that itcan be implemented by means of software tools.The utilization of this methodology during thesoftware development allows designers to validatedi.erent kinds of properties over their BON mo d-els. Allowing, in this way, the finding of criti-cal bugs in earlier steps of system construction.Finally, we present a software which implementsthis translation from BON to Alloy
