1,721,088 research outputs found
Some Concurrency Models in a Categorical Framework
No full textThe paper defines a taxonomy of concurrent models.
Concurrent models are seen as categories and passages
between models as functors.
We particularly care about the notions of concurrency, causal and temporal
dependencies and their possible different perception. According to the chosen
model, only part of these notions are, indeed, relevant and recoverable
from the
observation of a concurrent system
A Control Flow Analysis for Beta-binders with and without Static Compartments
No full textWe introduce a Control Flow Analysis, that statically approximates the dynamic behaviour of processes, expressed in the Beta-binders calculus and in an extended version of the calculus modelling static compartments. Our analysis of a system is able to describe the essential behaviour of each box, tracking all the possible bindings of variables, all the possible intra- and inter-boxes communications, and, finally, all the possible movements across compartments. The analysis offers a basis for establishing static checks of biological dynamic properties. We apply our analysis to an abstract specification of the interaction between a virus and cells of the immune system and to a model of the cAMP-signaling Pathway in Olfactory Sensory Neurons
Securing IoT communications: at what cost?
Full text linkIoT systems use wireless links for local communication, where locality depends on the
transmission range and include many devices with low computational power such as sensors.
In IoT systems, security is a crucial requirement, but difficult to obtain, because standard cryptographic techniques have a cost
that is usually unaffordable.
We resort to an extended version of the process calculus LySa, called IoTLySa,
to model the patterns of communication of IoT devices.
Moreover, we assign rates to each transition
to infer quantitative measures on the specified systems.
The derived performance evaluation can be exploited to
establish the cost of the possible security countermeasures
A Static Analysis for Beta-Binders
No full textAbstractWe introduce a Control Flow Analysis, that statically approximates the dynamic behaviour of processes, expressed in the Beta-Binders calculus. Our analysis of a system is able to describe the essential behaviour of each box, tracking all the possible bindings of variables and all the possible intra- e inter-boxes communications. The analysis offers a basis for establishing static checks of biological dynamic properties. We finally apply our analysis to an example, based on an abstract specification of the interaction between a virus and cells of the immune system
True Concurrency via Abstract Interpretation
No full textAbstract interpretation can be used to formalize the concept of parametricity in the concurrency field. The concrete domain is the proved transition system, whose transitions are labelled by encodings of the parallel structure of processes. Suitable relabelling functions of proved transitions allow us to retrieve many non interleaving models presented in the literature. We prove here that such relabelling functions are indeed abstraction functions in the sense of abstract interpretations, considering causality as a test-bed. They induce Galois connections between the concrete domain and the abstract semantic models. We prove that abstractions preserve non interleaving bisimulations
Brane Calculi Systems: A Static Preview of their Possible Behaviour
No full textWe improve the precision of a previous Control Flow Analysis for Brane Calculi, by adding information on the context and introducing causality information on the membranes. This allows us to prove some biological properties on the behaviour of systems specified in Brane Calculi
Il bivio di Alan
No full textIl 17 febbraio 2012, centenario della nascita di Alan Turing, il Dipartimento di Informatica
dell’Università di Pisa ha organizzato una giornata celebrativa. Eccone un resoconto
Tracking sensitive and untrustworthy data in IoT
Full text linkThe Internet of Things (IoT) produces and processes large amounts of data. Among
these data, some must be protected and others must be carefully handled because they
come from untrusted sources. Taint analysis techniques can be used to for marking data and for monitoring their propagation at run time, so to determine how they influence the rest of the computation.
Starting from the specification language IoT-LySa, we propose
a Control Flow Analysis for statically predicting how tainted data spread across an IoT system and for checking whether those computations considered security critical are not affected by tainted data
The cost of securing IoT communications
Full text linkMore smart objects and more applications on the Internet of Things (IoT) mean more security challenges. In IoT security is crucial but difficult to obtain. On the one hand the usual trade-off between highly secure and usable systems is more impelling than ever; on the other hand security is considered a feature that has a cost often unaffordable. To relieve this kind of problems, IoT designers not only need tools to assess possible risks and to study countermeasures, but also methodologies to estimate their costs. Here, we present a preliminary methodology, based on the process calculus IoT-LySa, to infer quantitative measures on systems evolution. The derived quantitative evaluation is exploited to establish the cost of the possible security countermeasures
- …
