Alexander Romanovsky

Alexei Iliasov, Dominic Taylor, Linas Laibinis et al.

The increasing complexity of modern interlocking poses a major challenge to ensuring railway safety. This calls for application of formal methods forassurance and verification of their safety. We have developed an industry-strength toolset, called SafeCap, for formal verification of interlockings. Our aim was to overcome the main barriers in deploying formal methods in industry. The approach proposed verifies interlocking data developed by signalling engineers in the ways they are designed by industry. It ensures fully-automated verification of safety properties using the state of the art techniques (automated theorem provers and solvers), and provides diagnostics in terms of the notations used by engineers. In the last two years SafeCap has been successfully used to verify 26 real-world mainline interlockings, developed by different suppliers and design offices. SafeCap is currently used in an advisory capacity, supplementing manual checking and testing processes by providing an additional level of verification and enabling earlier identification of errors. We are now developing a safety case to support its use as an alternative to some of these activities.

Flavio Primo, Paolo Missier, Alexander Romanovsky et al.

On social media platforms and Twitter in particular, specific classes of users such as influencers have been given satisfactory operational definitions in terms of network and content metrics. Others, for instance online activists, are not less important but their characterisation still requires experimenting. We make the hypothesis that such interesting users can be found within temporally and spatially localised contexts, i.e., small but topical fragments of the network containing interactions about social events or campaigns with a significant footprint on Twitter. To explore this hypothesis, we have designed a continuous user profile discovery pipeline that produces an ever-growing dataset of user profiles by harvesting and analysing contexts from the Twitter stream. The profiles dataset includes key network and content-based users metrics, enabling experimentation with user-defined score functions that characterise specific classes of online users. The paper describes the design and implementation of the pipeline and its empirical evaluation on a case study consisting of healthcare-related campaigns in the UK, showing how it supports the operational definitions of online activism, by comparing three experimental ranking functions. The code is publicly available.

Paolo Missier, Callum McClean, Jonathan Carlton et al.

Tropical diseases like \textit{Chikungunya} and \textit{Zika} have come to prominence in recent years as the cause of serious, long-lasting, population-wide health problems. In large countries like Brasil, traditional disease prevention programs led by health authorities have not been particularly effective. We explore the hypothesis that monitoring and analysis of social media content streams may effectively complement such efforts. Specifically, we aim to identify selected members of the public who are likely to be sensitive to virus combat initiatives that are organised in local communities. Focusing on Twitter and on the topic of Zika, our approach involves (i) training a classifier to select topic-relevant tweets from the Twitter feed, and (ii) discovering the top users who are actively posting relevant content about the topic. We may then recommend these users as the prime candidates for direct engagement within their community. In this short paper we describe our analytical approach and prototype architecture, discuss the challenges of dealing with noisy and sparse signal, and present encouraging preliminary results.

Paulius Stankaitis, Alexei Iliasov, David Adjepon-Yamoah et al.

Event-B is one of more popular notations for model-based, proof driven specification. It offers a fairly high-level mathematical lan- guage based on FOL and ZF set theory and an economical yet expres- sive modelling notation. Model correctness is established by discharging proving a number conjectures constructed via a syntactic instantiation of schematic conditions. A large proportion of provable conjectures re- quires proof hints from a user. For larger models this becomes extremely onerous as identical or similar proofs have to be repeated over and over, especially after model refactoring stages. In the paper we briefly present a new Rodin Platform proof back-end based on the Why3 umbrella prover.

Alexander Romanovsky, Marc-Olivier Killijian

The 21st century society relies on computing systems more than ever. Computers are no longer simply machines that are used by organizations or at home. They are embedded everywhere, from cell phones to cars or industrial control devices, and large-scale cloud computing providers are sharing them among many organizations in an unprecedented scale. As computers have become indispensable, their failures may significantly perturb our daily lives. The increased hardware and software complexity, as well as the scaling of manufacturing technologies towards nanometer size devices, pose new challenges to the developers. As a consequence the development, testing, and benchmarking of dependable systems has become a vital topic of research, both for academia and industry. EDCC is the leading European conference for presenting and discussing the latest research in dependable computing. As in previous years, its tenth edition aims at providing a European-hosted venue for researchers and practitioners from all over the world to present and discuss their latest research results on dependability, security, fault-tolerance, and testing. Original papers are solicited on theory, techniques, systems, and tools for the design, validation, operation and evaluation of dependable and secure computing systems, covering any fault model, from traditional hardware and software faults to accidental and malicious human interactions.