Búsqueda avanzada

Timed Automata and Model Checking to Verify Business Processes


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 enterprise­project 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 BP­task 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 BP­task model with respect to the initial property specification derived from the business rules.

Palabras Clave:

Business process - Model checking - Timed automata - Uppaal tool - Verification





Este artículo tiene una licencia de uso CreativeCommons - Reconocimiento (by)

Ver la referencia en formato Bibtex