News Releases

Release of highly reliable and efficient software development technology for social infrastructure

- 80% reduction in development time of "formal methods" suitable for ensuring safety and security -

Tokyo, February 12, 2013 - Hitachi, Ltd. (TSE:6501, "Hitachi") today announced the co-development of a technology to verify software specifications in highly efficient software development of reliable large-scale software in social infrastructure systems, together with the Swiss Federal Institute of Technology Zurich ("ETH") and Hitachi India Pvt. Ltd. ("Hitachi India"). The technology developed employs formal methods that are techniques suited to the development of high quality software regarding reliability and security. It was verified that if a model is developed and its quality is verified, by re-using this model in the development of other systems, the development time to generate and verify new models can be reduced by approximately 80%. Hitachi will release the supporting tool as open source software from today to promote its use and improvement in real applications.

In social infrastructure such as energy supply, public systems and railways, it is essential to efficiently develop software that is able to address the complexity and scale of the system while maintaining a high level of reliability. In recent years, formal methods have received attention as techniques for the development of such high quality software requiring safety and security, and its use is recommended in international standards. Formal methods differ from previous techniques, which check the quality after the software is developed, in that it systematically confirms the accuracy of design descriptions during software development. Thus, software development time is greatly influenced by how efficiently this confirmation process is conducted. The software technology developed re-employs models created with formal methods, and by doing so, significantly reduces the confirmation process thus shortening development time.

Features of the software technology developed are as described below.

(1)Developed as an enhanced function of formal modeling method Event-B based on the theorem proving approach

The development is based on Event-B,*1 a widely accepted method using the theorem proving*2 approach to prove that the design description meets the requirements, and features the ability to efficiently verify the quality of even large-scale systems.

(2)Realized the re-use of templated verified formal models

Once a model has its quality verified, it can be re-used in the development of similar systems. As a result, a benefit of reducing development time by 80% was found by using software that has been verified with this technology, compared to developing a model from the beginning and verifying its design description.*3

In order to improve this software technology for practical applications, Hitachi will release the supporting tool as open source software from February 12. Hitachi will continue to promote research and development of technologies applying formal methods for the efficient development of highly reliable systems for social infrastructure.

Open source website

• http://sourceforge.net/projects/gen-inst/

Technical terms

*1

Event-B: A formal modeling method developed by ETH and others under an EU project, based on the theorem proving approach. The method is suited to modeling in the upstream stage of system development, and its application has been reported in the development of railway systems, automotive systems, and enterprise information systems.

*2

Theorem proving approach: A widely accepted verification method to prove formal models, this approach verifies that the design description meets requirements mathematically, such as by first-order predicate logic, using computing. Although part of the verification process must be conducted manually, it can be applied to the verification of large-scale systems without being restricted by computer resource.

*3

Based on Hitachi estimate. In an internal feasibility study for this project, an instantiated formal model was generated based on an already proven generic model. In the generated model, it was found that approximately 80% of the items that require verification could be re-used.

Details of the Formal Verification Support Software

The Formal Verification Support Software adapts the re-use technology in the Generic Instantiation Model. Generic instantiation is a technique to generate a desired formal model from a template called the generic model that consists of some abstract symbols. A desired model is generated by replacing these abstract symbols in the generic model with other, more concrete values specified by the user. The generated model is called an instantiated model to distinguish it from the generic model. The Formal Verification Support Software developed has the function of generating the desired instantiated model from the generic model described above together with the relationship between abstract symbols and its concrete values. Thus re-using the generic model as a template has the benefit of significantly reducing the volume of model description.
Further, by proving the validity of the generic model beforehand, generic instantiation allows to omit a large portion of the verification of the instantiated one. In order to skip the redundant verification steps, however, it is necessary that the concrete values replacing the abstract symbols meet some specified syntactic constraints. The Formal Verification Support Software developed includes a function to check that these syntactic constraints are met and only then generates an instantiated model.

About Hitachi, Ltd.

Hitachi, Ltd. (TSE: 6501), headquartered in Tokyo, Japan, is a leading global electronics company with approximately 320,000 employees worldwide. Fiscal 2011 (ended March 31, 2012) consolidated revenues totalled 9,665 billion yen. Hitachi is focusing more than ever on the Social Innovation Business, which includes information and telecommunication systems, power systems, industrial, transportation and urban development systems, as well as the sophisticated materials and key devices that support them. For more information on Hitachi, please visit the company's website at http://www.hitachi.com.