Verifying BON models with alloy


  • Ramiro Adrián Demasi Dpto. de Computación, Universidad Nacional de Río Cuarto, Río Cuarto, Argentina
  • Pablo Daniel Ponzio Dpto. de Computación, Universidad Nacional de Río Cuarto, Río Cuarto, Argentina
  • Pablo Francisco Castro Department of Computing and Software, McMaster University Hamilton, Canada
  • Gabriel Alfredo Baum LIFIA, Universidad Nacional de La Plata, La Plata, Argentina


BON, Alloy, Formal Methods, Software Engineering, Object Oriented Languages, Architectural Models


In this paper we describe a methodology to translate BON (architectural) designs to Alloy specifications. The main virtue of this process is that it can be implemented by means of software tools. The utilization of this methodology during the software development allows designers to validate different kinds of properties over their BON models. Allowing, in this way, the finding of critical bugs in earlier steps of system construction. Finally, we present a software which implements this translation from BON to Alloy.


Download data is not yet available.


[1] Kim Waldn and Jean-Marc Nerson. “Seamless Object-Oriented Software Architecture”. Addison-Wesley 1994.
[2] Richard F. Paige. “An Introduction to BON”. August 1999.
[3] Castro Pablo, Baum Gabriel. “Integrando BON con Alloy”. CACIC 2003.
[4] D. Jackson. “Micromodels of Software: Lightweight Modeling and Analysis with Alloy”. February 2002.
[5] D. Jackson. “Alloy 3.0 Reference Manual”. May 2004.
[6] Richard F. Paige and Jonathan S. Ostroff. “A Comparison of Business Object Language and the Unified Modeling Language”. May 1999.
[7] B. Meyer. “Object-oriented software construction”. Prentice-Hall. New Jersey, 1988.
[8] C.A.R. Hoare. “An Axiomatic Basis for Computer Programming,” Communications of the ACM, Oct. 1969.




How to Cite

Demasi, R. A., Ponzio, P. D., Castro, P. F., & Baum, G. A. (2005). Verifying BON models with alloy. Journal of Computer Science and Technology, 5(04), p. 292–298. Retrieved from



Original Articles