Safety inspection of software specifications and automatic synthesis of software.
Information and Communication Technology (Saitama University Research Seed Collection 2025-27 p.85)
Keywords: specifications, verification, software, automatic synthesis, safety
Software that serves as social infrastructure, such as airplane control programs and bank ATMs, is a system that provides services while interacting with users. Such systems are called reactive systems. The design specifications, which serve as blueprints for building and verifying reactive systems, are crucial. By verifying whether the software operates according to the specifications, we ensure the safety of the software. However, if there are deficiencies or inconsistencies in the specifications themselves, the verification becomes pointless. Therefore, research is being conducted to investigate whether there are any errors in the specifications themselves. In particular, when various requirements for different software are included in the specifications, it is possible that the software does not exist. Thus, research is also being conducted to determine whether software that operates according to the specifications exists. As a development of this, research is also being conducted on the automatic synthesis of software from specifications. By automating the synthesis, we can efficiently create safe software.
Inquire About This Product
basic information
Noriaki Yoshiura, Professor Graduate School of Science and Engineering, Department of Mathematical and Electronic Information, Information Area 【Recent Research Topics】 ● Tracking money laundering in cryptocurrency ● Identifying users and web servers in anonymizing networks
Price range
Delivery Time
Applications/Examples of results
【Appeal Points to the Industry】 ● By verifying software specifications, it becomes possible to detect deficiencies and defects in the specifications during the system design phase, thereby improving the efficiency of software development. ● It can make software verification more effective. ● By achieving automatic synthesis of software from specifications, it can reduce the cost of software generation and enable the creation of safer software. 【Examples of Practical Use, Applications, and Utilization】 ● Construction of a system for determining the programmability of specifications ● Construction of an automatic software synthesis system from specifications ● Construction of a system for detecting deficiencies in specifications
Detailed information
-
Specifications in Software Verification
catalog（1）
Download All Catalogs
Company information
The Saitama University Open Innovation Center is a center that functions as a liaison office for industry-academia-government collaboration. It consists of three departments: the Industry-Academia-Government Collaboration Department, the Intellectual Property Department, and the Startup Support Department, each staffed with coordinators well-versed in various fields. The center's activities include solving technical challenges in companies, supporting the implementation of joint research, and conducting technology transfer aimed at introducing and utilizing Saitama University's intellectual property.