Software Adaptation is a hot topic in Software Engineering since it is the only way to compose non-intrusively black-box components or services with mismatching interfaces. However, adaptation is a ...complex issue especially when behavioral descriptions of services are considered. This paper presents optimised techniques to generate adaptor protocols, being given a set of service interfaces involved in a composition and an adaptation contract. In this work, interfaces are described using a signature, and a protocol that takes value passing into account. Our proposal is completely supported by tools that automate the generation and the verification of the adaptor protocols. Last, we show how our adaptation techniques are implemented into BPEL.
Checking business process evolution Krishna, Ajay; Poizat, Pascal; Salaün, Gwen
Science of computer programming,
01/2019, Letnik:
170
Journal Article
Recenzirano
Odprti dostop
Business processes support the design and implementation of software as workflows of local and inter-organisation activities. Tools provide the business process designer with modelling and execution ...facilities, but they barely provide formal analysis techniques. When one makes a process evolve, for example by refactoring it or by adding new features in it, it is important to be able to check whether, and how, this process has changed, and possibly correct evolution flaws. To reach this objective, we first present a model transformation from the BPMN standard notation to the LNT process algebra and LTS formal models. We then propose a set of relations for comparing business processes at the formal model level. With reference to related work, we propose a richer set of comparison primitives supporting renaming, refinement, property and context-awareness. We also support BPMN processes containing unbalanced structures among gateways. In order to make the checking of evolution convenient for business process designers, we have implemented tool support for our approach as a web application.
•A model transformation from BPMN to LTS that deals with unbalanced workflows.•Evolution relations for business processes based on formal behavioural relations.•An abstract intermediate meta model and format for business processes, PIF.•Our VBPMN tool that implements model transformation and evolution checking.
Choreography supports the specification, with a global perspective, of the interactions between roles played by peers in a collaboration. Choreography conformance testing aims at verifying whether a ...set of distributed peers collaborates wrt. a choreography. Such collaborations are usually achieved through information exchange, thus taking data into account during the testing process is necessary. We address this issue by using a non-intrusive passive testing approach based on functional properties. A property can express a critical (positive or negative) behavior to be tested on an isolated peer (locally) or on a set of peers (globally). We support online verification of these kind of properties against local running traces of each peer in a distributed system where no global clock is needed. Our framework is fully tool supported.
The BPMN standard notation allows business process designers to model both intra-organizational processes and inter-organizational collaborations. A great effort has been devoted in proposing formal ...semantics for BPMN, and, fewer, in providing dedicated verification tools. Still, some advanced features of BPMN, namely communication or time-related constructs, are often set aside. This becomes an issue as BPMN gains interest outside of its original scope, e.g., for the IoT where communication and time play an important role. In this paper, we propose a formal semantics for a subset of BPMN. This semantics takes into account not only the usual gateways, but also sub-processes, inter-process communication, and time-related constructs. In contrast to transformational approaches, which give a semantics to BPMN by mapping it to some formal model (e.g., transition systems or Petri nets), our approach is based on a direct formalization in first-order logic that is then realized in a straightforward way into the TLA+ formal language. We build on the TLA+ model-checker, TLC, to provide process designers with a verification framework, fbpmn, that one may use to check BPMN and workflow specific properties. Our tools and our model database are open source and freely available online.
•A direct formal semantics for a subset of BPMN, including sub-processes, communication and time constructs.•Automated verification of intra-organization workflows and inter-organization collaborations.•Seven models for communication, two models for time.•Communication models and properties of interest are easily extensible.•Open source and freely available tools and model repository.
Component-Based Software Engineering focuses on the reuse of existing software components. In practice, most components cannot be integrated directly into an application-to-be, because they are ...incompatible. Software Adaptation aims at generating, as automatically as possible, adaptors to compensate mismatch between component interfaces, and is therefore a promising solution for the development of a real market of components promoting software reuse. In this article, we present our approach for software adaptation which relies on an abstract notation based on synchronous vectors and transition systems for governing adaptation rules. Our proposal is supported by dedicated algorithms that generate automatically adaptor protocols. These algorithms have been implemented in a tool, called Adaptor, that can be used through a user-friendly graphical interface.
Reuse and composition are increasingly advocated and put into practice in modern software engineering. However, the software entities that are to be reused to build an application, e.g., services, ...have seldom been developed to integrate and to cope with the application requirements. As a consequence, they present mismatch, which directly hampers their reusability and the possibility of composing them. Software Adaptation has become a hot topic as a nonintrusive solution to work mismatch out using corrective pieces named adaptors. However, adaptation is a complex issue, especially when behavioral interfaces, or conversations, are taken into account. In this paper, we present state-of-the-art techniques to generate adaptors given the description of reused entities' conversations and an abstract specification of the way mismatch can be solved. We use a process algebra to encode the adaptation problem, and propose on-the-fly exploration and reduction techniques to compute adaptor protocols. Our approach follows the model-driven engineering paradigm, applied to service-oriented computing as a representative field of composition-based software engineering. We take service description languages as inputs of the adaptation process and we implement adaptors as centralized service compositions, i.e., orchestrations. Our approach is completely tool supported.
Choreographies are contracts specifying from a global point of view the legal interactions that must take place among a set of services. Such a contract may serve as a reference in the development of ...concurrent distributed system, whether it is achieved following a top-down or a bottom-up approach. In this article, we present VerChor, a generic, modular, and extensible framework for supporting the development based on choreographies. It relies on a choreography intermediate format (CIF) into which several existing choreography description languages can be transformed. VerChor builds around a set of formal properties whose verification is central to choreography-based development. To support this development process, we propose a connection between CIF and the CADP verification toolbox, which enables the full automation of the aforementioned properties. Finally, we illustrate a practical use of the VerChor framework through its integration with the Eclipse BPMN 2.0 designer.
PDF
