Reliable Software System Design and Verification

NII Shonan Meeting:

@ Shonan Village Center, May. 19-20, 2011 SUSPENDED



  • Jin-Song Dong (Associate Professor, National University of Singapore)
  • Jun Sun, Assistant (Professor, Singapore University of Technology & Design)



Information and communication technology are important sectors of the world economy and they are both
rely heavily on software. Unlike many physical systems, software systems will inevitably grow in scale and functionality. Because of this increase in complexity, the likelihood of subtle errors is much greater. Some of these errors may cause loss of money, time, or even human life. Although the trustworthiness of software is increasingly critical, existing tools and methods available for constructing reliable software are unfortunately not well developed. As a consequence, we have witnessed a number of software failures. For examples, in the 80s, a software bug (called a “race condition error”) caused the radiation therapy device Therac-25 to malfunction and deliver lethal radiation doses at several medical facilities, leading to the death of at least five patients and severe injury of many others. In the 90s, the Intel Pentium “floating point error” costs Intel close to $470 million and the flight computer system error led to the Ariane 5 disaster which costs European Space Agency $500 million. In 2010, Toyota recall can cost excess of 2 billion USD and much of the cost, damage to the company’s reputation, and the uncertainty regarding the nature of the problems, could have been avoided if the correctness of the software components have been established beyond doubt.
Many leading computer scientists believe that the most promising approach to developing trusted and reliable software is to follow the example of more mature branches of engineering, by integrating scientific (esp. mathematically-based) methods into the software life cycle. In the past years, various rigorous techniques for developing software have been investigated. These techniques include formal specification, extended type checking, model checking, program analysis/transformation and model driven software construction. Microsoft has recognized the importance of investing in software reliability. Bill Gates made this clear in his talk at the 2002 Windows Hardware Engineering Conference:

Software verification has been the Holy Grail of computer science for many decades, but now in
some key areas, for example, driver verification, we’re building tools that can do actual proof about the software and how it works, in order to guarantee reliability.

Besides Microsoft, IBM also believes in the importance of software reliability, and in 2003, completed its
$2.1 billion cash acquisition of Rational Software ? a family of software products that improves the reliability of software projects. In 2009, Intel reported that Intel i7 CPU is verified using model checking without a single test case. Despite the ferocious investments into improving software trustworthiness by many software houses, software reliability assurance remains a challenging task. Specifically, new verification techniques and scientifically proven methodologies will need to be developed to meet the demand for increasingly complex software and to ensure safe deployment of software systems in every part of society. For the next decade, there remains a huge and global demand for new and improved tools to assist in the design and verification of reliable software.
This NII International Meeting on Reliable Software System Design and Verification is aim to bring together researchers and industry R&D expertise together to exchange their knowledge, discuss their research findings, and explore potential collaborations. Potential invited academics may include various leading researchers from NII, Oxford, NASA, Microsoft Research, Tokyo University, top universities in China and etc. Potential industry invited participants may include leading embedded system company such as Toyota, Sony and other top leading industries in Japan. The timing of this international meeting
is scheduled at 19-20 May 2011 (Check in around late afternoon of 18 May and Checkout around late
afternoon on 20May). Selected original presentation papers is planned to be published by Formal Aspects
of Computing Journal or Innovations in Systems and Software Engineering, A NASA Journal.