Formal Model of ATM Based on Object Constraint Language (OCL)

Formal methods (FM) are innovative methods which employ mathematical notations to specify explicit and precise requirements. This paper presents a formal model of an automated teller machine (ATM) using Object Constraint Language (OCL) to illustrate the benefits of employing FM to develop commercial applications. FM provide a mathematically rigorous framework for specifying, developing, and verifying software systems. It enhances reliability, robustness, and security. FM plays a crucial role in the context of ATM, which requires high levels of trust and correctness due to their financial and security-critical nature. Using OCL, we demonstrate how formal specifications can be applied to define an ATM system's precise behavior and constraints. It allows for the early detection and correction of errors, reducing development costs and improving overall system quality. This study argues that adopting FM in commercial applications not only boosts the reliability and security of the systems but also increases customer satisfaction and trust. Results of ATM development under OCL have been compared with traditional methods (TM), showing reductions such as 51 % in development time, 53 % in cost, 94 % in ambiguity and 97% in quality and customer trust.