The construction of software for an application is a complicated process. We employ Software Engineers to develop software in a way that helps us arrive at robust solutions, and it is the training and experience of such engineers that we rely on.
One of the many effects of the adoption of Internet of Things technologies is the realisation that the inter-connected-ness of physical objects with other objects, and human beings, is creating systems that are inherently complex.
If we consider the scenario where a machine-tool is controlled by a microprocessor, usually referred to as an embedded system, the range of outcomes that the system must govern, whilst numerous, is conceivable to the software engineer and can be accounted for in the resultant program code for that application.
If, however, we consider a situation where collections of machine tools, all of different types, are networked such that they can exchange information for the purposes of enhanced control, optimising resources and reducing wastage, the complexity of such a system is more challenging to fathom. If we then augment such a system with inputs from the functions from within a manufacturing supply chain, the scope of complexity becomes increasingly more difficult to fathom.
The combination of localised sensing, data processing and analytics, data exchange, data fusion and aggregation, data storage and visualisation is what constitutes a system (perhaps a Cyber Physical System) that can offer considerable benefits for an organisation that seeks competitive advantage. But how do our software engineers deal with such a challenge?
There has been a tradition of developing the craft of software engineering, whereby the use of methods and frameworks, when combined with real-world experience of software creation, has culminated in the development of the skills and knowledge that we recognise as befitting the role of a “software engineer”.
A significant proportion of the software engineering role is the ability to deal with complexity in system design, but also to handle the effects of complexity after a system has been implemented, through updates that might be required as a result of new requirements, unforeseen requirements, and system design deficiencies, otherwise known as “bugs”.
As we start to comprehend the potential impact of the IoT era, there is an emerging awareness of the need to be able to design and test – more exhaustively – software before it is deployed.
The development of formal approaches to software development is something that has been an active research topic in academic arenas for many years, with its industrial application being generally limited to “safety-critical” systems such as nuclear power plants, aircraft control systems, etc.
But we are now in the midst of a period where CPS are increasingly accessible and as a consequence they are being introduced into application areas by individuals who a) are ignorant of formal approaches to software development and b) are not software engineers and are therefore lacking even the “craft” of software engineering.
What do we mean by formal methods?
Formal methods are an approach where the ability to analyse software design is an inherent part of the design process. This facilitates not only the construction of models that replicate the system to be developed (and thus use abstraction to manage the complexity), but it means that a system model can be tested and evaluated before a line of code is even written.
The use of mathematical notation means that the specification of a system can be expressed precisely, but that it can also be formally reasoned against to test for inconsistencies.
This formality offers considerable advantages for software development such as:
- software specifications are more explicit and rigorous. This supports the goal of requirements engineering to ensure that the proposed system delivers what is needed;
- program code is more rigorous as there is a formal underpinning for each aspect of the software that is being developed. The software engineer knows that functions within the model have been tested against the specification and as such has already verified that the program functionality is correct. There is the additional benefit that the formal declaration of requirements, together with logical reasoning, means that some degree of testing can actually be automated;
- system maintenance and future modification will be simpler, partly because such a system has been more thoroughly designed, but also because the underlying documentation is explicit and includes the reasoning for the inclusion of a all functionality.
The above are compelling arguments for a return to the thinking around formal methods, and how these can help us develop the next generation of IoT-inspired systems.