Using Lightweight Formal Methods to Model Class and Object Diagrams

Fernando Valles-Barajas1

  1. Department of Information Technology, Faculty of Engineering, Universidad Regiomontana
    15 de Mayo 567 Pte., C.P. 64000 Colonia Centro, Monterrey, Nuevo Leon, Mexico,


In this paper a formal model for class and object diagrams is presented. To make the model the author used Alloy, which is a threein-one package: a modeling language that constructs software models, a formal method that guides the construction of software models and an analyzer that helps find inconsistencies in software models. In the proposed model the entities that form class and object diagrams, as well as the rules that govern how these elements can be connected, are specified.

Key words

Alloy, Formal Methods, UML

Digital Object Identifier (DOI)

Publication information

Volume 9, Issue 1 (January 2012)
Year of Publication: 2012
ISSN: 1820-0214 (Print) 2406-1018 (Online)
Publisher: ComSIS Consortium

Full text

DownloadAvailable in PDF
Portable Document Format

How to cite

Valles-Barajas, F.: Using Lightweight Formal Methods to Model Class and Object Diagrams. Computer Science and Information Systems, Vol. 9, No. 1, 411-429. (2012),