What is model checking?

As software systems become more complex, and we use rapidly developing technologies to connect systems together to achieve new objectives, the scope for the introduction of errors increases. Such errors may cost an organisation money or they may cause harm.

We can reason as to the range of possible outcomes of a system only up to a certain point; beyond that we are reliant upon the rigour of the design of a device, as well as the information that exists to describe how the system is intended to operate.

As such, verification of systems is an important topic for the emerging Cyber Physical Systems that constitute a lot of the thinking around Industry 4.0 and digital manufacturing. Formal methods are an approach that can both simplify the process of verification during the design stage, as well as enabling the automation of testing, which is useful when a system grows to a size that is beyond what we can comprehend.

The aim of a formal approach to design is to use mathematical techniques and rigour to verify that a system will be specified and operate correctly. Research and industrial practice have led to the development of tools that help manage the verification process, and this includes the automation of the necessary permutations that a system will be required to demonstrate a response to.

Model checking is an approach where every system state is explored and tested in an exhaustive manner. This exploration then presents results that document how a model will operate in relation to its original specification.

The use of abstraction within models allows very large software specifications to be verified, assisting the discovery of inconsistencies between the model and its specification, prior to system realisation and deployment.

Another feature of model checking is that the use of mathematics to specify the model means that any queries upon that model can reveal ambiguous properties or characteristics, which can then be re-specified in much greater detail.

If we consider the adoption of IoT devices in a manufacturing company, there will be a requirement to manage the production of many concurrent data sources. The act of attaching cheap hardware to some manufacturing plant is much easier than it is to craft the software that is required to integrate that component into an existing system.

This leads to the possibility that data sources and data processing may be added to exiting manufacturing systems that cannot fully realise the potential value of the extra data. In fact, the addition of the data may cause confusion and lead to an obfuscation of exiting insight, to the detriment of the business.

Model checking is thus a powerful approach to the design of systems, that protects against the enthusiastic augmentation of software that might actually prevent the desired objective of greater insight from being achieved. Whilst model checking would ideally be applied to all software design from the outset, it can be effectively utilised to verify the design of components, and as such this means that pre-existing systems can be developed further with sub-systems that have been formally tested and shown to be rigorous.