Need for formal methods in software design

Formal methods: There is a wide range of architectural styles that range from informal approaches such as “boxes and lines” to formal ones that use mathematical logic. Between the two extremes, the Unified Modeling Language (UML) is widely used in industry with its multiple views, for example activity and sequence diagrams. The formal approach to software design rose to prominence after some well-known critical industrial failures such as (i) Ariane-5, (ii) Pentium FDIV bug, (iii) Denver baggage system failure, ( iv) THERAC-25 radiation therapeutic catastrophe, etc. The fact that natural language has too much ambiguity to express specifications and constraints has led to low adoption of trends such as precise UML or model-driven architectures (MDA).

Requirements are usually stated in natural language and implementation is done using programming languages. The main design challenge was to bridge the gap between specification and implementation for traceability and assurance. The need was for an accurate language that could be subject to automated analysis so that the expected runtime behavior of the implementation would conform to the specification. Mathematical logic and new efficient state-space search algorithms have led to the development of techniques and tools that have come to the rescue where such guarantees are required. The techniques range from fully automated property checking (known as “model checking”) to using a kind of mathematical logic known as temporal logic that goes beyond traditional predicate logic (that’s i.e. “and”, “or”, “for all”, etc.) with new logical operators such as “eventually”, “always” for human-assisted or automated theorem provers.

Use of tools: A wide range of tools have been developed to support the formal specification and verification of software. The biggest challenge to adopting these tools in commercial application software is the lack of skilled software architects and engineers. In certain areas such as cyber-physical systems, security, device drivers, etc., there is sufficient motivation to apply formal specification and design cycles, thanks to recent titles such as “Spectre” bugs and “Meltdown”. In areas such as security, Europe’s ITSEC recommended the use of strict formal design from its fifth level of security and required the use of formal verification techniques at the seventh level. With the widespread prevalence of cloud-based distributed tools and new software building methodologies, the importance of proper design has become more vital. For some new categories of entrants, for example, real-time machine learning applications, the lack of security could be fatal. Model checkers such as Spin, NuSMV, UPPAL or Alloy have already proven themselves by uncovering critical design flaws. In the commercial sector, Amazon has used TLA+ to verify popular AWS component designs such as S3 and DynamoDB. Theorem provers such as Isabelle/HOL or Coq are used in blockchain designs.

conclusion: Software is part of our daily lives and bugs are not hard to spot, leading to endless frustration among consumers and businesses. The emergence of automated tools for model verification and theorem proofs is one answer to solving this central problem of design verification. The pressure on enterprises to more quickly deploy software with more functionality in an environment of faster hardware, networking and distributed systems demands an urgent need to use formal methods where appropriate. It is imperative that CIOs recognize the critical role of formal architecture and design in mission-critical business software today, given the high cost of failure.


Comments are closed.