PAPM-PROBMIV on Friday

Detailed program
Friday July 26th, 2002
See also the unified by-slot program


All sessions take place in auditorium 3.

Session 5: Invited talk

08:50-09:50  David Sands, Chalmers U of Techn., Sweden
Invited talk: Probability and timing: Challenges for secure programming
In this talk we will provide an overview of our recent work on the specification and verification of secure information flow in such programs. We highlight how probabilistic considerations enter in two quite different ways. In the first instance, probabilities are an additional security threat. Concurrent systems might exhibit probabilistic behaviour which an attacker could exploit to leak information. In this case we look at the modelling and verification of secure information flow using probabilistic bisimulations. In the second case, we look at how probabilistic behaviour can come to our aide when trying to eliminate the information flows which arise through the timing behaviour of programs. This talk is based on joint work with Andrei Sabelfeld and Johan Agat.

Session 6: Security

09:50-10:30  Alessandro Aldini, U Bologna, Italy
Roberto Gorrieri, U Bologna, Italy
Security analysis of a probabilistic non-repudiation protocol
Non-interference is a definition of security introduced for the analysis of confidential information flow in computer systems. In this paper, a probabilistic notion of non-interference is used to reveal information leakage which derives from the probabilistic behavior of systems. In particular, as a case study, we model and analyze a non-repudiation protocol which employs a probabilistic algorithm to achieve a fairness property. The analysis, conducted by resorting to a definition of probabilistic non-interference in the context of process algebras, confirms that a solely nondeterministic approach to the information flow theory is not enough to study the security guarantees of cryptographic protocols.

Session 7: Model checking

11:00-11:40  Michael Huth, Imperial College, UK
Possibilistic and probabilistic abstraction-based model checking
We present a framework for the specification of abstract models whose verification results transfer to the abstracted models for a logic with unrestricted use of negation and quantification. This framework is novel in that its models have quantitative or probabilistic observables and state transitions. Properties of a quantitative temporal logic have measurable denotations in these models. For probabilistic models such denotations approximate the probabilistic semantics of full LTL. We show how predicate-based abstractions specify abstract quantitative and probabilistic models with finite state space.

11:40-12:20  Marta Kwiatkowska, U Birmingham, UK
Gethin Norman, U Birmingham, UK
Antonio Pacheco, IST Lisbon, Portugal
Model checking CSL until formulae with random time bounds
Continuous Time Markov Chains (CTMCs) are widely used as the underlying stochastic process in performance and dependability analysis. Model checking of CTMCs against Continuous Stochastic Logic (CSL) has been investigated previously by a number of authors. CSL contains a time-bounded until operator that allows one to express properties such as "the probability of 3 servers becoming faulty within 7.01 seconds is at most 0.1". In this paper we extend CSL with a random time-bounded until operator, where the time bound is given by a random variable instead of a fixed real-valued time (or interval). With the help of such an operator we can state that the probability of reaching a set of goal states within some generally distributed delay while passing only through states that satisfy a certain property is at most (at least) some probability threshold. In addition, certain transient properties of systems which contain general distributions can be expressed with the extended logic. We extend the efficient model checking of CTMCs against the logic CSL developed in [Katoen et al. 2001] to cater for the new operator. Our method involves precomputing a family of coefficients for a range of random variables which includes Pareto, uniform and gamma distributions, but otherwise carries the same computational cost as that for ordinary time-bounded until. We implement the algorithms in Matlab and evaluate them by means of a queueing system example.

Session 8: Short presentations

14:00-14:20  Richard Lassaigne, U Paris VII, France
Sylvain Peyronnet, U Paris XI (Paris-Sud), France
Short presentation: Approximate verification of probabilistic systems

14:20-14:40  Olivier Bournez, LORIA Nancy, France
Short presentation: A generalization of equational proof theory?

14:40-15:00  Alessandra Di Pierro, U Pisa, Italy
Herbert Wiklicky, Imperial College, UK
Short presentation: Probabilistic abstract interpretation and statistical testing

15:00-15:20  Mario Bravetti, U Bologna, Italy
Short presentation: An integrated approach for the specification and analysis of stochastic real-time systems

Session 9: Refinement strategies

16:00-16:40  Pedro D'Argenio, National U of Córdoba, Argentina
Bertrand Jeannet, IRISA Rennes, France
Henrik Jensen, Aalborg U, Denmark
Kim Guldstrand Larsen, Aalborg U, Denmark
Reduction and refinement strategies for probabilistic analysis
We report on new strategies for model checking quantitative reachability properties of Markov decision processes by successive refinements. In our approach, properties are analyzed on abstractions rather than directly on the given model. Such abstractions are expected to be significantly smaller than the original model, and may safely refute or accept the required property. Otherwise, the abstraction is refined and the process repeated. As the numerical analysis involved in settling the validity of the property is more costly than the refinement process, the method profits from applying such numerical analysis on smaller state spaces. The method is significantly enhanced by a number of novel strategies: a strategy for reducing the size of the numerical problems to be analyzed by identification of so-called essential states, and heuristic strategies for guiding the refinement process.

16:40-16:50  Closing and Farewell