VECoS

Abstract : In order to master the increasing complexity of modern railway control systems, novel model-based approaches are needed to allow engineers evaluate such systems against strict system-level dependability requirements. In this talk, driven by railway case-studies, we provide an overview of model-based approaches which have been succesfully adopted to ensure system safety, reliability and security. It is a matter of fact that dependability assurance requires holistic assessment both at the software and at the hardware levels. At the software level, models have proven useful to support both static and dynamic functional analyses in order to discover systematic faults in the code. At the hardware level, compositional multi-formalism modeling approaches well suited the evaluation of system safety and reliability against random faults. The use of models allows engineers to improve both the effectiveness and the efficiency of system verification. Views of the Unified Modeling Language can be adopted to perform informal or semi-formal analyses, while Stochastic Petri Nets, (Repairable) Fault Trees, Continuous Time Markov Chains and Bayesian Networks can be employed to perform formal and quantitative analyses. Furthermore, analytical risk and vulnerability models have also been experimented for security assessment with respect to intentional threats and natural hazards. Due to the wide range of possible applications, a promising research trend is devoted to the study of the challenging theoretical and technological issues related to the multi-paradigm dependability modeling using appropriate frameworks.

Abstract : One of the concerns in the use of computer systems is to avoid the leakage of secret information through public outputs. Ideally we would like systems to be completely secure, but in practice this goal is often impossible to achieve. Therefore it is important to have a way to assess the amount of leakage. In this talk, we illustrate various quantitative approaches to measure the leakage, in relation to the model of adversary. We also make a connection with the recent notion of "differential privacy" which is another way to quantify information leakage, developed independently in the area of statistical databases.

Abstract : Since their introduction in the 50's, Markov Decision Process (MDP) models have gained recognition in several fields including computer science and telecommunications. They provide a simple mathematical model in order to express optimization problems in random environments and a rich theory leading to efficient algorithms for many practical problems. Being a low level formalism, it is rather hard to directly use MDPs to model complex systems. Some high level MDP specification formalisms have been proposed in the literature to overcome this problem (e.g. Stochastic Transition Systems, Dynamic Decision Networks, Reactive Modules ,.); in this talk Markov Decision Petri Net (MDPN) and Markov Decision Well-formed Net (MDWN) formalisms will be presented, two high level formalisms that allow to describe the system in terms of its components and their interactions. As a consequence, the models are more compact and manageable. MDWN formalism inherits the efficient algorithms originally devised for Well-Formed Nets, allowing to automatically take advantage of the model symmetries to reduce the analysis complexity. MDPN/MDWNs have several possible applications, that will be illustrated in the talk. The solution of MDPN and MDWN models is supported by MDWNsolver: a framework integrated within the GreatSPN tool suite. MDPN has also been proposed as a target formalisms for the translation of Non deterministic Repairable Fault Trees (NdRFT), an extension of Fault-trees allowing to model faults of complex systems as well as their repair processes. The originality of this formalism w.r.t. other Fault Tree extensions is that it enables to face repair strategy optimization problems: in an NdRFT model, the decision on whether to start or not a given repair action is non deterministic, so that all the possibilities are left open. The optimal repair strategy w.r.t. some relevant system state function, e.g. the system unavailability, can then be computed by solving an optimization problem on a Markov Decision Process. A translator from NdRFT to MDPN models has been implemented and integrated within the DrawNet multi-formalism framework and linked with MDWNsolver, thus providing a NdRFT design and analysis tool. To conclude, an outlook on possible extensions of the work: on one hand many practical problems would require to model the fact that the state is only partially observable, hence suggesting to extend the approach towards Partially Observable MDP, on the other hand the complexity of the solution calls for increased efficiency, possibly obtained by accepting approximate solutions.