A featured contribution from Leadership Perspectives, a curated forum for enterprise technology leaders, nominated by our subscribers and vetted by the CIOApplications Editorial Board.

Lendmark Financial Services

Need For Formal Methods In Software Design

The major goals of enterprise application software in the industry have remained the same since its inception. Enterprise software is supposed to meet its functional specification, remain error-free and must be able to perform and scale as demanded by changing business needs. As is customary in all modern engineering disciplines and practices in the industry, a critical aspect of the successful use of technological tools is the need for proper design before development. This typically happens at multiple levels, from high-level architectures to the lowest levels of code and infrastructure. Modern software technology stacks, whether infrastructure-as-a-service (IaaS), platform-as-a-service (PaaS) or common-off-the-shelf (COTS) application solutions deployed on the cloud via DevOps with push-button agility, are still very much dependent on the appropriate architecture to meet the desired business goals.

Architecture/design: Any software product starts with its specification followed by design, development and testing phases irrespective of development methodologies or tools. Despite great advancements in software technology in recent decades, there appear to be some widespread misconceptions and a lack of appreciation of the importance of architecture and design phases in the Software Development Lifecycle (SDLC). Architecture is fundamentally about choice and options to assemble appropriate components and configure and connect them to achieve the goals of the specification. The complexity management in the evolution toward a digital transformation of enterprise roadmaps, in the backdrop of a reference architecture, mandates some level of concrete design before any development begins, even in iterative and agile methodologies. Elimination of risk is the major reason for high-level architecture followed by more detailed design, due to the cost of fixing bugs late. As Edsger W. Dijkstra said,“ Program testing can be used to show the presence of bugs, but never to show their absence!”; hence, enter formal methods.

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

Requirements are typically stated in some 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 a precise language amenable to automated analysis so that the expected run-time behaviour of the implementation conforms to the specification. Mathematical logic and new efficient state-space search algorithms led to the development of techniques and tools that came to the rescue where such guarantees are demanded. The techniques range from fully automated property checking (known as ‘model checking’) using a kind of mathematical logic known as temporal logic that goes beyond traditional predicate logic (i.e., ‘and’, ‘or’, ‘for all’ etc.) with new logical operators such as ‘eventually’, ‘always’ to human-assisted or automated theorem provers.

Tools usage: A wide range of tools have been developed to support formal specification and verification of software. The biggest challenge to the adoption of these tools in commercial application software is the lack of skilled architects and software engineers. In certain domains such as cyber-physical systems, security, device drivers etc., there is enough motivation to apply formal specification and design cycles, thanks to recent headlines such as ‘Spectre’ and ‘Meltdown’ bugs. In areas such as security, the European ITSEC recommended the use of strict formal design from its fifth security level and required the use of formal verification techniques at the seventh level. With the widescale prevalence of distributed cloud-based tools and new methodologies of software construction, the importance of proper design has become more vital. For some new categories of entrants, e.g., real-time machine learning applications, lack of safety could be fatal. Model checkers such as Spin, NuSMV, UPPAL or Alloy have already proven their worth by uncovering critical design flaws. In the commercial sector, Amazon used TLA+ to verify designs of widely popular AWS components such as S3 and DynamoDB. Theorem provers such as Isabelle/HOL or Coq are being used in blockchain designs.

Conclusions: Software is part of our daily life and it is not hard to spot bugs resulting in endless frustration among consumers and corporations. The emergence of automated model checking and theorem prover tools is a response to address that core design verification issue. The pressure on corporations to deploy software quicker with more features in an environment of faster hardware, network and distributed systems demands a dire need to use formal methods when appropriate. It is imperative for CIOs to recognize the critical role of formal architecture and design in commercial mission-critical software today, given the high cost of failures.

The articles from these contributors are based on their personal expertise and viewpoints, and do not necessarily reflect the opinions of their employers or affiliated organizations.