Reasoning Based on Continuous Time. In engineering, dependability attributes are often assessed using continuous- time modelling. In [And10] we proposed an approach to extending Event-B models with event rates and giving the models the semantics of continuous- time Markov chains. We have further investigated the topic by modelling a flash filestore example – one of the examples in the Grand Challenge initiative on Verified Software. Our focus is on the analysis of wear-levelling algorithms using novel probabilistic specification and analysis techniques. The expected lifetime of a flash filestore implementing such an algorithm may be derived using probabilistic proof techniques [AMMM10]3. The work conducted in Task 8.4 has aimed at strengthening the theoret- ical basis for stochastic reasoning in Event-B. Hence it has not been actively used by the deployment partners so far. However, the theory shows signs of maturity. The results of the task will be used within WP2 to assess the probability of hazardous event occurrence, i.e. to assess safety stochastically. Moreover, the work conducted in WP4 might also be augmented by proba- bilistic reasoning while designing protocols. The main technical challenge is to increase usability and scalability of the developing approaches to stochastic and logical reasoning in Event-B. In particular, we are planning to consider architectural-level reasoning, work on finding powerful yet simple proof obligations to support our approaches, 3Following a Deploy workshop at Newcastle involving Xxxxxxx Xxxxxx and Xxxxxxxxx XxXxxx, external funding permitted Xxx Xxxxxxx to visit the University of New South Wales to work on continuous distributions with for a month in late 2009. as well as to conduct large case studies inspired by the tasks of deployment partners.
