著者
畑 秀明 水野 修 菊野 亨
出版者
日本ソフトウェア科学会
雑誌
コンピュータ ソフトウェア (ISSN:02896540)
巻号頁・発行日
vol.29, no.1, pp.1_106-1_117, 2012-01-26 (Released:2012-02-26)

近年,ソフトウェアリポジトリのデータマイニングを利用した不具合予測の研究が活発に行われている.不具合予測に関連してどのようなメトリクスが研究されているかを明らかにするため,本稿では系統的レビューを行った.2つの論文誌と5つの国際会議において,2000年から2010年に発表された文献のうち63編を調査した.研究されたメトリクスを分析するため,測定対象と測定に必要な履歴情報に基づき8つの領域に分類した.レビューの結果,主に2005年以降コードやプロセスの履歴に基づくメトリクスが研究されるようになっており,また2008年以降には新たに開発組織や地理的位置関係に関連したメトリクスが提案されていることが明らかになった.
著者
片山 卓也
出版者
日本ソフトウェア科学会
雑誌
コンピュータ ソフトウェア (ISSN:02896540)
巻号頁・発行日
vol.36, no.3, pp.3_33-3_46, 2019

<p>国民年金法の述語論理による記述と定理自動証明システムZ3Pyによる検証に関するケーススタディついて述べた.法令の作成は伝統的に人手により行われて来たが,近年法令が大量に作られるようになり,その品質の維持には計算機科学,特にソフトウェア工学や人工知能で培われた技術を応用することが有効であると考えられる.本稿では,法令を意図した通りに正しく作る上で,法令の形式的記述と自動検証技術が有効であることを確認する目的で,国民年金法の基本的条文の述語論理による記述と,そのSMTソルバーZ3Pyによる検証を試行した結果を報告する.法令の文章上の複雑さは別にすると,その論理的深度は深くなく,このような方法が誤りの無い法令を作る上で有効な方法になり得ることが分かった.</p>
著者
高田 広章
出版者
日本ソフトウェア科学会
雑誌
コンピュータ ソフトウェア (ISSN:02896540)
巻号頁・発行日
vol.37, no.3, pp.3_45-3_66, 2020-07-22 (Released:2020-09-22)

使用するOSオブジェクトをシステム構築時に生成する静的OSにおいては,OSオブジェクトの生成に必要なコンフィギュレーション情報を,何らかの方法で記述する必要がある.静的APIは,リアルタイムOSのコンフィギュレーション情報を記述するための記述言語である.μITRON4.0仕様においてはじめて導入し,TOPPERS新世代カーネル仕様において改善を行った.本論文では,静的APIに求められる要件と,それらの仕様における静的APIの具体的な仕様について述べる.また,静的APIを処理するコンフィギュレータの設計と実装について,TOPPERSプロジェクトにおける約20年間の開発の歴史に沿って述べる.
著者
登 大遊 新城 靖 佐藤 聡
出版者
日本ソフトウェア科学会
雑誌
コンピュータ ソフトウェア (ISSN:02896540)
巻号頁・発行日
vol.32, no.4, pp.4_3-4_30, 2015-10-26 (Released:2015-12-26)

SoftEther VPN Serverはマルチプロトコル対応のクロスプラットフォームなオープンソースVPNサーバソフトウェアであり,既存のVPNサーバプログラムにない2つの特徴がある.1つ目は,単一VPNサーバインスタンスで複数のVPNプロトコルをサポートしている点にある.管理者は,複数のVPNプロトコルによる多種類のVPNデバイスからのリモートアクセスおよび拠点間接続を受付けるVPNサーバを容易に管理することができる.そのために,SoftEther VPN Server内にL2アダプタと呼ばれるモジュールを実装し,レイヤ2 VPNプロトコルとレイヤ3 VPNプロトコルとの間の通信を,共通のバスである仮想L2スイッチを経由させ,シームレスに実現にした.2つ目は,ユーザ管理やネットワークの機能を仮想化するマルチテナント機能である.これは,仮想ホスティングサービスのために必須である.本プログラムは複数のOS間の移植性を有する.本プログラムは2013年3月から2014年9月までの間に,世界中で242,000回インストールされた実績を有する.また,異なるVPNプロトコル間での通信速度実験では,従来のVPNプロトコルのネイティブなVPNサーバプログラムを組み合わせて用いた場合と比較して高速な結果が得られた.
著者
宋 剛秀 番原 睦則 田村 直之
出版者
日本ソフトウェア科学会
雑誌
コンピュータ ソフトウェア (ISSN:02896540)
巻号頁・発行日
vol.34, no.1, pp.1_67-1_80, 2017-01-25 (Released:2017-03-25)

近年SATソルバーの求解性能が飛躍的に向上しており,様々な分野で応用が進んでいる.しかし,SATソルバーは連言標準形の命題論理式を入力としており,実用的な応用が多くある算術制約を含むような問題を直接記述して解くことには向いていない.このため,より表現力のある入力形式に対応できるようにSATソルバーを利用・拡張したシステムが研究されている.本解説では,そのような利用・拡張の1つとしてSATソルバーの求解性能と制約プログラミングシステムの表現力を融合させたSAT型制約プログラミングシステム(SAT型CPシステム)について説明し,その周辺技術についても概説する.
著者
沢田 篤史 野呂 昌満
出版者
日本ソフトウェア科学会
雑誌
コンピュータ ソフトウェア (ISSN:02896540)
巻号頁・発行日
vol.32, no.1, pp.1_35-1_46, 2015-01-26 (Released:2015-03-26)

ソフトウェアアーキテクチャの設計結果は,開発対象であるソフトウェアシステムの完成時における機能や非機能に関する様々な特徴だけでなく,実装や検証,保守など,他の開発プロセスに多大な影響を及ぼす.高品質のシステムを開発するために,アーキテクチャ設計を支援する技術は重要である.また,システムの品質を適切に予測し,管理を可能とするためには,設計結果としてのアーキテクチャと,その設計過程において行われた判断を文書化することも重要である.長期間にわたって運用されるシステムにおいては,アーキテクチャ設計に関連する文書と,要求仕様,設計,実装などの他のソフトウェア構成要素との間の追跡可能性が求められる.本稿ではまず,高品質のソフトウェアシステム開発におけるソフトウェアアーキテクチャの重要性について解説する.アーキテクチャ設計と文書化に関連し,アーキテクチャスタイル,パターン,関心事,ビューなどの諸概念についてそれらの意味的関連も含めて説明する.さらに,アーキテクチャに関する設計判断の文書化技術,追跡性管理と知識管理の技術,それらを支援するツールの動向を解説する.
著者
上嶋 祐紀 住井 英二郎
出版者
日本ソフトウェア科学会
雑誌
コンピュータ ソフトウェア (ISSN:02896540)
巻号頁・発行日
vol.26, no.1, pp.139-154, 2009

C言語サブセットのプログラムを安全なJava言語のプログラムに変換する方式を実装した.そのような変換のためには,C言語独特の操作であるポインタ演算を,Javaプログラムで安全に模倣する必要がある.これを実現するために,まずC言語のポインタやメモリブロックを表現するJavaのクラスを定義した.次に,これらのクラスを利用するようなJavaへの変換規則を定め,規則に従ってトランスレータを実装した.また,C言語ではポインタと整数を相互にキャストすることが可能なので,整数もポインタと同様のオブジェクトに変換しなければならない.しかし,すべての整数をポインタと同様に表現すると大幅に効率が悪化する.そこで,データフロー解析により,ポインタが代入されない基本型の変数は,Javaの通常の基本型変数に変換する,などの最適化を実装した.9個のベンチマークプログラムで実験したところ,最適化前の変換結果コードは元のCプログラムに対し3.3倍~585倍程度の実行時間がかかったが,最適化後は(元のCプログラムに対し)1.3倍~5.9倍程度に改善した.
著者
横尾 真 岩崎 敦 櫻井 祐子 岡本 吉央
出版者
日本ソフトウェア科学会
雑誌
コンピュータ ソフトウェア (ISSN:02896540)
巻号頁・発行日
vol.29, no.3, pp.3_39-3_53, 2012-07-25 (Released:2012-09-25)

本編では非協力ゲーム(発展編)として,非協力ゲームの均衡概念で最も重要なものであるナッシュ均衡について詳しく述べる.2人ゼロサム標準形ゲームでは,プレイヤが選択可能な純粋戦略の個数に関する多項式時間でナッシュ均衡を計算できる.しかしながら,プレイヤが交互に行動を繰り返し選択するような複雑なゲームでは純粋戦略の個数が膨大となる.本編では,このような複雑な2人ゼロサムゲームの均衡を計算する例として,ポーカー等のカードゲームにおいてナッシュ均衡を計算するアルゴリズムを紹介する.一方,一般の有限2人標準形ゲームでは,ナッシュ均衡が多項式時間で計算可能かどうかが分かっていない.しかしながら,ナッシュ均衡の存在自体は証明されているので,PやNPのような判定問題に関する概念は,ナッシュ均衡計算問題の難しさを議論するためには適切ではない.本編では,ナッシュ均衡計算問題の難しさを議論する際に有用な問題のクラスであるPPAD,およびPPAD完全性について解説する.
著者
上野 雄大 大堀 淳
出版者
日本ソフトウェア科学会
雑誌
コンピュータ ソフトウェア (ISSN:02896540)
巻号頁・発行日
vol.29, no.1, pp.1_191-1_210, 2012-01-26 (Released:2012-02-26)

本論文では,多相レコード計算のコンパイル方式を応用し軽量に実現可能な,型付き関数型言語の第一級オーバーロード方式を提案する.この方式の下では,オーバーロードされた関数は,オーバーロードされた型上のみを動く型変数で束縛された多相型を持つ第一級の関数として扱われる.本機能の実現に要求されるものは,型抽象におけるインスタンス変数の生成と,型適用におけるインスタンスの選択のみであり,これらは多相レコードコンパイルと同様の方式で達成できる.本方式はSML#コンパイラ上に実装され公開されている.
著者
阪上 紗里 浅井 健一
出版者
日本ソフトウェア科学会
雑誌
コンピュータ ソフトウェア (ISSN:02896540)
巻号頁・発行日
vol.26, no.2, pp.2_3-2_17, 2009-04-24 (Released:2009-06-24)

「プログラムの残りの計算」を表す継続を扱う為の基礎言語体系として,対称λ計算(Symmetric λ-calculus, SLC)がFilinskiによって提案されている.SLCにおいては項と継続が完全に対称な形をしており,項を扱うのと同じように継続を扱うことができる.そのため,項と継続を統一的に議論するのに適していると思われるが,これまでSLCについての研究はほとんどなされていない.ここでは,まずSLCをsmall step semanticsで定式化し直し,型付き言語の基本的な性質であるProgressとPreservationを満たすことを証明する.次に,SLCが継続計算を議論・表現するのに適していることを示すため,(1) FelleisenのCオペレータを含むcall-by-value言語,ΛC計算,および(2) Parigotのcall-by-name λμ計算が,どちらも自然にSLCに変換できることを示す.近年call-by-valueとcall-by-nameの双対性が項と継続の対称性と絡めて注目されているが,ここでの結果はそれに対する洞察を与えるものと期待される.
著者
山本 章博
出版者
日本ソフトウェア科学会
雑誌
コンピュータ ソフトウェア (ISSN:02896540)
巻号頁・発行日
vol.23, no.2, pp.2_29-2_44, 2006 (Released:2006-06-30)
被引用文献数
1

帰納論理プログラミングとは,論理プログラムを用いた機械学習手法であり,構造化データからのデータ分析と知識獲得への応用が進められている.本稿では,計算の立場から学習という行為を捉えた上で,パラメータ推定と比較しつつ,論理プログラミングの理論と計算論的学習理論を基礎にして帰納論理プログラミングの基礎理論について解説する.そして,演繹的な推論によって定義される順序関係である精密化が,帰納論理プログラミングの学習アルゴリズムの設計と分析に威力を発揮することを詳述する.さらに,帰納論理プログラミングの最近の研究動向についても述べる.
著者
小形 真平 松浦 佐江子
出版者
日本ソフトウェア科学会
雑誌
コンピュータ ソフトウェア (ISSN:02896540)
巻号頁・発行日
vol.27, no.2, pp.2_14-2_32, 2010-04-27 (Released:2010-06-27)

業務システム開発では,顧客と開発者の間の要求の誤解,顧客の暗黙的要求の存在,開発者の要求の誤った仕様化を原因として,要求仕様の品質が低下する問題がある.そこで,顧客が妥当性を確認した要求分析モデルによるシステム開発手法の確立を目的として,業務系Webアプリケーション開発を対象に,UML要求分析モデルからWeb UIプロトタイプを自動生成する手法を提案する.本研究では,業務を構成する業務遂行手順および業務データをそれぞれ,サービスを構成するユーザとシステムのやり取りおよびやり取り中の入出力データとみなす.そして,この振舞いとデータの観点から,アクティビティ図・クラス図・オブジェクト図を用いて要求分析モデルを定義し,要求分析モデルの妥当性を確認するためのHTML形式のUIプロトタイプを生成する.本稿では,複数の適用事例を通して提案手法の有効性について議論する.
著者
大堀 淳
出版者
Japan Society for Software Science and Technology
雑誌
コンピュータ ソフトウェア (ISSN:02896540)
巻号頁・発行日
vol.31, no.1, pp.1_30-1_42, 2014

コンパイラの構文解析器に広く使用されているLR構文解析の原理を解説する.LR構文解析の基礎をなすアイデアは,「正規言語の解析手法を繰り返し使い,文脈自由文法の幅広いクラスを解析する」という(多くの優れたアイデアがそうであるように)単純なものである.Knuthは,この直感的で単純なアイデアを基礎とし,緻密な理論的な展開と巧みな実用化戦略によって,構文解析におけるブレークスルーを達成した.本解説では,LR構文解析が基礎とするアイデアに即してその原理とアルゴリズムの構造を解説する.これらを理解するならば,一般に複雑で難解なものと受け取られているLR構文解析法の全体像が容易に理解できるはずである.本解説では,オートマトンの基礎知識を持つ一般の読者が,LR構文解析の考え方と原理を理解できることを目指す.
著者
戸田 貴久 斎藤 寿樹 岩下 洋哲 川原 純 湊 真一
出版者
日本ソフトウェア科学会
雑誌
コンピュータ ソフトウェア (ISSN:02896540)
巻号頁・発行日
vol.34, no.3, pp.3_97-3_120, 2017-07-25 (Released:2017-08-09)

列挙問題とは,与えられた条件を満たす対象(解)をすべて求める問題であり,電力網解析など社会のさまざまな問題への応用がある.さまざまな組合せ列挙問題に対して,問題の解集合を表現するデータ構造ZDDを高速に求める方法(トップダウンZDD構築法)を通して元の問題を効率的に解く汎用的な手法の研究が近年盛んに行われている.本論文ではトップダウンZDD構築に焦点を絞り,基礎となるアルゴリズムから,複雑な問題制約に対処するための発展的手法,プログラミングツールTdZddの基本的な使い方,さらに,具体的な応用問題を例にしたプログラミングまで解説する.