La mayoría de los métodos de desarrollo de software orientado a objetos imponen ciertos conceptos que son generalmente aceptados. Frameworks y patterns expresan ejemplos de buenas prácticas que pueden usarse para alcanzar resultados más efectivos [Bus96]. Pero en algunos casos particulares, es necesario una especificación formal que pueda verificarse a fin de producir sistemas mús seguros.
Los patrones de Gamma [Gam95] (GoF patterns) desempeñan varios roles en el proceso de desarrollo orientado a objetos: proveen un vocabulario común para diseño; constituyen una base de experiencia para construir software reusable; y actúan como elementos básicos a partir de los cuales pueden construirse diseños más complejos. Una notación más formal que permita especificar en forma más segura, consistente y completa es todavía un desafío. Un primer trabajo en esa dirección [EdeA] representa patrones como formulas de LePus, un lenguaje definido como un fragmento de la lógica de primer orden [EdeB]. En [Mik98] se presenta un modelo abstracto de patrones, construido usando el método DisCo que se fundamenta en la lógica temporal.
En este resumen, presentamos nuestro modelo formal de patrones [Cec99B] basado en RSL (RAlSE Specification Language) [Geo92], y el estado actual de su desarrollo. Futuras extensiones son abordadas al final.