著者
安永 憲司
出版者
日本ソフトウェア科学会
雑誌
コンピュータ ソフトウェア (ISSN:02896540)
巻号頁・発行日
vol.34, no.1, pp.1_81-1_92, 2017-01-25 (Released:2017-03-25)

暗号技術の設計にゲーム理論の手法を利用した研究が行われるようになっている.本稿では,暗号の研究においてゲーム理論がどのように関わっているかについて概説する.特に,暗号プロトコルにおける合理的なプレイヤー,均衡概念による安全性の特徴付け,報酬を利用した委託計算について解説する.
著者
誉田 直美 山田 茂
出版者
日本ソフトウェア科学会
雑誌
コンピュータ ソフトウェア (ISSN:02896540)
巻号頁・発行日
vol.30, no.2, pp.2_66-2_82, 2013-04-25 (Released:2013-08-25)

高品質ソフトウェア開発の実現は重要な課題であるものの,それを達成している開発組織は少ない.本論文では,ソフトウェア開発の品質問題を解決するために日本電気株式会社が考案した品質管理手法「ソフトウェア品質会計」を論述する.さらに,従来からの品質会計の適用方法を見直すことによって品質向上を実現した事例を紹介する.その改善事例に基づいて,品質会計の厳格な適用と品質会計を取り巻くソフトウェアプロセス全般に対する総合的な取り組みが,高品質ソフトウェア開発の実現に効果を発揮することを示す.
著者
井上 克巳 坂間 千秋
出版者
日本ソフトウェア科学会
雑誌
コンピュータ ソフトウェア (ISSN:02896540)
巻号頁・発行日
vol.25, no.3, pp.3_20-3_32, 2008-07-25 (Released:2008-09-30)
被引用文献数
1

Prologがベースとしているホーン節論理に基づく論理プログラミングでは,構文的制約があって確定的知識しか表現できないことが,現実的な知識表現のためには限界であるとされていた.この問題点を克服するために,論理プログラミングにおいて不完全・不確定な情報を扱うための拡張理論が1980年代後半から数多く提案された.1999年にはこれらに加えて制約プログラミングの概念を融合した解集合プログラミングの概念が確立され,現在では論理プログラミングの中心的な研究テーマの1つになっている.本稿では過去からのこうした研究の流れと新しい論理プログラミングの可能性について探る.
著者
藤井 秀明 原口 弘志 泥谷 誠 岩瀬 高博 岩爪 道昭
出版者
日本ソフトウェア科学会
雑誌
コンピュータ ソフトウェア (ISSN:02896540)
巻号頁・発行日
vol.30, no.1, pp.1_130-1_151, 2013-01-25 (Released:2013-03-05)

近年,ビッグデータと呼ばれる大量データの集積と戦略的な利活用に対する関心と期待が大きく高まっている.本論文では,その技術的背景として,大量データの集積化および並列分散処理を支える基盤ソフトウェア技術に焦点を当て,代表的な研究開発事例について紹介する.また,同分野全体の俯瞰化を試み,今後の技術動向について議論する.
著者
河野 真治 佐渡山 陽
出版者
日本ソフトウェア科学会
雑誌
日本ソフトウェア科学会大会講演論文集
巻号頁・発行日
vol.19, pp.4B2, 2002

PS2Linux は,PlayStation2上で動作するLinuxである。PS2の描画機構であるEmotion Engine および専用DSPであるVUの特徴を活かしつつ、ネットワークゲームを構築するフレームワークを提案する。ネットワーク部分には、リアルタイム処理を考慮したユーザレベル・トランスポート層を持つSuciライブラリを用いる。
著者
鵜川 始陽 信岡 孝佳 海野 弘成 湯淺 太一
出版者
日本ソフトウェア科学会
雑誌
コンピュータ ソフトウェア (ISSN:02896540)
巻号頁・発行日
vol.29, no.3, pp.3_143-3_156, 2012-07-25 (Released:2012-08-20)

ロックやメモリバリア命令の実行には多くのCPUサイクルを消費するため,並行GC(ごみ集め)では,書込みバリアからロックやメモリバリア命令を排除することが容易なインクリメンタルアップデートGCが使われることが多い.しかし,インクリメンタルアップデートGCの通常の実装では,マークフェーズ後にミューテータを止めて多くのオブジェクトをマークする可能性があり,実時間アプリケーションには向かない.本論文では,この処理が必要のないスナップショットGCを使った並行GCを提案する.提案するGCでは,ロックやメモリバリア命令の頻繁な使用を避けるために,ミューテータは書込みの履歴を溜めておいて,GCとハンドシェイクすることで,履歴をまとめてGCに渡す.このGCをDalvik VMに実装し,評価を行った.
著者
畑 秀明 水野 修 菊野 亨
出版者
日本ソフトウェア科学会
雑誌
コンピュータ ソフトウェア (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

帰納論理プログラミングとは,論理プログラムを用いた機械学習手法であり,構造化データからのデータ分析と知識獲得への応用が進められている.本稿では,計算の立場から学習という行為を捉えた上で,パラメータ推定と比較しつつ,論理プログラミングの理論と計算論的学習理論を基礎にして帰納論理プログラミングの基礎理論について解説する.そして,演繹的な推論によって定義される順序関係である精密化が,帰納論理プログラミングの学習アルゴリズムの設計と分析に威力を発揮することを詳述する.さらに,帰納論理プログラミングの最近の研究動向についても述べる.