Navegación

Búsqueda

Búsqueda avanzada

Ensuring the Semantic Correctness of a BAUML Artifact-centric BPM (Summary)

Using models to represent business processes provides several advantages, such as being able to check the correctness of the processes before their implementation. In contrast to traditional process modeling approaches, the artifact-centric approach treats data as a key element of the process, also considering the tasks or activities that are performed in it. This paper presents a way to verify and validate the semantic correctness of an artifact-centric business process model defined using a combination of UML and OCL models – a BAUML model. To do this, we provide a method to translate all BAUML components into a set of logic formulas. The result of this translation ensures that the only changes allowed are those specified in the model, and that those changes are taking place according the order established by the model. Having obtained this logic representation, these models can be validated by any existing reasoning method able to deal with negation of derived predicates. Moreover, we show how to automatically generate the relevant tests to validate the models and we prove the feasibility of our approach.

A characterisation of reliability tools for Software Defined Networks (Trabajo original)

Software Defined Network (SDN) is a new paradigm in networking that introduces great flexibility, allowing the dynamic configuration of parts of the network through centralised programming. SDN has been successfully applied in field networks, and is now being applied to wireless and mobile networks, generating Software Defined Mobile/Wireless networks (SDWNs). SDN can be also combined with Network Function Virtualization (NFV) producing a software network in which the specific hardware is replaced by general purpose computing equipment running SDN and NFV software solutions. This highly programmable and flexible network introduces many challenges from the point of view of reliability (or robustness), and operators need to ensure the same level of confidence as in previous, less flexible deployments. This paper provides a first study of the current tools used to analyse the reliability of SDNs before deployment and/or during the exploitation of the network. Most of these tools offer some kind of automatic verification, supported by algorithms based on formal methods, but they do not differentiate between fixed and mobile/wireless networks. In the paper we provide a number of classifications of the tools to make this selection easier for potential users, and we also identify promising research areas where more effort needs to be made.

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.