Tag Archives: Process Algebras

08/11/2016 – Talk by Filippo Cavallin

Title: Multi-Step Discrete Time Process Algebra (MuPA)
Time: 13:00
Location: Meeting room, Building Zeta
Type: Research Result
Speaker: Filippo Cavallin
We consider Discrete Time Markov Chains with synchronous behaviour, i.e. models in which multiple events may occur at each recorded time in the model. This is based on a conceptual model in which the discrete times are sampling points when the system is observed and at each instant all events that have occurred since the previous observation point will be noted. We propose the first process algebra which is capable of capturing such systems and demonstrate its application to discrete time queues both in isolation and forming networks.

10.01.2013 – Talk by Giovanni Bernardi

Title: Testing preorders for clients and peers

Date: 10/01/2012
Time: 1:00 pm
Location: Sala riunioni
Type: research talk
Speaker: Giovanni Bernardi (Trinity College, Dublin)

The must testing is a formalism that let us reason on the safety of  computations performed by two communicating parties; typically a  client (test) and a server (process). By using the must testing one can define three refinements that state when it is safe to replace servers, clients, or peers.
In this talk we explain the classic semantic characterisation of the must preorder for servers, and then we show how to generalise so as to characterise also the preorders for clients and peers.

12.12.2012 – Tutorial by Stefano Calzavara

Title: An introduction to stochastic process algebras and quantitative security analysis

Date: 12/12/2012
Time: 3:00 pm
Location: Sala riunioni
Type: review of literature
Speaker: Stefano Calzavara (Ca’ Foscari, Venice)

Stochastic process algebras are a popular and convenient specification tool, which have proven successful in many applications from the areas of performance modeling, bioinformatics, and security. However, approaching the world of stochastic process algebras is a nontrivial task, since the very foundations of such models are rather peculiar and the well-known formal machinery of classical (non-deterministic) process algebras does not properly fit them. In this talk we analyze stochastic process algebras from the point of view of the programming languages community, and we try to motivate and understand some apparently weird design choices underlying their development. We then focus on an application of stochastic process algebras to security verification and we propose a personal understanding of the challenges behind such task. We argue that, as the foundations of stochastic process algebras depart from those of classical process algebras, also the approach to their verification may probably benefit from a change of perspective.

Prerequisites: Some notions on process algebras and formal methods may help in appreciating the contents, but the seminar is self-contained.