Curso Dr. Gerardo Schneider

Lenguajes y herramientas para especificar y validar contratos electrónicos

 

Resumen

El término "contrato" se ha usado tradicionalmente en Computación como una metáfora para describir diferentes tipos de "acuerdos" entre entidades a diferentes niveles de abstracción (objetos, clases, servicios, componentes, etc). A un nivel de abstracción bastante bajo, tales contratos pueden entonces referirse a pre/post-condiciones e invariantes (en programación orientada a objetos), interfaces de comportamiento (en desarrollo de componentes), y "service-level agreements" (en arquitectura orientada a servicios, SOA), para mencionar unos pocos. Por otro lado, los contratos también existen a mas altos niveles de abstracción en donde existe uno o mas clientes (usuarios) y proveedores, en general personas y no entidades abstractas: especificaciones de software, requerimientos de usuarios, descripciones de "workflow", y naturalmente contratos legales.

Algunos de los tipos de contratos descritos más arriba podrían ser considerados no como tales sino simplemente como propiedades ya que es posible determinar (estáticamente) si son verdaderos (no hay posibilidad de violarlos) o falsos (no hay forma de satisfacerlos). La descripción y análisis de tales contratos ha sido objeto de estudio en varias áreas en Computación (por ejemplo usando lógica temporal). Los casos interesantes y da aplicación mas general son aquellos "contratos" que son sujetos a ser violados (como sucede en el área judicial) y que por lo tanto precisan ser "monitoreados" en tiempo real (por ejemplo, una obligación no tiene valor de verdad: puede ser satisfecha o violada pero nada se sabe en general hasta que una situación real lo determine).

Muchas preguntas se podrían hacer sobre cada contrato, como por ejemplo:

  • Contiene contradicciones?
  • Es posible determinar cuales son las cláusulas que nos conciernen y que responsabilidad conllevan?
  • Cuáles son nuestros derechos/obligaciones?
  • Bajo que condiciones el contrato nos obliga a hacer algo específico y cuáles son las penalidades asociadas en caso de no cumplimiento?

Para poder responder a tales (y similares) preguntas es necesario formalizar la noción de contrato y definir algoritmos y herramientas para su análisis.

En este curso discutiremos trabajos de investigación reciente en la especificación y análisis de contratos electrónicos, incluyendo una descripción general del área y de los desafíos existentes. En particular presentaremos el lenguaje formal CL en el cual es posible representar obligaciones, permisos y prohibiciones, así como cuales son las penalidades en caso de violación de obligaciones y prohibiciones. Mostraremos las ventajas y desventajas de CL, y describiremos técnicas y herramientas para validar contratos escritos en CL.


Contenido general (Preliminar)

  1. Introducción. Usos de "contratos" en Computación.
  2. Desafíos en el diseño y análisis de contratos electrónicos
  3. El lenguaje de especificación de contratos CL
  4. AnaCon: framework para análisis de contratos en CL
  5. Discusión sobre el estado del arte y problemas abiertos del área.

 

Bibliografía

Cristian Prisacariu and Gerardo Schneider. CL: An Action-based Logic for Reasoning about Contracts. In 16th Workshop on Logic, Language, Information and Computation (WOLLIC'09), volume 5514 of LNCS, pages 335-349, Tokyo, Japan, June 2009. Springer.

Stephen Fenech, Gordon J. Pace, and Gerardo Schneider. Clan: A tool for contract analysis and conflict discovery. In 7th International Symposium on Automated Technology for Verification and Analysis (ATVA'09), volume 5799 of LNCS, pages 90-96, Macao, China, October 2009. Springer.

Gordon Pace, Cristian Prisacariu, and Gerardo Schneider. Model checking contracts -a case study. In 5th International Symposium on Automated Technology for Verification and Analysis (ATVA'07), volume 4762 of LNCS, pages 82-97, Tokyo, Japan, October 2007. Springer-Verlag.

Gordon J. Pace and Gerardo Schneider. Challenges in the specification of full contracts. In Integrated Formal Methods (iFM'09), volume 5423 of LNCS, pages 292-306, Düseldorf, Germany, February 2009.