17 Result(s)
-
Chapter
Security Metrics at Work on the Things in IoT Systems
The Internet of Things (IoT) is deeply changing our society. Daily we use smart devices that automatically collect, aggregate and exchange data about our lives. These data are often pivotal when they are used ...
-
Article
Regular and context-free nominal traces
Two kinds of automata are presented, for recognising new classes of regular and context-free nominal languages. We compare their expressive power with analogous proposals in the literature, showing that they e...
-
Chapter and Conference Paper
Refactoring Long Running Transactions
Sagas calculi have been proposed to specify distributed Long Running Transactions (LRT) and, in previous work, a subset of naive sagas has been encoded in the Signal Calculus (SC) to enable their use in servic...
-
Chapter and Conference Paper
ν-Types for Effects and Freshness Analysis
We define a type and effect system for a λ-calculus extended with side effects, in the form of primitives for creating and accessing resources. The analysis correctly over-approximates the sequences of resource a...
-
Chapter
Ugo Montanari and Software Verification
The great honour of introducing the Chapter on Software Verification for the Festschrift dedicated to Ugo Montanari brings to mind a very personal memory. I was a young Ph.D. student and I was discussing somethin...
-
Chapter
Event-Based Service Coordination
In this paper we tackle the problem of designing and implementing a framework for programming service coordination policies. In particular, we illustrate the design and the prototype implementation of Java Sig...
-
Chapter
History Dependent Automata for Service Compatibility
We use History Dependent Automata (HD-Automata) as a syntax-indepentend formalism to check compatibility of services at binding time in Service-Oriented Computing.
-
Chapter and Conference Paper
Types and Effects for Resource Usage Analysis
An extension of the λ-calculus is proposed, to study resource usage analysis and verification. Resources can be dynamically created, and passed / returned by functions; their usages have side effects, represented...
-
Chapter and Conference Paper
Synchronised Hyperedge Replacement as a Model for Service Oriented Computing
This tutorial paper describes a framework for modelling several aspects of distributed computing based on Synchronised Hyperedge Replacement (SHR), a graph rewriting formalism. Components are represented as edges...
-
Chapter and Conference Paper
Checking Risky Events Is Enough for Local Policies
An extension of the λ-calculus is proposed to study history-based access control. It allows for parametrized security policies with a possibly nested, local scope. To govern the rich interplay between local polic...
-
Chapter and Conference Paper
Security-Aware Program Transformations
Stack inspection is a basic mechanism for implementing language based security. Stack inspection is time consuming and may prevent from code optimization. A static analysis is presented that safely approximate...
-
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
The observation algebra of spatial pomsets
For sequential programming, the theory of functions provides a uniform metalanguage to describe behaviours by abstracting from the actual implementation of programs. For concurrent and distributed systems, ins...
-
Chapter and Conference Paper
An extended expansion theorem
Closed CCS (CCCS) is a CCS-like algebra of processes with a generalized form of prefixing based on a full-fledged algebra of transitions rather than on basic actions only. The basic idea is that the generalize...
-
Chapter and Conference Paper
On causality observed incrementally, finally
One of the main problems of the partial ordering approach to the description of computations of concurrent and distributed systems is that there is no operation of sequential composition for partial orders whi...
-
Chapter and Conference Paper
Observational logics and concurrency models
The aim of this paper is to examine some basic topics of true concurrency from the viewpoint of program logics. In particular, logical characterizations of observational (bisimulation) equivalences based on pa...
-
Chapter and Conference Paper
Transition systems with algebraic structure as models of computations
This paper is a tutorial introduction to a general methodology, consisting of categorical constructions, for the definition of new algebraic semantics for transition-based formalisms. The methodology individua...
