ソフトウェア・シンポジウム 2024 in 長崎

形式手法による開発において報告された問題のトピックモデルによる分析
井上 蒼士

崔 恩瀞， 西浦 生成， 水野 修

京都工芸繊維大学

京都工芸繊維大学

大学院工芸科学研究科 情報工学専攻

情報工学・人間科学系

s-inoue@se.is.kit.ac.jp{echoi, k-nishiura, o-mizuno}@kit.ac.jp

要旨

手法として形式手法が注目されている [19]．
一方で現在において形式手法は広く普及しているとは

ソフトウェア仕様の品質がソフトウェア品質に寄与す

言えず，その適用は形式検証が不可欠な領域に限定されることが報告されており，自然言語による仕様の曖昧さている．この要因として学習コストの高さや開発時間のが課題として指摘されている．形式手法はこの課題に対増加などの課題が報告されており [12, 18]，これらの課処する手法として注目されているが，形式手法はソフト

題を解消する取り組みが行われている [6, 16]．

ウェア開発に広く普及しているとは言えない．この要因

しかしこれらの課題は形式手法を導入する段階に焦点として学習コストの高さや開発時間の増加などの課題がを当てており，導入した後の開発過程に焦点を当てた課指摘されているが，これらは形式手法の導入の難しさに

題の報告は少ない．そこで本研究ではソフトウェア開発

焦点が当たっており，形式手法の適用によるソフトウェに形式手法を導入した後の開発過程に発生した問題を分

ア開発への影響の報告は少ない．本研究では，GitHub

類することで，形式手法を適用したソフトウェア開発に

リポジトリから収集した問題報告（Issue）を用いて形式特有の傾向を調査した．

手法を適用したソフトウェア開発に特有の傾向を調査し調査には GitHub リポジトリから取得した Issue をデーた．具体的には，トピックモデルである BERTopic を用タセットとして，トピックモデルである BERTopic[4] をいて Issue から特徴的な単語および文書を抽出し，これ手法として，それぞれ用いた．データセットに対してトらを用いて Issue をラベリングすることでソフトウェア

ピックモデルを適用することで Issue から特徴的な単語

開発の傾向を調査した．調査の結果，形式手法を適用しおよび文書を抽出し，抽出された特徴によって Issue にたソフトウェア開発とそうでないソフトウェア開発とのラベルを付与した．このラベルにより Issue を分類し，間で Issue の傾向に有意な差が示された．これらの結果

形式手法を適用したソフトウェア開発に特有の傾向を調は，形式手法を適用したソフトウェア開発に特有の問題

査した．

が存在することを示唆している．

本研究では形式手法を適用したソフトウェア開発に特有の傾向が存在することを仮説とした．またこの仮説の下で，ソフトウェアに対して報告される動作不良，バグ，

1. 緒言

機能の追加や改善，保守の 4 項目に関する報告について
形式手法を適用して開発されたソフトウェアに特有の傾ソフトウェア開発において仕様品質の向上がソフト向が存在すると仮説を立てた．

ウェア品質の向上に寄与することが報告されており [9]，調査の結果，形式手法を適用したソフトウェア開発とソフトウェア仕様が抱える課題として自然言語による記そうでないソフトウェア開発との間で Issue の傾向に有述に起因する曖昧さが指摘されている [8]．形式手法は意な差が認められた．またソフトウェアの動作不良に関システムの仕様を形式的に記述・検証する手法であり，する報告について，形式手法を適用して開発されたソフ

形式的に記述された仕様は特定の性質を容易に検証できトウェアがそうでないソフトウェアより有意に少ないこる．このような性質から，高品質なソフトウェアの開発

122

SEA

ソフトウェア・シンポジウム 2024 in 長崎

2.3. 形式手法の普及とが認められた．一方でソフトウェアの機能追加や改善を求める報告について，形式手法を適用して開発された

2.2 節で述べた利点にもかかわらず形式手法は一般的なソフトウェア開発手法として普及しているとは言えな
い．この要因として学習コストの高さが報告されており[17]，形式手法の学習に関する取り組みが行われている[16, 14, 15]．また開発時間の増加もその要因として報告されている [18] が，これらはいずれも形式手法が持つ複雑さに起因する課題であり，形式手法の適用によるソ
フトウェア開発への影響についての研究は少ない．本研
究では形式手法を適用したソフトウェア開発に特有の傾向を調査することで形式手法の普及に寄与することを目指す．

ソフトウェアとそうでないソフトウェアとの間に有意な差は認められなかった．これらは形式手法の適用がソフ
トウェア開発に特有の影響を与えること，ソフトウェアの動作不良を低減すること，ソフトウェアへの機能の追加や改善の要求に与える影響が小さいことをそれぞれ示
唆するものである．

2. 背景
2.1. ソフトウェア仕様
ソフトウェア開発において仕様品質の向上がソフト
ウェア品質の向上に寄与することが報告されている [9]．

2.4. GitHub Issues

ソフトウェア仕様が抱える課題として自然言語による記

GitHub Issues1（Issue）は GitHub2 リポジトリに提供される機能であり，リポジトリに対して問題を報告するための機能である．これによりソフトウェア開発者は他の開発者および使用者からバグの報告や改善の要求を受け取ることができる．ソフトウェアに報告された問題の分類によってソフトウェア開発を評価した先行研究が存在し [5]，Issue とソフトウェア開発との間に多くの連関が報告されている [1]．本研究では Issue をデータセット
として形式手法を適用したソフトウェア開発に特有の傾向を調査する．

述に起因する曖昧さが指摘されており [8]，自然言語で記述された仕様の曖昧さを低減する手法が提案されている [10, 13]．一方で Yang らの研究 [13] では自然言語で記述された仕様から曖昧さを予測する手法に改善の余地が報告されており，自然言語で記述された仕様から曖昧さを完全に取り除く手法には課題が残されている．そのためソフトウェア仕様から曖昧さを完全に取り除く手法が求められている．

2.2. 形式手法

2.5. BERTopic

形式手法はシステムの仕様を形式的に記述・検証する手法である．形式的とは数学的に厳密であることを意味

BERTopic は文書分類に用いられるトピックモデル手法の一種である．トピックモデル手法として LDA(Latent
Dirichlet Allocation) が広く利用されているが，LDA は
ハイパーパラメータの調整の難しさが指摘されている[11]．一方で BERTopic はモデルの学習後にトピックの数を調整できるため，LDA より容易に最適な分類が得られる．また BERTopic は LDA を含む従来のトピック
モデル手法より性能に優れることが報告されている [2]．
本研究では Issue に対して BERTopic を適用し，ソフトウェアに報告される問題をトピックモデルにより分類することで形式手法の適用によるソフトウェア開発に特有の傾向を調査する．

し，形式的に記述された仕様は特定の性質を満たすことを容易に検証できる．2.1 節で述べた Koerner と Brummの研究 [10] は自然言語で記述された仕様の曖昧さを低減するものであるが，形式的に記述された仕様は曖昧さを低減する必要がない．また既存のソフトウェア開発に対して形式手法を適用する手法として自然言語で記述された仕様を形式的に記述された仕様に変換する手法が提案されている [7]．形式的に記述された仕様は自然言語で記述された仕様より品質に優れることが報告されており[3]，ソフトウェア仕様の品質を向上させる手法として形式手法が注目されている．ソフトウェア仕様の品質の向上はソフトウェア品質の向上に寄与するため，形式手法
はソフトウェア工学における重要な題材の 1 つとなっており，その普及が求められている．

1 https://docs.github.com/en/issues
2 https://github.com

123

SEA

ソフトウェア・シンポジウム 2024 in 長崎

表 1. 形式手法を適用して開発されたリポジトリの

表 2. 形式手法を適用せず開発されたリポジトリの

一覧

一覧

リポジトリ

seL4
hacl-starcakeml

Star
数

Issue
数

ソフトウェアの

4445
1558
882

383
222
456

マイクロカーネル

リポジトリ

1721

276

Issue
数

ソフトウェアのblog os

13612

450

オペレーティング

cryfs
shc
hakyll

1915
1856
2633

419
130
485

種類

種類

システム

暗号化ライブラリ
プログラミング
言語

CompCert

Star
数

コンパイラ

暗号化ライブラリ
コンパイラ
静的サイトジェネレータ

3. 形式手法を適用したソフトウェア開発の調査
フトウェアの種類に依存する可能性があり，その影響を

3.1. 調査対象排除するには様々な種類のソフトウェアについてのリポ
ジトリを選定することが望ましい．しかし形式手法を適

本研究では GitHub で公開されているリポジトリの用して開発されたソフトウェアのリポジトリで条件を満

Issue をソフトウェアに対して報告される問題として調査した．調査対象とするリポジトリとして形式手法を適用して開発されたものとそうでないものとの双方についてそれぞれ複数を選定し，選定したリポジトリの Issue を取得した．Issue の取得にあたっては次の条件を満たすリ
ポジトリを選定した．ただし形式手法を適用して開発されたものについては，ドキュメントに”formal method”
および”formal veriﬁcation”のような語が含まれており，
形式手法を適用した旨が判断できるものを目視により選定した．

たすものが少なかったため，傾向の比較からソフトウェ
アの種類による影響を排除するために種類が類似するものを選定した．ここで選定した 8 例のリポジトリのソフ
トウェアの種類は表 1，表 2 に示す通りである．
ここでウェルチの検定（両側検定）により，Issue 数
および Star 数のそれぞれについて形式手法を適用して開発されたソフトウェアとそうでないソフトウェアとの間に有意な差は認められなかった．したがって形式手法を適用して開発されたソフトウェアおよびそうでないソ
フトウェアについて，同等の規模のリポジトリをデータセットとして選定できたと考えられる．

1. Star 数が 100 以上である．
2. Issue 数が 100 以上である．

3.2. 仮説

3. ドキュメントが英語で記述されている．

本研究では各リポジトリの Issue を 4.3 節で述べる error，bug，requirement，improvement，question，maintenance，other の 8 種類のラベルによって分類した．ここで形式手法を適用して開発されたソフトウェアに特有の傾向があることを仮説とし，加えて次の仮説を立てた．

これにより選定した各データセットに属するリポジト
リの一覧を表 1，表 2 に，各データセットに属するリポ
ジトリの Issue 数および Star 数の分布を図 1 にそれぞれ示す．
ただしリポジトリの選定にあたっては，形式手法を適

仮説 1. 形式手法を適用して開発されたソフトウェアはそ用して開発されたものを選定した後に，そうでないもの

うでないソフトウェアより error の出現割合が低い．

として形式手法を適用して開発されたものと規模が同程度でありソフトウェアの種類が類似するものを選定した．

仮説 2. 形式手法を適用して開発されたソフトウェアは

これは形式手法を適用して開発されたソフトウェアのリ

そうでないソフトウェアより bug の出現割合が高い．

ポジトリで条件を満たすものとして発見したものが表 1

仮説 3. 形式手法を適用して開発されたソフトウェアはに示す 4 例のみであったためである．Issue の傾向はソ

124

SEA

ソフトウェア・シンポジウム 2024 in 長崎

number of Stars

14000

500

number of Issues

450

12000

400

10000

count

count

350
8000

300

6000
250
4000

200

2000

150
General methods

Formal methods

General methods

Formal methods

図 1. 形式手法を適用して開発されたリポジトリのデータセットとそうでないリポジトリのデータセットとのIssue 数および Star 数の分布

そうでないソフトウェアより improvement の出現

ある．improvement の出現割合が低いことは形式手法を割合が低い．

適用して開発されたソフトウェアに機能の追加や改善を求める報告が少ないことを示唆する．したがって仮説 3.

仮説 4. 形式手法を適用して開発されたソフトウェアはは形式手法を適用して開発されたソフトウェアに機能のそうでないソフトウェアより maintenance の出現追加や改善の要求が少ないという仮説である．これは形割合が高い．

式手法を適用して開発されたソフトウェアは仕様が形式的に記述されることで仕様の変更が煩雑であると考えら

仮説 1. は error の出現割合についての仮説である．er-

ror の出現割合が低いことは形式手法を適用して開発されたソフトウェアに動作不良の報告が少ないことを示唆する．したがって仮説 1. は形式手法を適用して開発されたソフトウェアに動作不良が少ないという仮説である．
これは形式手法を適用して開発されたソフトウェアは仕様が形式的に記述・検証されることで動作不良が少ないと考えられるために立てたものである．
仮説 2. は bug の出現割合についての仮説である．bugの出現割合が高いことは形式手法を適用して開発された
ソフトウェアにバグの報告が多いことを示唆する．したがって仮説 2. は形式手法を適用して開発されたソフト
ウェアにバグが多いという仮説である．これは形式手法を適用して開発されたソフトウェアは仕様が形式的に記述・検証されることでバグが発見されやすいと考えられるために立てたものである．
仮説 3. は improvement の出現割合についての仮説で125れるために立てたものである．
仮説 4. は maintenance の出現割合についての仮説である．maintenance の出現割合が高いことは形式手法を適用して開発されたソフトウェアに保守に関する報告が多いことを示唆する．したがって仮説 4. は形式手法を適用して開発されたソフトウェアに保守に関する報告が多いという仮説である．これは形式手法を適用して開発されたソフトウェアは仕様が形式的に検証されることで保守が煩雑であると考えられるために立てたものである．

4. 調査手法
形式手法を適用したソフトウェア開発に特有の問題を調査するため，3.1 節で述べたリポジトリの Issue を各々について分類し，その傾向を比較した．調査は以下の手順で行った．

SEA

ソフトウェア・シンポジウム 2024 in 長崎

手順 1. 各リポジトリの Issue を取得し，前処理を行う．
手順 2. 前処理が施された Issue を BERTopic により分表 3. Issue の分類に付与したラベルとその意味
ラベル

類する．

意味

error
動作不良
bug
明確にバグと判断される動作不良
requirement ソフトウェアに対する要求
improvement 特に機能追加・改善の要求
question
ソフトウェアに関する質問
maintenance 保守に関する報告
other
いずれにも分類されないもの

手順 3. 手順 2. で得られた分類に対してラベルを付与する．
手順 4. 手順 3. で得られたラベルの出現頻度を，形式手法を適用して開発されたソフトウェアとそうでない
ソフトウェアとのそれぞれについて集計する．
手順 5. 手順 4. で得られた集計結果をピアソンの χ2 検
定およびウェルチの検定により比較する．

する文書とは各分類に含まれる文書の中で最もその分類を特徴づけると考えられる文書であり，本手順において

4.1. 手順 1. Issue の取得と前処理はそれぞれの分類に対して 3 文書を抽出した．

本手順ではリポジトリから取得した Issue を BERTopic

4.3. 手順 3. ラベルの付与により分類するための前処理を行う．前処理の内容は次の通りである．ただしそれぞれの Issue について，最初本手順では手順 2. で得られた分類に対してラベルをに投稿された内容のみを調査対象としており，その内容付与する．付与するラベルは Hall らの研究 [5] およびに連なって投稿されたコメントは調査対象外とした．

Bissyandé らの研究 [1] において用いられたものを参考に，本研究で取得した Issue の分類に適切であると考えられるものを設定した．付与したラベルとその意味を表3 に示す．
各ラベルは手順 2. で得られた分類において，その分類を代表する文書を参考にして付与した．ただし BERTopicによる分類では外れ値が発生するため，外れ値に対しては一律に other を付与した．

1. Issue の title 要素および body 要素から URL，メー
ルアドレス，コードブロック，記号を除去する．
2. Issue の title 要素および body 要素を結合し，単一のテキストとする．
BERTopic は一般的な文章分類においては前処理を必要としない．しかし本研究で取得した Issue は Markdown3 形式で記述されており，またソフトウェアに対す
る報告であることからエラーメッセージやコードスニ
ペットを含むことがある．これらの情報は文章の意味に影響を与えないが，BERTopic による分類に影響を与える可能性があるため，前処理によって除去した．

4.4. 手順 4. ラベルの集計
本手順では手順 3. で得られたラベルの出現回数を，形式手法を適用して開発されたソフトウェアとそうでない
ソフトウェアとについて集計する．まず各リポジトリにおいて Issue の分類に付与されたラベルから各ラベルに4.2. 手順 2. BERTopic による分類

属する Issue の出現回数を算出し，これを各リポジトリ

本手順では各リポジトリについて前処理を行った Issue

におけるラベルの出現回数とした．次に形式手法を適用

を BERTopic により分類する．この結果として，分類おしたソフトウェアとそうでないソフトウェアとのそれぞ

よびその分類に属する Issue 数，また各分類を代表するれのデータセットについて，各リポジトリにおけるラベ

単語および文書が得られる．ここで分類を代表する単語

ルの出現回数を合算し，これから各ラベルの出現割合をとは各分類に含まれる文書の中で最もその分類を特徴づ算出した．本研究では各データセットについて算出したけると考えられる単語であり，本手順においてはそれぞ

ラベルの出現回数および出現割合を Issue の傾向としてれの分類に対して 10 単語を抽出した．また分類を代表扱う．

3 https://daringfireball.net/projects/markdown

126

SEA

ソフトウェア・シンポジウム 2024 in 長崎

4.5. 手順 5. 統計分析
表 4. 形式手法を適用して開発されたソフトウェア
本手順では手順 4. で得られた Issue をピアソンの χ2の各リポジトリにおけるラベルの出現回数

検定により，各ラベルの出現割合をウェルチの検定により，それぞれ比較する．ここでピアソンの χ2 検定は分

ラベル

seL4
(回)

haclstar
(回)

Cake
ML
(回)

Comp 合計
Cert (回)
(回)

error
bug
requirement
improvement
questionmaintenance
other

108
37
0
30
0
15
193

70
0
0
21
0
41
90

0
0
96
173
0
0
186

18
49
0
32
0
74
103

類されたデータの連関を検定するノンパラメトリック検定であり，ウェルチの検定は平均値の差を検定するパラ
メトリック検定である．本研究においては手順 4. で得られたラベルの出現割合について，形式手法を適用して開発されたソフトウェアとそうでないソフトウェアとの間
でピアソンの χ2 検定を行う．また各ラベルの出現割合
について，形式手法を適用して開発されたソフトウェアとそうでないソフトウェアとの間でウェルチの検定（片側検定）を行う．

196
86
96
256
0
130
572

ただし検定は other のラベルについての情報を除いて行った．これは BERTopic による分類における外れ値にother を付与しており，どの分類にも属さない Issue のみが other のラベルを持つとは限らないためである．

表 5. 形式手法を適用せず開発されたソフトウェア

5. 調査結果

ラベル

blog cryfs
os(回) (回)

error
bug
requirement
improvement
questionmaintenance
other

223
0
0
66
0
0
161

の各リポジトリにおけるラベルの出現回数

形式手法を適用して開発されたソフトウェアとそうでないソフトウェアとにおけるラベルの出現割合の比をピアソンの χ2 検定により有意水準 5%で比較した結果，ラベルの出現割合に有意な差が認められた．ここで 4.3 節，

4.4 節の手順で得た各リポジトリにおけるラベルの出現回数を表 4，表 5 に示す．また表 4，表 5 のそれぞれについて合計の列から算出したラベルの出現割合を表 6 に示す．これが 4.5 節の手順で検定により比較した対象である．
また 3.2 節で立てた仮説に用いる error，bug，improvement，maintenance のラベルについて，ウェルチの検定（片側検定）により有意水準 5%で出現割合の大小関係をそれぞれ比較した．その結果を次に示す．

154
15
0
68
0
0
182

shc
(回)
58
0
0
0
0
0
72

hakyll 合計(回) (回)
105
0
0
83
50
0
247

540
15
0
217
50
0
662

り有意に低いことが認められなかった．

4. maintenance の出現頻度は形式手法を適用して開発されたソフトウェアがそうでないソフトウェアより有意に高いことが認められなかった．
また有意な差が認められなかった仮説 2.，仮説 3.，仮

1. error の出現頻度は形式手法を適用して開発された
ソフトウェアがそうでないソフトウェアより有意に低いことが認められた．

説 4. について，それぞれと逆の事象を示す次の仮説を立てた．

2. bug の出現頻度は形式手法を適用して開発されたソ
フトウェアがそうでないソフトウェアより有意に高いことが認められなかった．

仮説 2′ . 形式手法を適用して開発されたソフトウェアは

3. improvement の出現頻度は形式手法を適用して開発されたソフトウェアがそうでないソフトウェアよそうでないソフトウェアより improvement の出現

そうでないソフトウェアより bug の出現割合が低い．
仮説 3′ . 形式手法を適用して開発されたソフトウェアは割合が高い．

127

SEA

ソフトウェア・シンポジウム 2024 in 長崎

表 6. 形式手法を適用して開発されたソフトウェア

表 7. 形式手法を適用して開発されたソフトウェアとそうでないソフトウェアにおけるラベルの出現におけるラベルの出現割合

割合
ラベル

error
bug
requirement
improvement
questionmaintenance
other

形式手法を

形式手法を

適用 (%)

適用せず (%)

14.67
6.44
7.19
19.16
0.00
9.73
42.81

36.39
1.01
0.00
14.62
3.37
0.00
44.61

仮説 4′ . 形式手法を適用して開発されたソフトウェアは

ラベル

seL4
(%)

haclstar
(%)

error
bug
requirement
improvement
questionmaintenance
other

28.20
9.66
0.00
7.83
0.00
3.92
50.39

31.53
0.00
0.00
9.46
0.00
18.47
40.54

CakeML Comp
(%)
Cert
(%)
0.00
0.00
21.10
38.02
0.00
0.00
40.88

6.52
17.75
0.00
11.59
0.00
26.81
37.32

表 8. 形式手法を適用せず開発されたソフトウェア

そうでないソフトウェアより maintenance の出現におけるラベルの出現割合割合が低い．
これらの仮説についてウェルチの検定（片側検定）に

ラベル

blog
os(%)

cryfs
(%)

shc
(%)

hakyll
(%)

error
bug
requirement
improvement
questionmaintenance
other

41.30
0.00
0.00
14.67
0.00
0.00
35.78

36.80
3.58
0.00
16.23
0.00
0.00
43.44

44.62
0.00
0.00
0.00
0.00
0.00
55.38

21.65
0.00
0.00
17.11
10.31
0.00
50.93

より有意水準 5%で出現割合の大小関係をそれぞれ比較した．その結果を次に示す．

1. bug の出現頻度は形式手法を適用して開発されたソ
フトウェアがそうでないソフトウェアより有意に低いことが認められなかった．
2. improvement の出現頻度は形式手法を適用して開発されたソフトウェアがそうでないソフトウェアより有意に高いことが認められなかった．

間で Issue の傾向に有意な差が認められた．このことは

3. maintenance の出現頻度は形式手法を適用して開発されたソフトウェアがそうでないソフトウェアより有意に低いことが認められなかった．

形式手法を適用したソフトウェア開発に特有の傾向が存在することを示唆している．また 3.2 節で立てた仮説について，仮説 1. は支持されたが仮説 2.，仮説 3.，仮説

4. は支持されなかった．
以下でそれぞれの仮説について考察する．
仮説 1. が支持されたことは，形式手法を適用して開発されたソフトウェアはそうでないソフトウェアより動作不良の報告が少ないことを示唆する．したがって形式
手法の適用がソフトウェアの動作不良を低減すると考えられる．
仮説 2. が支持されなかったことは，形式手法を適用して開発されたソフトウェアはそうでないソフトウェア
よりバグの報告が多いとは言えないことを示唆する．各

ここでウェルチの検定による比較に用いた各データ
セットにおけるラベルの出現割合を表 7，表 8 にそれぞ
れ示す．

6. 議論
本研究では形式手法を適用したソフトウェア開発に特有の傾向を，ソフトウェアのリポジトリに対して報告された Issue に着目して調査した．その結果，形式手法を適用されたソフトウェアとそうでないソフトウェアとの

128

SEA

ソフトウェア・シンポジウム 2024 in 長崎

データセットにおけるラベルの出現割合に着目すると，アの動作不良を低減することを示唆するものである．

双方ともに半数以上のリポジトリにおいて bug の出現割

ここで本研究が抱える課題として次が挙げられる．

合が 0.0%であった．一般にソフトウェアがバグを含まな

課題 1. BERTopic による分類に多くの外れ値が含まれいことは考え難いため，bug が付与されるべき Issue にている．

他のラベルが付与されていると考えられる．ここで bugが付与されるべき Issue に error が付与されていること

課題 2. OSS と産業用ソフトウェアとの差異を考慮してが考えられる．Issue における動作不良の報告はその後いない．

の議論によって bug と判断されることがあるが，本研究
課題 3. リポジトリの開発段階を考慮していない．

では Issue を title 要素および body 要素に着目して分類しており，そのような議論を反映していない．したがっ課題 1. は BERTopic による分類において，多くの Issueて形式手法の適用がソフトウェアにおけるバグの発見をが外れ値と判定され，分類が推定されなかったことを指容易にするとは言えないが，Issue に付随する議論を含す．本研究では Issue の title 要素および body 要素をトめた今後の調査が必要であると考えられる．

ピックモデルにより分類するために BERTopic を用いた仮説 3. が支持されなかったことは，形式手法を適用が，その結果として多くの Issue が外れ値と判定され，分して開発されたソフトウェアはそうでないソフトウェア類が推定されなかった．本研究ではこの外れ値に other

より機能の追加や改善の要求が少ないとは言えないことのラベルを付与したため，一部の Issue について適切なを示唆する．したがって形式手法の適用がソフトウェア

ラベルが付与できていないと考えられる．BERTopic はへの機能の追加や改善の要求に与える影響は小さいと考外れ値を削減する手法を複数持つため，今後はそれらのえられる．

手法を用いて外れ値を削減することが望ましいと考えら

仮説 4. が支持されなかったことは，形式手法を適用れる．

して開発されたソフトウェアはそうでないソフトウェア

課題 2. は本研究で対象を OSS(Open Source Software)

より保守に関する報告が多いとは言えないことを示唆すに限定しているために産業用ソフトウェアについての調る．ここで形式手法を適用せず開発されたソフトウェア

査が行われていないことを指す．産業用ソフトウェアのにおけるラベルの出現割合は全てのリポジトリにおいて開発には OSS の開発とは異なる事情が存在する．例え

0.0%であり，形式手法を適用して開発されたソフトウェ
アに保守に関する報告が多いように思われる．一方で各データセットにおけるラベルの出現割合についての検定
結果は maintenance の出現割合について有意な差を示さなかった．この一因としてデータセットにおけるリポジ
トリの少なさが考えられる．したがって形式手法の適用がソフトウェアにおける保守に与える影響については今後の調査が必要であると考えられる．

ば OSS においては開発者は形式手法を独学するが，産業用ソフトウェアにおいては開発者は形式手法について教育を受ける，などである．そのため OSS と産業用ソ
フトウェアとでは形式手法の適用による影響が異なると考えられる．
課題 3. はリポジトリの開発段階を考慮していないことを指す．本研究で調査対象としたリポジトリは Star 数
および Issue 数のみを選定条件としたが，Issue はソフト
ウェアの開発段階によって傾向が変化すると報告されて

7. 今後の展望いる [1]．そのためバージョンや開発期間など，リポジ
トリの開発段階を条件に加えてリポジトリを選定するこ本研究では形式手法を適用したソフトウェア開発に特とが望ましいと考えられる．ただし GitHub において公有の傾向を，リポジトリに対して報告された Issue に着開されているリポジトリで形式手法を適用して開発され目して調査した．その結果，形式手法を適用したソフト

たものは極めて少なく，この条件を加えてリポジトリをウェア開発とそうでないソフトウェア開発との間で Issue

選定することは難しい．

の傾向に有意な差が認められた．この差は形式手法の適今後は以上の課題を解消することにより，形式手法を用がソフトウェア開発に与える影響を示唆するものであ

適用したソフトウェア開発に特有の傾向をより詳細に調る．一方で個々のラベルについては error のみに有意な査することが望ましいと考えられる．

差が認められた．この差は形式手法の適用がソフトウェ

129

SEA

ソフトウェア・シンポジウム 2024 in 長崎

8. 結言[5] T. Hall, A. Rainer, N. Baddoo, and S. Beecham. An
empirical study of maintenance issues within process
improvement programmes in the software industry. In
In Proceedings of 17th IEEE International Conference
on Software Maintenance (ICSM), pp. 422–430, 2001.

本研究ではソフトウェアに対して報告された問題としてソフトウェアのリポジトリに対して報告された Issueに着目し，形式手法を適用したソフトウェア開発に特有[6] M. Huisman, D. Gurov, and A. Malkis. Formal methods: From academia to industrial practice: A travel
guide. Workingpaper, Cornell University, 2020.

の傾向を調査した．その結果，形式手法を適用したソ
フトウェア開発とそうでないソフトウェア開発との間でIssue の傾向に有意な差が認められた．このことは形式手法を適用したソフトウェア開発に特有の傾向が存在することを示唆するものである．
またソフトウェアの動作不良に関する報告について，
形式手法を適用して開発されたソフトウェアがそうでな
いソフトウェアより有意に少ないことが認められた．このことは形式手法の適用がソフトウェアの動作不良を低減することを示唆するものである．
一方でソフトウェアの機能追加や改善を求める報告について，形式手法を適用して開発されたソフトウェアとそうでないソフトウェアとの間に有意な差は認められなかった．このことは形式手法の適用がソフトウェアへの機能の追加や改善の要求に与える影響が小さいことを示
唆するものである．
この他にバグ，保守に関する報告についても形式手法を適用して開発されたソフトウェアとそうでないソフト
ウェアとの間に有意な差は認められなかった．これらはIssue に付随する議論の内容を考慮していないことやサン
プル数の少なさ，トピック分析による外れ値に起因している可能性が考えられるため，今後の調査が求められる．

参考文献[7] M. Ilieva and O. Ormandjieva. Automatic transitionof natural language software requirements speciﬁcation into formal presentation. In In Proceedings of the10th International Conference on Application of Natural Language to Information Systems (NLDB), pp.
392–397, 2005.
[8] E. Kamsties. Understanding Ambiguity in Requirements Engineering, pp. 245–266. Springer Berlin Heidelberg, 2005.
[9] E. Knauss, C. Boustani, and T. Flohr. Investigating
the impact of software requirements speciﬁcation quality on project success. In In Proceedings of the 10th
International Conference on Product Focused Software
Process Improvement, Vol. 32, pp. 28–42, 2009.
[10] S. J. Körner and T. Brumm. Natural language speciﬁcation improvement with ontologies. International
Journal of Semantic Computing, 3(4):445–470, 2009.
[11] A. Panichella. A systematic comparison of searchbased approaches for LDA hyperparameter tuning. Information and Software Technology, 130:1–20, 2021.
[12] A. Reid, L. Church, S. Flur, S. de Haas, M. Johnson, and B. Laurie. Towards making formal methods
normal: meeting developers where they are. arXiv
preprint arXiv:2010.16345, 2020.
[13] H. Yang, A. De Roeck, V. Gervasi, A. Willis, andB. Nuseibeh. Analysing anaphoric ambiguity in natural language requirements. Requirements engineering,
16:163–189, 2011.
[14] 荒木. ソフトウェア開発現場への形式手法導入形式手法
適用の実経験から得られた知見. SEC journal, 6(2):104–
107, 2010.

[1] T. F. Bissyandé, D. Lo, L. Jiang, L. Réveillere,
J. Klein, and Y. Le Traon. Got issues? Who cares
about it? A large scale investigation of issue trackers from GitHub. In In Proceedings of the 24th IEEE
International Symposium on Software Reliability Engineering (ISSRE), pp. 188–197, 2013.
[2] R. Egger and J. Yu. A topic modeling comparison
between LDA, NMF, Top2Vec, and BERTopic to demystify twitter posts. Frontiers in sociology, 7:1–16,
2022.
[3] F. Fabbrini, M. Fusani, S. Gnesi, and G. Lami. An
automatic quality evaluation for natural language requirements. In In Proceedings of the 7th International
Workshop on Requirements Engineering: Foundationfor Software Quality (REFSQ), Vol. 1, pp. 4–5, 2001.
[4] M. Grootendorst. Bertopic: Neural topic modelingwith a class-based TF-IDF procedure. arXiv preprint
arXiv:2203.05794, 2022.

[15] 荒木. 形式手法導入のための産学連携 PBL の活用. SEC
journal, 7(4):177–182, 2011.
[16] 大西, 吉村, 阿部, 稲川, 山本, 堀. 工業高等専門学校の学生に対する形式手法 b-method の学生実験の実践. 情報処理学会論文誌, 61(4):863–883, 2020.
[17] 栗田. 形式手法の実践に対してよく尋ねられる質問とその回答モバイル FeliCa の開発における形式仕様記述を通して. SEC journal, 7(1):34–39, 2011.
[18] 喜多村, 上原他. F*言語による MQTT パケットパーサの開発と安全性評価. 研究報告セキュリティ心理学とトラスト (SPT), 2021(8):1–7, 2021.
[19] 青木. 車載システム開発における形式手法実践の現状と課題. システム／制御／情報, 62(4):134–140, 2018.

130

SEA