A10

アーキテクチャ・ソフトウェア/うごかすちから

Architecture, Software

ソフトウェアの要件の「ぼかし方」に関する研究

Research on refinement-based formal specifications

適切な「ぼかし」で、ソフトウェアの複雑さに挑む

Dealing with complexity of software with abstraction

代表者名

小林 努

Tsutomu Kobayashi

共同発表者名

ERATO蓮尾メタ数理システムデザインプロジェクト, Agustin Eloy Martinez Sune, 石川 冬樹, 蓮尾 一郎

ERATO Hasuo Metamathematics Systems Design Project, Agustin Eloy Martinez Sune, Fuyuki Ishikawa, Ichiro Hasuo

所属分野

アーキテクチャ科学研究系

Information Systems Architecture Science Research Division

pdf-image

要旨

ソフトウェアシステムの信頼性を保証するためには,求められる要件を明確化し,それらが満たされることを確認する必要があります.
特に近年複雑化するソフトウェアでは信頼性が重要である一方,検証が難しくもあります.
我々は,全体の正しさを保ったまま適切な「ぼかし」方をして要件を解きほぐしつつソフトウェアの性質について厳密に議論するアプローチについて研究しています.
本発表では,ぼかし方に対してリファクタリングや解析などの工学的アプローチを適用する研究や,ぼかしを上手に用いて自動運転のソフトウェアを検証する試みについて説明します.

In order to ensure the dependability of software systems, it is essential to clarify the requirements and verify they are satisfied.
Recent complex systems, especially, requires careful consideration of requirements but makes verification more difficult to handle.
We tackle this problem based on an approach called `stepwise refinement’, namely starting from verifying abstract requirements and gradually making them complex and realistic.
This presentation introduces our studies on the refactoring and analysis on refinement-based formal specifications.
We also present applications of such techniques to advanced systems such as software for autonomous vehicles.

関連動画