In today’s world, critical infrastructure is often controlled by computing systems. This introduces new risks for cyber attacks, which can compromise the security and disrupt the functionality of these systems. It is therefore necessary to build such systems with strong guarantees of resiliency against cyber attacks. One way to achieve this level of assurance is using formal verification, which provides proofs of system compliance with desired cyber security properties. The use of Formal Methods (FM) in aspects of cyber security and safety-critical systems are reviewed in this article. We split FM into the three main classes: theorem proving, model checking, and lightweight FM. To allow the different uses of FM to be compared, we define a common set of terms. We further develop categories based on the type of computing system FM are applied in. Solutions in each class and category are presented, discussed, compared, and summarised. We describe historical highlights and developments and present a state-of-the-art review in the area of FM in cyber security. This review is presented from the point of view of FM practitioners and researchers, commenting on the trends in each of the classes and categories. This is achieved by considering all types of FM, several types of security and safety-critical systems, and by structuring the taxonomy accordingly. The article hence provides a comprehensive overview of FM and techniques available to system designers of security-critical systems, simplifying the process of choosing the right tool for the task. The article concludes by summarising the discussion of the review, focusing on best practices, challenges, general future trends, and directions of research within this field.

This paper demonstrates a step on the transition towards a digital twin for a desktop version of an agricultural robot. This includes implementation of motor control and in-door localisation capabilities for the robot. Data from the physical twin is streamed to a co-simulation based on the Functional-Mockup Interface, in which a digital twin simulates the robot’s movement. Safety constraints are established inside the digital twin and a proof of concept communication is enabled when such constraints are violated.

Digital innovation hubs (DIHs) are a strategic means to drive European Small and Medium Enterprises (SMEs) digital transition. The European Commission has envisioned four main functions characterizing DIHs' service portfolios (“Test before invest”; “Support to find investments”; “Innovation ecosystem and networking”; and “Skills and training”). However, DIHs target different functions, e.g. focusing on helping launch novel digital technologies to market, or directing investment opportunities. DIHs are also at different maturity levels, interact with different actors and exist in regions with different conditions for innovation. There might not be an equal need for all four functions, and they might not be equally well served. This study aims to explore and derive implications for the deployment of the four main functions by DIHs. It builds on the activities of DIHs involved in the DIH initiative through several innovation actions, including FED4SAE and HUBCAP.

A digital twin for a Cyber-Physical System includes a simulation model that predicts how a physical system should behave. We show how to quantify and characterise violation events for a given safety property for the physical system. The analysis uses the digital twin to inform a runtime monitor that checks whether the noise and violations observed fall within expected statistical distributions. The results allow engineers to determine the best system configuration through what-if analysis. We illustrate our approach with a case study of an agricultural vehicle.

Businesses, particularly small and medium-sized enterprises, aiming to start up in Model-Based Design (MBD) face difficult choices from a wide range of methods, notations and tools before making the significant investments in planning, procurement and training necessary to deploy new approaches successfully. In the development of Cyber-Physical Systems (CPSs) this is exacerbated by the diversity of formalisms covering computation, physical and human processes. In this paper, we propose the use of a cloud-enabled and open collaboration platform that allows businesses to offer models, tools and other assets, and permits others to access these on a pay-per-use basis as a means of lowering barriers to the adoption of MBD technology, and to promote experimentation in a sandbox environment.

Architecture space exploration of multicore systems has been studied for more than a decade now. The main exploration factor was the workload distribution in a sense that all processing elements run fairly similar workloads, and none of the processes misses its real-time constraints. For safety critical systems, assigning the software functions to real-time tasks of the target operating system is a crucial task as it is constrained with a set of different criticality, architectural and time-related constraints. Finding a suitable architecture configuration involves many important design decisions that have a strong impact on the system safety and performance. With the increasing complexity and scale of today's systems and the large number of possible architecture configurations, identifying the efficient architectures while satisfying different (potentially conflicting) criteria becomes tedious and error-prone for designers. In this paper, we propose an automated method using multi-objective criteria to explore the architecture of multicore safety critical systems. Our method relies on a constellation of analysis techniques where we consider architectural, criticality and time requirements (schedulability). We have implemented two Matlab algorithms to perform the architecture exploration, while the final candidate configurations are analyzed for schedulability using the Uppaal model checker.

Abstract Inspired by the relational algebra of data processing, this paper addresses the foundations of data analytical processing from a linear algebra perspective. The paper investigates, in particular, how aggregation operations such as cross tabulations and data cubes essential to quantitative analysis of data can be expressed solely in terms of matrix multiplication, transposition and the Khatri–Rao variant of the Kronecker product. The approach offers a basis for deriving an algebraic theory of data consolidation, handling the quantitative as well as qualitative sides of data science in a natural, elegant and typed way. It also shows potential for parallel analytical processing, as the parallelization theory of such matrix operations is well acknowledged.