ABSTRACT. Industry 4.0, the new wave of Smart Manufacturing in Europe and globally, relies on a Digital Thread to connect the data and processes for smarter products, smarter production, and smarter integrated ecosystems. But what is the Digital Thread? The talk will discuss a few key questions about modelling, the nature of models and the use of models that arose from the experience in the first two years of Confirm, the Irish Centre for Smart Manufacturing. It will also provide a few examples of how the new model-powered and integrated thinking can disrupt the status quo, empower a better understanding, and deliver a more automatic management of the many cross-dimensional issues that future connected software and systems will depend upon.

Tiziana Margaria is Chair of Software Systems and Head the Dept. of Computer Science and Information Systems at the University of Limerick (Ireland). She is also a Principal Investigator of Lero, The Irish Software Research Center, where she heads the Committee on International Relations Development, and is the Principal Investigator of Confirm, the new SFI Research Centre on Smart Manufacturing. In Lero, she leads research projects on Scientific Workflow and model-driven HW/SW Cybersecurity. In Confirm, she is co-leading the Hub on Cyberphysical Systems, and uses her expertise in advanced model driven, generative, and service-oriented design in the industrial automation context. She has broad experience in the use of formal methods for high assurance systems, in particular concerning functional verification, reliability, and compliance of complex heterogeneous systems. She is (co-)author of over 200 refereed papers in international journals and conferences, and she has served on more than 100 Program Committees, over 20 times as chair. She is the creator and General Chair of ISoLA (since 2004), co-founder of STTT (Springer, 1997), and most recently Founding editor of the Transactions on Foundations for Mastering Change (Springer, 2016). She is Fellow of the Irish Computer Society and Fellow of SDPS. She is currently Vice-president of EASST, and current Chair of FMICS. In EuSEM she is Member of the Research Committee SIG-TPCEC. She holds 2 USPTO patents, one of which with NASA.

ABSTRACT. Distributed systems are challenging to design properly and prove correctly due to their heterogeneous and distributed nature. These challenges depend on the programming paradigms used and their semantics. The actor paradigm has the advantage of offering a modular semantics, which is useful for compositional design and analysis. Shared variable concurrency and race conditions are avoided by means of asynchronous message passing. The object-oriented paradigm is popular due to its facilities for program structuring and reuse of code. These paradigms have been combined by means of concurrent objects where remote method calls are transmitted by message passing and where low-level synchronization primitives are avoided. Such kinds of objects may exhibit active behavior and are often called active objects. In this setting the concept of futures is central and is used by a number of languages. Futures offer a flexible way of communicating and sharing computation results. However, futures come with a cost, for instance with respect to the underlying implementation support, including garbage collection. In particular this raises a problem for IoT systems.

The purpose of this paper is to reconsider and discuss the future mechanism and compare this mechanism to other alternatives, evaluating factors such as expressiveness, efficiency, as well as syntactic and semantic complexity including ease of reasoning. We limit the discussion to the setting of imperative, active objects and explore the various mechanisms and their weaknesses and advantages. A surprising result (at least to the authors) is that the need of futures in this setting seems to be overrated.

ABSTRACT. Distributed systems are notoriously difficult to develop correctly, due to the concurrency in their communicating subsystems. Several techniques are available to help developers to improve the reliability of message passing software, including deductive verification and model checking. Both these techniques have advantages as well as limitations, which are complementary in nature. This paper contributes a novel verification technique that combines the strengths of deductive and algorithmic verification to reason elegantly about message passing concurrent programs, thereby reducing their limitations. Our approach allows to verify data-centric properties of message passing programs using concurrent separation logic (CSL), and allows to specify their communication behaviour as a process-algebraic model. The key novelty of the approach is that it formally bridges the typical abstraction gap between programs and their models, by extending CSL with logical primitives for proving deductively that a program refines its process-algebraic model. These models can then be analysed via model checking, using mCRL2, to reason indirectly about the program's communication behaviour. Our verification approach is compositional, comes with a mechanised correctness proof in Coq, and is implemented as an encoding in Viper.

ABSTRACT. We present MADA, a deployment approach to facilitate the design of efficient and safe distributed software commissioning. MADA is built on top of the Madeus formal model that focuses on the efficient execution of installation procedures. Madeus puts forward more parallelism than other commissioning models, which implies a greater complexity and a greater propensity for errors. MADA provides a new specific language on top of Madeus that allows the developer to easily define the properties that should be ensured during the commissioning process. Then, MADA automatically translates the description to a time Petri net and a set of TCTL formulae. MADA is evaluated on the OpenStack commissioning.

ABSTRACT. Input/Output Automata (IOA) is an expressive and popular specification framework with built-in properties for compositional reasoning. It has been shown to be effective in specifying and analyzing distributed and networked systems. The available verification engines for IOA are all based on interactive theorem provers such as Isabelle, Larch, PVS, and Coq, and are expressive but require heavy human interaction. Motivated by the advances in SMT solvers, in this work we explore a different expressivity-automation tradeoff for IOA. We present Dione, the first IOA analysis system built with Dafny and its SMT-powered toolchain and demonstrate its effectiveness on four distributed applications. Our translator tool converts Python-esque Dione language specification of IOA and their properties to parameterized Dafny modules (similar to theories in theorem provers). Dione automatically generates the relevant compatibility and composition lemmas for the IOA specifications, which can then be checked with Dafny on a per module-basis. We ensure that all resulting formulas are expressed mostly in fragments solvable by SMT solvers and hence enables Bounded Model Checking and k-induction-based invariant checking using Z3. We present successful applications of Dione in verification of an asynchronous leader election algorithm, two self-stabilizing mutual exclusion algorithms, and CAN bus Arbitration: we automatically prove key invariants of all four protocols; for the last three this involves reasoning about arbitrary number of participants. These analyses are largely automatic with minimal manual inputs needed, and they demonstrate the effectiveness of this approach in analyzing networked and distributed systems.

ABSTRACT. The prevalence of the JavaScript programming language makes the correctness and security of its execution environments highly important. The most exposed and vulnerable parts of these environments are the APIs published to the executed untrusted JavaScript programs. This paper revisits the fuzzing technique that generates JavaScript environment API calls using random walks on so-called prototype graphs to uncover potentially security-related failures. We show the limits of generating independent call expressions, the approach of prior work, and give an extension to enable the generation of interdependent API calls that re-use each other's results. We demonstrate with an experiment that this enhancement allows to exercise JavaScript environment APIs in ways that were not possible with the previous approach, and that it can also trigger more issues in a real target.

ABSTRACT. This paper presents a technique to measure and visualize execution path coverage of test cases in the context of model-based software systems testing. Our technique provides visual feedback of the tests, their coverage, and their diversity. We provide two types of visualizations for path coverage based on so-called state-based graphs and path-based graphs. Our approach is implemented by extending the Modbat tool for model-based testing and experimentally evaluated on a collection of examples, including the ZooKeeper distributed coordination service. Our experimental results show that the state-based visualization is good at relating the tests to the model structure, while the path-based visualization shows distinct paths well, in particular linearly independent paths. Furthermore, our graph abstractions retain the characteristics of distinct execution paths, while removing some complexity of the graph.

ABSTRACT. GALS (Globally Asynchronous Locally Synchronous) systems, such as the Internet of Things or autonomous cars, integrate reactive synchronous components that interact asynchronously. The complexity induced by combining synchronous and asynchronous aspects makes GALS systems difficult to develop and debug. Ensuring their functional correctness and reliability requires rigorous design methodologies, based on formal methods and assisted by validation tools. In this paper we propose a testing methodology for GALS systems integrating: (1) synchronous and asynchronous concurrent models; (2) functional unit testing and behavioral conformance testing; and (3) various formal methods and their tool equipments. We leverage the conformance test generation for asynchronous systems to automatically derive realistic scenarios (input constraints and oracle), which are necessary ingredients for the unit testing of individual synchronous components, and are difficult and error-prone to design manually. We illustrate our approach on a simple, but relevant example inspired by autonomous cars.

ABSTRACT. This paper introduces a model-based testing framework and associated toolkit, so called HYPpOTesT, for uncertain service-based web applications specified as probabilistic systems with non-determinism. The framework connects input/output conformance theory with hypothesis testing in order to assess if the behavior of the application under test corresponds to its probabilistic formal specification. The core component is a (on-the-fly) model-based testing algorithm able to automatically generate, execute and evaluate test cases from a Markov Decision Process specification. The testing activity feeds a Bayesian inference process that quantifies and mitigates the system uncertainty by calibrating probability values in the initial specification. This paper illustrates the structure, features, and usage of HYPpOTesT using the U-Store exemplar, i.e., a web-based e-commerce application that exhibits uncertain behavior.

ABSTRACT. A common problem in the certification of highly safety or security critical systems is the consistency of the certification documentation in general and, in particular, the linking between semi-formal and formal content.

We address this problem by providing a framework, called Isabelle/DOF, that allows writing certification documents with consistency guarantees, in both, the semi-formal and formal parts. Isabelle/DOF supports the modeling of document ontologies using a strongly typed ontology definition language. The ontologies are enforcement inside theory documents and formal parts, e. g., system verification, are checked within Isabelle/HOL. Both the definition of ontologies and the editing of documents referring to an ontology are supported by an IDE that, e.g., provides continuous checking of the document consistency.

In this paper, we present how a specific software-engineering certification standard, namely CENELEC 50128, is modeled inside Isabelle/DOF. Moreover, we present how the Isabelle/DOF approach can be applied to a certification case-study in the railway domain.

ABSTRACT. Assurance cases (ACs) are often required to certify critical systems. Use of integrated formal methods (FMs) in assurance can improve automation, increase confidence, and overcome ambiguity and faulty reasoning. However, ACs can rarely be fully formalised, as the use of FMs is contingent on models validated by informal processes. Consequently, we need assurance techniques that support both formal and informal artifacts, with explicated inferential links between them. In this paper, we contribute a formal machine-checked interactive language for the computer-assisted construction of ACs called Isabelle/SACM. The framework guarantees well-formedness, consistency, and traceability of ACs, and allows a tight integration of formal and informal evidence of various provenance. To validate Isabelle/SACM, we define a novel formalisation of the Tokeneer benchmark, verify its security requirements, and form a mechanised AC that combines the resulting formal evidence with informal artifacts.

ABSTRACT. There are publications that consider the use of program slicing in software verification, but we are aware of no publication that thoroughly evaluates the impact of program slicing on the verification process. This paper aims to fill in this gap by providing a comparison of the effect of program slicing on the performance of the reachability analysis in several state-of-the-art software verification tools, namely CPAchecker, DIVINE, KLEE, SeaHorn, and SMACK. The effect of slicing is evaluated on the number of solved benchmarks and running times of the tools. Experiments show that the effect of program slicing is mostly positive and can significantly improve the performance of some tools.

ABSTRACT. Autonomous robotic systems are complex, hybrid, and often safety-critical; this makes their formal specification and verification uniquely challenging. Though commonly used, testing and simulation alone are insufficient to ensure the correctness of, or provide sufficient evidence for the certification of, autonomous robotics. Formal methods for autonomous robotics has received some attention in the literature, but no resource provides a current overview. This journal-first paper provides an overview of a systematic survey of the state-of-the-art in formal specification and verification for autonomous robotics.

ABSTRACT. Schematic drawings showing railway tracks and equipment are commonly used to visualize railway operations and to communicate system specifications and construction blueprints. Recent advances in on-line collaboration and modeling tools have raised the expectations for quickly making changes to models, resulting in frequent changes to layouts, text, and/or symbols in schematic drawings. Automating the creation of high-quality schematic views from geographical and topological models can help engineers produce and update drawings efficiently.

This paper describes three methods for automatically producing schematic railway drawings with increasing level of quality and control over the result. The final method, implemented in the tool that we present, can use any combination of the following optimization criteria, which have different priorities in different use cases: width and height of the drawing, the diagonal line lengths, and the number of bends. We show how to encode schematic railway drawings as an optimization problem over Boolean and numerical domains, using combinations of unary number encoding, lazy difference constraints, and numerical optimization into an incremental SAT formulation.

We compare resulting drawings from each of the three approaches, applied to models of real-world engineering projects and existing infrastructure. We also show how to add symbols and labels to the track plan, which is important for the usefulness of the final outputs. Since the proposed tool is customizable and efficiently produces high-quality drawings from railML 2.x models, it can be used (as it is or extended) both as an integrated module in an industrial design tool like Railcomple, or by researchers for visualization purposes.

ABSTRACT. Over the last decades, significant progress has been made on formal techniques for software verification. However, despite this progress, these techniques are not yet structurally applied in industry. To reduce the well-known industry--academia gap, industrial case studies are much-needed, to demonstrate that formal methods are now mature enough to help increase the reliability of industrial software. Moreover, case studies also help researchers to get better insight into industrial needs.

This paper contributes such a case study, concerning the formal verification of an industrial, safety-critical traffic tunnel control system that is currently employed in Dutch traffic. We made a formal, process-algebraic model of the informal design of the tunnel system, and analysed it using mCRL2. Additionally, we deductively verified whether the implementation adheres to its intended behaviour, by proving that the code refines our mCRL2 model, using VerCors. By doing so, we detected undesired behaviour: an internal deadlock due to an intricate, unlucky combination of timing and events. Even though the developers were already aware of this, and deliberately provided us with an older version of their code, we demonstrate that formal methods can indeed help to detect undesired behaviours within reasonable time, that would otherwise be hard to find.