Una perspectiva formal para modelar transacciones de comercio electrónico

Abstract

Muchos modelos de aplicaciones de comercio electrónico utilizan enfoques informales y la intuición humana. aunque su modelo de datos subyacente es sólido. En consecuencia, la mayoría de los diseños contienen inconsistencias y algunos puntos frágiles ocultos que no se manifiestan hasta el se utilizan aplicaciones. Además, los enfoques de diseño informal dejan la determinación de la corrección de los diseños de sistemas a la intuición de los diseñadores. diseño informal Los enfoques no brindan el grado de corrección y confiabilidad requerido para las transacciones de comercio electrónico. Este documento formaliza los requisitos para las transacciones electrónicas utilizando Z. El especi - cación describe las restricciones relacionadas con la singularidad de los clientes, cuentas, productos, y tiendas, a la disponibilidad de productos, a la validez de los clientes y al mantenimiento de fondos suficientes. La especificación formal ha sido verificada mecánicamente utilizando Z/EVES y, por lo tanto, está bien formado en términos de sintaxis y tipos.