![Loading...](https://link.springer.com/static/c4a417b97a76cc2980e3c25e2271af3129e08bbe/images/pdf-preview/spacer.gif)
-
Chapter
Quantitative Analysis of Services
We show a number of applications of the tools which have been developed within the sensoria project to perform quantitative analysis of services. These tools are formally grounded on source calculi which allow th...
-
Chapter and Conference Paper
Approximate Model Checking of Stochastic COWS
Given the description of a model and a probabilistic formula, approximate model checking is a verification technique based on statistical reasoning that allows answering whether or not the model satisfies the ...
-
Chapter and Conference Paper
A Tool for Checking Probabilistic Properties of COWS Services
We present a tool developed for fostering probabilistic model checking of services formally specified in Scows, a stochastic enrichment of the Calculus for Orchestration of Web Services. The tool, called Scows_lt...
-
Chapter and Conference Paper
BlenX Static and Dynamic Semantics
We introduce a new programming language called BlenX. It is strongly inspired to process calculi and it is an evolution of Beta-binders. It has been specifically designed and implemented to model and simulate bio...
-
Chapter
Process Calculi Abstractions for Biology
Several approaches have been proposed to model biological systems by means of the formal techniques and tools available in computer science. To mention just a few of them, some representations are inspired by ...
-
Chapter and Conference Paper
BlenX4Bio – BlenX for Biologists
We introduce BlenX4Bio, a high-level interface for the programming language BlenX. BlenX4Bio allows biologists to write BlenX programs without having any programming skills. The main elements of a biological mode...
-
Chapter and Conference Paper
Formal Analysis of BPMN Via a Translation into COWS
A translation of the Business Process Modeling Notation into the process calculus COWS is presented. The stochastic extension of COWS is then exploited to address quantitative reasoning about the behaviour of ...
-
Chapter
On Beta-Binders Communications
Beta-binders is a bio-inspired formalism with a formal reduction semantics in the process calculi style. The terms of the language are boxes with an internal processing engine and provided with interfaces for ...
-
Chapter and Conference Paper
Stochastic COWS
A stochastic extension of COWS is presented. First the formalism is given an operational semantics leading to finitely branching transition systems. Then its syntax and semantics are enriched along the lines o...
-
Chapter and Conference Paper
Beta Binders for Biological Interactions
This paper presents binders and operators, in the process calculi tradition, to reason about biological interactions.
-
Chapter and Conference Paper
Model Checking Biological Systems Described Using Ambient Calculus
We propose a way of performing model checking analysis for biological systems. The technics were developed for a CTL* logic built upon Ambient Calculus.
-
Chapter and Conference Paper
Performance Analysis of a UML Micro-business Case Study
This paper presents a technique to carry out performance analysis of UML specifications. We consider UML specifications composed of activity, sequence and deployment diagrams. Specifications are translated int...
-
Chapter and Conference Paper
Modeling Kohn Interaction Maps with Beta-Binders: An Example
We represent a subset of the mammalian cell cycle Kohn interaction map using Beta-binders, a formalism inspired to the pi-calculus and enriched with binders that allow the description of enclosing surfaces equ...
-
Chapter
Operational Patterns in Beta-Binders
As a preliminary step in testing the expressiveness of Beta-binders against realistic case studies, we comment on a number of operational properties of the formalism and present a set of derived patterns that ...
-
Chapter and Conference Paper
On Synchronous and Asynchronous Mobile Processes
This paper studies the relationship between synchronous and asynchronous mobile processes, in the setting of the π-calculus. A type system for processes of the asynchronous monadic subcalculus is introduced and u...
-
Chapter and Conference Paper
Pi-Congruences as CCS Equivalences
We show the coincidence of non-ground π-calculus and πξ-calculus, a CCS-like calculus that allows processes to be explicitly represented as temporary functions of input parameters, and as permanent functions o...
-
Chapter and Conference Paper
On encoding pπ in mπ
This paper is about the encoding of pπ, the polyadic π-calculus, in mπ, the monadic π-calculus. A type system for mπ processes is introduced which captures the interaction regime underlying the encoding of pπ pro...
-
Chapter and Conference Paper
The weak late π-calculus semantics as observation equivalence
We show that the Weak Late π-calculus semantics can be characterized as ordinary Observation congruence over a specialized transition system where both the instantiation of input placeholders and the name substit...
-
Chapter and Conference Paper
A π-calculus with explicit substitutions: The late semantics
A new formulation of the π-calculus, where name instantiation is handled explicitly, is presented. The explicit handling of name instantiation allows us to reduce the π-calculus transitional semantics to a standa...
-
Chapter and Conference Paper
A fully parallel calculus of synchronizing processes
We propose a fully parallel calculus of synchronizing processes. The calculus was deeply inspired by LOTOS, of which it inherits multi-party synchronization in process parallel composition. On the other hand, its...