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.

In modern software development, the practices of continuous integration and DevOps are widely used to increase delivery speed and reduce the time it takes to deploy software changes to production. If formal method tools cannot be efficiently integrated in a DevOps paradigm, then their impact on software development will be reduced. In this paper, we present work addressing this issue through a series of extensions for the Overture tool supporting the Vienna Development Method. These extensions enable Overture to be used in a DevOps setting, through continuous integration and validation of models and generated code via integration with the Jenkins automation server. We frame the integration of formal methods and DevOps in a series of principles, demonstrate the value of this integration through a case study, and reflect on our experiences using formal methods and DevOps in an industrial setting. We hope that this work can help other formal method practitioners integrate their tools with DevOps.

Industrial control systems are moving from monolithic to distributed and cloud-connected architectures, which increases system complexity and vulnerability, thus complicates security analysis. When exhaustive verification accounts for this complexity the state space being sought grows drastically as the system model evolves and more details are considered. Eventually this may lead to state space explosion, which makes exhaustive verification infeasible. To address this, we use VDM-SL's combinatorial testing feature to generate security attacks that are executed against the model to verify whether the system has the desired security properties. We demonstrate our approach using a cloud-connected industrial control system that is responsible for performing safety-critical tasks and handling client requests sent to the control network. Although the approach is not exhaustive it enables verification of mitigation strategies for a large number of attacks and complex systems within reasonable time.

Summary Development of distributed software systems is complex due to the distribution of resources, which complicates validation of system‐wide functionality. Such systems include various facets like functionality and distribution, each of which must be validated and integrated in the final software solution. Model‐based techniques advocate various abstraction approaches to cope with such challenges. To enhance model‐based development, this paper proposes (1) guidelines for development of distributed systems, where the different facets are introduced gradually through systematic modeling extensions, (2) code generation capabilities supporting technology specific realizations, and (3) demonstration of the applicability of our approach using an industrial case study involving the development of a harvest planning system, where the communication infrastructure paradigm changed late in the project. When developing this system, we spent most time validating system‐wide functionality. The model extensions allowed an easier change of the underlying communication paradigm and code generation supported realization of the different system representations.

Modelling and simulation assist in decision support or planning activities by allowing efficient exploration of multiple scenarios in a situation where testing in a real setting is impractical. This exploration is often done by varying numerical parameters in the model such as physical dimensions or speed in order to find the optimal configuration. However, for certain problems, in order to find optimal solutions it is beneficial to vary the algorithms that are used to implement the behaviour of the model. For example, when calculating optimised routes for harvesters and other vehicles in a harvest operation, the choice of optimisation algorithms is an important part of the problem. Traditional modelling and simulation techniques do not allow us to vary algorithms across simulations effectively. In this paper, we address this issue by applying the strategy pattern from software engineering to the construction of a formal model that enables different combinations of harvest optimisation algorithms to be analysed effectively. This approach can be generalised to other planning activities where multiple algorithms need to be considered.

We present and analyse an architectural migration in the Overture tool, a tool for which the primary internal data structure is an Abstract Syntax Tree (AST). The migration was from a high-cohesion AST with functionality encapsulated in its nodes to an extensible, low-cohesion AST with functionality implemented in visitors. This was motivated by the need for a high degree of extensibility in the tool's core functionality. We describe the migration process and both architectures in detail. We also present a comparative analysis between both architectures, including the trade-offs made between extensibility and performance. Finally, we generalise these results to other tool migrations that have hierarchical data structures at their core.

This paper introduces a generic solution for gradually moving from a model of an embedded system to include embedded hardware and software components into the simulation of the model. Our technique enables combined execution (co-execution) of system components models expressed in the VDM-RT formalism with actual hardware/software realizations through the application of Hardware In the Loop (HIL) simulation. Introducing such component realizations in the simulation increases the fidelity of the simulation outcome, thus enabling improved prediction of properties for the system realization.