Skip to main content
Fachgebiete
Automobil + Motoren Bauwesen + Immobilien Business IT + Informatik Elektrotechnik + Elektronik Energie + Nachhaltigkeit Finance + Banking Management + Führung Marketing + Vertrieb Maschinenbau + Werkstoffe Versicherung + Risiko
DE
EN
Themenseiten
Organisationspsychologie Projektmanagement Marketing Smart Manufacturing
Bücher
Zeitschriften
Weitere Formate
Podcasts Webinare Technik Webinare Wirtschaft Kongresse Veranstaltungskalender Awards
Jetzt Einzelzugang starten
Zugang für Unternehmen
Referenzkunden
MTZ-Fachkongress

Antriebe und Energiesysteme von morgen


Austausch von Automobil- und Energiewirtschaft

Am 14./15. Mai geht es in Chemnitz um die Mobilitätswende durch Elektro- und Wasserstofffahrzeuge.
Erweiterte Suche
Anmelden
nach oben

2016 | Buch

Kickstarting Choreographic Programming Kapitel lesen Erstes Kapitel lesen

Web Services, Formal Methods, and Behavioral Types

11th International Workshop, WS-FM 2014, Eindhoven, The Netherlands, September 11-12, 2014, and 12th International Workshop, WS-FM/BEAT 2015, Madrid, Spain, September 4-5, 2015, Revised Selected Papers

herausgegeben von: Thomas Hildebrandt, António Ravara, Jan Martijn van der Werf, Matthias Weidlich

Verlag: Springer International Publishing

Buchreihe : Lecture Notes in Computer Science

Enthalten in: Springer Professional "Wirtschaft+Technik" , Springer Professional "Technik" , Springer Professional "Wirtschaft"

Einloggen, um Zugang zu erhalten
insite
SUCHEN

Über dieses Buch

This volume contains the refereed joint proceedings of two initiatives that have been devoted to the formal foundations of complex systems: the WS-FM:FASOCC 2014 and WS-FM/BEAT 2015 workshops.
The 11th International Workshop on Web Services and Formal Methods: Formal Aspects of Services-Oriented and Cloud Computing, WS-FM 2014, took place in Eindhoven, The Netherlands, in September 2014. The 12th International Workshop on Web Services, Formal Methods, and Behavioral Types, WS-FM 2015, took place in Madrid, Spain, in September 2015.
The total of 8 papers presented in this volume was carefully reviewed and selected from 18 submissions. They were organized in topical sections named: expressiveness of behavioral models; service-oriented systems, and behavioral types.

Inhaltsverzeichnis

Frontmatter

Invited Talk

Frontmatter
Kickstarting Choreographic Programming
Abstract
We present an overview of some recent efforts aimed at the development of Choreographic Programming, a programming paradigm for the production of concurrent software that is guaranteed to be correct by construction from global descriptions of communication behaviour.
Fabrizio Montesi

Expressiveness of Behavioral Models

Frontmatter
On the Suitability of Generalized Behavioral Profiles for Process Model Comparison
Abstract
Given two process models, the problem of behavioral comparison is that of determining if these models are behaviorally equivalent (e.g., by trace equivalence) and, if not, identifying how can the differences be presented in a compact manner? Behavioral profiles have been proposed as a convenient abstraction for this problem. A behavioral profile is a matrix, where each cell encodes a behavioral relation between a pair of tasks (e.g., causality or conflict). Thus, the problem of behavioral comparison can be reduced to matrix comparison. It has been observed that while behavioral profiles can be efficiently computed, they are not accurate insofar as behaviorally different process models may map to the same behavioral profile. This paper investigates the question of how accurate existing behavioral profiles are. The paper shows that behavioral profiles are fully behavior preserving for the class of acyclic unlabeled nets with respect to configuration equivalence. However, for the general class of acyclic nets, existing behavioral profiles are exponentially inaccurate, meaning that two acyclic nets with the same behavioral profile may differ in an exponential number of configurations.
Abel Armas-Cervantes, Marlon Dumas, Luciano García-Bañuelos, Artem Polyvyanyy
Formal Verification of Petri Nets with Names
Abstract
Petri nets with name creation and management have been recently introduced so as to make Petri nets able to model the dynamics of (distributed) systems equipped with channels, cyphering keys, or computing boundaries. While traditional formal properties such as boundedness, coverability, and reachability, have been thoroughly studied for this class of Petri nets, formal verification against rich temporal properties has not been investigated so far. In this paper, we attack this verification problem. We introduce sophisticated variants of first-order \(\mu \)-calculus to specify rich properties that simultaneously account for the system dynamics and the names present in its states. We then analyse the (un)decidability boundaries for the verification of such logics, by considering different notions of boundedness. Notably, our decidability results are obtained via a translation to data-centric dynamic systems, a recently devised framework for the formal specification and verification of business processes working over relational database with constraints. In this light, our results contribute to the cross-fertilization between areas that have not been extensively related so far.
Marco Montali, Andrey Rivkin

Service-Oriented Systems

Frontmatter
Modeling and Formal Analysis of a Client-Server Application for Cloud Services
Abstract
In the context of Cloud computing, a service can be invoked by distinct devices having different HW/SW characteristics; therefore, the content must be adapted to each device profile. A solution consists in having a middleware server that receives requests from the clients, forwards them to the cloud, and adapts the answers coming from the cloud on the base of device profiles. This paper proposes a formalization of this framework using Abstract State Machines (ASMs). The modeling process is based on the ASMs refinement method, and has been guided and supported by several validation and verification activities to guarantee consistency, correctness, and reliability properties.
Paolo Arcaini, Roxana-Maria Holom, Elvinia Riccobene
An Event-Based Approach to Runtime Adaptation in Communication-Centric Systems
Abstract
This paper presents a model of session-based concurrency with mechanisms for runtime adaptation. Thus, our model allows to specify communication-centric systems whose session behavior can be dynamically updated at runtime. We propose an event-based approach: adaptation requests, issued by the system itself or by its environment, are assimilated to events which may trigger runtime adaptation routines. Based on type-directed checks, these routines naturally enable the reconfiguration of processes with active sessions. We develop a type system that ensures communication safety and consistency properties: while the former guarantees absence of runtime communication errors, the latter ensures that update actions do not disrupt already established sessions.
Cinzia Di Giusto, Jorge A. Pérez
Designing Efficient XACML Policies for RESTful Services
Abstract
The popularity of REST grows more and more and so does the need for fine-grained access control for RESTful services. Attribute Based Access Control (ABAC) is a very generic concept that generalizes multiple different access control mechanisms. XACML is an implementation of ABAC based on XML and is established as a standard solution. Its flexibility opens the opportunity to specify detailed security policies. But on the other hand it has some drawbacks regarding maintenance and performance when the complexity of security policies grows. Long processing times for authorization requests are the consequence in environments that require fine-grained access control. We describe how to design a security policy in a resource oriented environment so that its drawbacks are minimized. The results are faster processing times for access requests and a guideline to structure security policies for RESTful services easing their maintenance.
Marc Hüffmeyer, Ulf Schreier

Behavioral Types

Frontmatter
Type Inference for Session Types in the -calculus
Abstract
In this paper we present a direct algorithm for session type inference for the \(\pi \)-calculus. Type inference for session types has previously been achieved by either imposing limitations and restriction on the \(\pi \)-calculus, or by reducing the type inference problem to that for linear types. Our approach is based on constraint generation and solving. We generate constraints for a process based on its syntactical components, and afterwards solve the generated constraints in a predetermined order. We prove the soundness, completeness, and termination of this approach.
Eva Fajstrup Graversen, Jacob Buchreitz Harbo, Hans Hüttel, Mathias Ormstrup Bjerregaard, Niels Sonnich Poulsen, Sebastian Wahl
Type Checking Purpose-Based Privacy Policies in the -Calculus
Abstract
In this paper we propose a formal framework for studying privacy preserving policies based on the notion of purpose. Our framework employs the \(\pi \)-calculus with groups accompanied by a type system for capturing privacy requirements. It also incorporates a privacy policy language which captures how different entities within a system, which are distinguished by their roles, may access sensitive information and the purposes for which they are allowed to process the data. We show that a system respects a policy if the typing of the system is compatible with the policy. We illustrate our methodology via analysis of privacy-aware services of a health-care system.
Eleni Kokkinofta, Anna Philippou
On the Decidability of Honesty and of Its Variants
Abstract
We address the problem of designing distributed applications which require the interaction of loosely-coupled and mutually distrusting services. In this setting, services can use contracts to protect themselves from unsafe interactions with the environment: when their partner in an interaction does not respect its contract, it can be blamed (and punished) by the service infrastructure. We extend a core calculus for services, by using a semantic model of contracts which subsumes various kinds of behavioural types. In this formal framework, we study some notions of honesty for services, which measure their ability to respect contracts, under different assumptions about the environment. In particular, we find conditions under which these notions are (un)decidable.
Massimo Bartoletti, Roberto Zunino
Backmatter
Metadaten
Titel
Web Services, Formal Methods, and Behavioral Types
herausgegeben von
Thomas Hildebrandt
António Ravara
Jan Martijn van der Werf
Matthias Weidlich
Copyright-Jahr
2016
Electronic ISBN
978-3-319-33612-1
Print ISBN
978-3-319-33611-4
DOI
https://doi.org/10.1007/978-3-319-33612-1

Premium Partner

    Bildnachweise