Resumen:
Currently, the use of Software Engineering methods has been shown to be useful in improving business modelling techniques as a result of their application to Business Process (BP)modelling initiatives. Nowadays when the business process needs to be supported by Information Technology, the Unified Modeling Language (UML) is widely used for modelling. This paper presents the use of Timed Automata (TA) and Model Checking (MC) by their application to an example of a BP enterpriseproject related to the Customer Relationship Management (CRM) business. The Uppaal tool is used in this work. With this proposal, the analysts and designers are supported in the development of the BPtask model associated with a BP design by using UML as the main modelling language. The application of the proposal is aimed at ensuring the correctness of the BPtask model with respect to the initial property specification derived from the business rules.