Verifying BON models with alloy

Authors

  • 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

Keywords:

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

Abstract

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.

Downloads

Download data is not yet available.

References

[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.

Downloads

Published

2005-12-01

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 https://journal.info.unlp.edu.ar/JCST/article/view/850

Issue

Vol. 5 No. 04 (2005): Sixteenth Issue

Section

Original Articles

License

 

Copyright and Licensing

Articles accepted for publication will be licensed under the Creative Commons BY-NC-SA. Authors must sign a non-exclusive distribution agreement after article acceptance.