Search

The SOAP track aims to bring together researchers and practitioners with the objective of transforming service-oriented programming into a discipline with solid scientific foundations and mature software engineering development methodologies supported by dedicated tools. From the foundational point of view, many attempts to use formal methods for specification and verification in this setting have been made. Session correlation, service types, contract theories and communication patterns are only a few examples of the aspects that have been investigated. Moreover, several formal models based upon automata, Petri nets and algebraic approaches have been developed. However, most of these approaches concentrate on only a few features of service-oriented systems in isolation, and a comprehensive approach is still far from being achieved. From the engineering point of view, there are open issues at many levels. At the system design level, both traditional approaches based on UML and approaches taking inspiration from business process modelling, like BPMN, are used. At the composition level, orchestration and choreography are continuously improved both formally and practically, with an evident need for their integration in the development process. At the description and discovery level, there are two separate communities pushing respectively the semantic approach (like ontologies and OWL) and the syntactic one (like WSDL). In particular, the role of discovery engines and protocols is not clear yet. In this respect, adopted standards are still to be achieved, taking features like Quality of Service, security and dependability into account.

Transition rules with negative premises are needed in the structural operational semantics of programming and specification constructs such as priority and interrupt, as well as in timed extensions of specification languages. The well-known proof-theoretic semantics for transition system specifications involving such rules is based on well-supported proofs for closed transitions. Dealing with open formulae by considering all closed instances is inherently non-modular - proofs are not necessarily preserved by disjoint extensions of the transition system specification. Here, we conservatively extend the notion of well-supported proof to open transition rules. We prove that the resulting semantics is modular, consistent, and closed under instantiation. Our results provide the foundations for modular notions of bisimulation such that equivalence can be proved with reference only to the relevant rules, without appealing to all existing closed instantiations of terms. © 2013 Springer-Verlag.

The SOAP track aims at bringing together researchers and practitioners having the common objective of transforming Service-Oriented Programming (SOP) into a mature discipline with both solid scientific foundations and mature software engineering development methodologies supported by dedicated tools. From the foundational point of view, many attempts to use formal methods for specification and verification in this setting have been made. Session correlation, service types, contract theories, and communication patterns are only a few examples of the aspects that have been investigated. Moreover, several formal models based upon automata, Petri nets and algebraic approaches have been developed. However, most of these approaches concentrate only on a few features of service-oriented systems in isolation, and a comprehensive approach is still lacking. From the engineering point of view, there are open issues at many levels. Among others, at the system design level, both traditional approaches based on UML and approaches taking inspiration from Business Process Modelling, e.g. BPMN, are used. At the composition level, orchestration and choreography are continuously being improved both formally and practically, with an evident need for their integration in the development process. At the description and discovery level, there are two separate communities pushing respectively the semantic approach (like ontologies and OWL) and the syntactic one (like WSDL). In particular, the role of discovery engines and protocols is not clear. In this respect, adopted standards are still missing.

Parameterised Boolean equation systems (PBESs) can be used for solving a variety of verification problems such as model checking and equivalence checking problems. The definition of solution for a PBES is notoriously difficult to understand, which makes them hard to work with. Tan and Cleaveland proposed a notion of proof for Boolean equation systems they call support sets. We show that an adapted notion of support sets called proof graphs gives an alternative characterisation of the solution to a PBES, and prove that minimising proof graphs is NP-hard. Finally, we explain how proof graphs may be used in practice and illustrate how they can be used in equivalence checking to generate distinguishing formulas.

Orchestrators are descriptions at implementation level and may contain sensitive information that should be kept private. Consequently, orchestration languages come equipped with a notion of abstract processes, which enable the interaction among parties while hiding private information. An interesting question is whether an abstract process accurately describes the behavior of a concrete process so to ensure that some particular property is preserved when composing services. In this paper we focus on compliance, i.e, the correct interaction of two orchestrators and we introduce two definitions of abstraction: one in terms of traces, called trace-based abstraction, and the other as a generalization of symbolic bisimulation, called simulation-based abstraction.We show that simulation-based abstraction is strictly more refined than trace-based abstraction and that simulation-based abstraction behaves well with respect to compliance.