著者
阿萬 裕久 野中 誠 水野 修
出版者
日本ソフトウェア科学会
雑誌
コンピュータ ソフトウェア (ISSN:02896540)
巻号頁・発行日
vol.28, no.3, pp.3_12-3_28, 2011-07-26 (Released:2011-09-26)

ソフトウェアメトリクスは,ソフトウェアの品質マネジメントを実践する上で必要不可欠な存在である.しかしながら,実際のところ広く積極的に活用されているとまでは言い難い.その背景には“何を測り,どう活用するのか?”というシンプルではあるが容易でない問題がある.本論文はそのための一助として,ソフトウェアメトリクスとそこでのデータ分析の基礎,特に,どういったソフトウェアメトリクスや数理モデルがあり,分析で何に気を付けるべきかを中心に解説を行っている.また,ソフトウェアメトリクスの円滑な活用に役立つツールもいくつか紹介している.
著者
横尾 真 岩崎 敦 櫻井 祐子 岡本 吉央
出版者
日本ソフトウェア科学会
雑誌
コンピュータ ソフトウェア (ISSN:02896540)
巻号頁・発行日
vol.30, no.2, pp.2_33-2_51, 2013-04-25 (Released:2013-08-25)

本稿では,ゲーム理論の主要領域の1つである協力ゲームについて解説する.協力ゲームは,主に2つの研究領域からなる.1つは,提携内のプレイヤ間で,協力によって得られた利益をどのように分配するかである.本編では,解概念と呼ばれる,協力的なエージェント間で利得を配分する望ましい方法について概説する.古典的な協力ゲーム理論では,コア,シャプレイ値,仁など,さまざまな解概念が提案されている.これらの解概念によって与えられる利得の配分を求めるアルゴリズムと計算量について考察する.2つ目は,全体提携が最適ではない場合,プレイヤがどのような協力関係(提携)を形成するかである.これは,提携構造形成問題(CSG)と呼ばれる.本編では,CSGを効率的に解く制約付き最適化アルゴリズムを紹介する.また,本編ではゲームの簡潔表現法を利用することで解概念やCSGに関する問題を効率的に解くことができるため,協力ゲームの簡潔な記述方法を概説する.
著者
妻木 俊彦
出版者
日本ソフトウェア科学会
雑誌
コンピュータ ソフトウェア (ISSN:02896540)
巻号頁・発行日
vol.29, no.2, pp.2_43-2_64, 2012-04-25 (Released:2012-06-25)

要求工学は,ソフトウェアシステムの外部仕様である振る舞いや制約を定義するための技術の集合である.そして,そこで定義された要求は,われわれが実際に生存している現実世界における意味や価値を反映したものでなければならない.極めて多岐にわたる要求工学の技術を,本稿では,正確な要求を定義するための技術,変動する要求に対処するための技術,および,視点の多様性に対応するための技術という3つの観点から概観する.
著者
高橋 和也 南出 靖彦
出版者
日本ソフトウェア科学会
雑誌
コンピュータ ソフトウェア (ISSN:02896540)
巻号頁・発行日
vol.38, no.2, pp.2_53-2_70, 2021-04-23 (Released:2021-06-23)

文字列の検索等に広く用いられる正規表現マッチングはその多くがバックトラックに基づくアルゴリズムで実装されており,対象文字列の長さに対して線形時間でマッチングを完了できない場合がある.これを事前に検知するために,マッチングに要する計算量を静的解析する手法が複数の先行研究によって提案されている.本研究では先行研究を拡張し,先読みや後方参照など,現実のソフトウェアで使用されている拡張された正規表現に対しても解析が行える手法を提案する.さらに,既存の解析アルゴリズムを高速化し,より実用的な速度で解析を行える手法を提案する.そして,これらの改良を施した計算量解析のツールをScalaで実装し,Weidemanらによる既存のツールよりも多くの正規表現が解析できることを実験により確認した.
著者
逢坂 美冬 上野 雄大 大堀 淳
出版者
日本ソフトウェア科学会
雑誌
コンピュータ ソフトウェア (ISSN:02896540)
巻号頁・発行日
vol.35, no.3, pp.3_79-3_95, 2018-07-25 (Released:2018-09-25)

一般にWebアプリケーションにおけるWebページの動的生成は,テンプレートエンジンを用い,事前に用意されたテンプレートに対して動的に値を埋め込むことで行う.テンプレートはテキストファイルとして用意され,実行時に読み込まれる.そのため,テンプレートに対する操作は一般に型無しの文字列操作となる.従って,たとえホスト言語が強い型付けを持つ関数型言語であったとしても,実際のテンプレート構造とプログラムの想定の間の不整合は静的に検出されない.本論文では,動的に読み込まれるテンプレートに対して,部分動的レコードに基づく動的型検査を行うことで,型付きのテンプレート操作を実現する言語機構を提案する.この機構は,テンプレートにホール名をラベルとするMLの部分動的レコード型を与え,テンプレートに値を埋め込む操作をレコードの更新演算と同様に型付けする.テンプレートに存在しないホールへの値の埋め込みは型エラーとなる.プログラムが想定するテンプレートの型と実際のテンプレートの構造の整合性は,テンプレートファイル読み込み時に動的に検査する.本論文ではさらに,この機構をML系関数型言語SML#のコンパイラを拡張することで実装し,実例を通じて実用性を検証するとともに,実用上の課題について議論する.
著者
叢 悠悠 浅井 健一
出版者
日本ソフトウェア科学会
雑誌
コンピュータ ソフトウェア (ISSN:02896540)
巻号頁・発行日
vol.36, no.2, pp.2_47-2_60, 2019-04-26 (Released:2019-06-25)

CoqやAgdaなどの定理証明支援系では,依存型を使ってプログラムの性質を正確に記述することができる.一方,依存型付き言語の多くは,副作用を許さないという制約もつ.これは,副作用の動的な振る舞いによって型が静的に定まらなくなることによるが,副作用の欠如は実用的なプログラムの実装の妨げとなるため,適切な制約を設けながら,依存型付き言語に副作用を導入する試みがなされてきた.本研究では,限定継続命令 shift/resetをもつ依存型付き言語を考える.shift/resetはさまざまな副作用の模倣を可能にするが,その応用例や型システムは単純型付き言語で考えられてきた.本稿では,shift/reset と依存型を組み合わせるために必要な制約を明らかにし,健全な型システムを定義する.また,設計した言語に対するCPS変換を与え,変換が型を保存することを証明する.
著者
松原 克弥 髙川 雄平
出版者
日本ソフトウェア科学会
雑誌
コンピュータ ソフトウェア (ISSN:02896540)
巻号頁・発行日
vol.39, no.1, pp.1_18-1_32, 2022-01-25 (Released:2022-03-25)

コンピュータ技術進歩の過程において,基盤ソフトウェアであるオペレーティングシステム(OS)の研究開発が盛んに行われ,数多くのOS実装が利用可能となった.デスクトップPCやスマートフォン,エンタープライズサーバなどの一部のプラットフォーム向けでは,WindowsやLinuxなどの少数のOSが寡占状態にあるが,すべてのシステムにおいて特定のOSが独占して採用されることはなく,現在でも,システムの目的や用途,プラットフォームの特性などに応じて複数のOSを使い分けている.著者らは,特性の異なる複数のOSを状況の変化に応じて動的に切り替えることで,OS上で稼働するサービスの負荷耐性や性能の改善を試みる手法を提案している.本論文では,LinuxとFreeBSDを対象として,サービス稼働中にそのシステム基盤であるOSの動的な切り替えを可能とすることを目的として,FreeBSDにおけるLinux互換プロセスのマイグレーション機構の実現手法についてまとめる.Linuxにおけるプロセスマイグレーション機構の標準ツールであるCRIUとのチェックポイントデータの相互互換性を維持することで,LinuxとFreeBSD間で同一のプロセスをマイグレーションする仕組みを実現する.本実現法では,FreeBSDカーネルとLinuxカーネルのOS機能の違いだけでなく,内部構造やインタフェース仕様の違いにも着目し,CRIUの各機能と同等の機能をFreeBSD上で実現する際の課題や実装の詳細を述べる.
著者
宋 剛秀 番原 睦則 田村 直之 鍋島 英知
出版者
日本ソフトウェア科学会
雑誌
コンピュータ ソフトウェア (ISSN:02896540)
巻号頁・発行日
vol.35, no.4, pp.72-92, 2018-10-25 (Released:2018-12-26)

命題論理式の充足可能性判定(SAT)問題を解くプログラムであるSATソルバーは,2000年以降その性能面において飛躍的に進化した.それに伴い,解きたい問題をSAT符号化によりSAT問題へと変換し,SATソルバーを用いて解くSAT型システムが,プランニング,ソフトウェア・ハードウェア検証,スケジューリング問題など様々な分野で成功を収めるようになった.本稿では,まずSATソルバーの最新動向として,性能面と機能面における進化をその要因の1つであるSATソルバーの国際競技会の視点から説明を行う.次に SAT ソルバーの利用技術の視点から,SAT ソルバーの機能面の進化と符号化技術を組み合わせることで,複雑な問題を解くことが可能になることの説明を行う.そのような例として多目的最適化問題のパレート解をSATソルバーを利用して求める方法を説明する.
著者
萩原 早紀 栗原 一貴
出版者
日本ソフトウェア科学会
雑誌
コンピュータ ソフトウェア (ISSN:02896540)
巻号頁・発行日
vol.33, no.1, pp.1_52-1_62, 2016-01-26 (Released:2016-03-26)

本論文では,俗に“コミュ障”と呼ばれている人間の性質に注目し,その中で他人と視線を合わせられない症状をもつ人々を社会福祉学的な観点から支援するためのシースルー型HMD を使用したシステムの提案を行う.この“コミュ障”支援システムは,彼ら/彼女らが他人と視線を合わせられないというコミュニケーション上の問題を緩和・改善するために,顔検出技術と視覚情報提示により相手の顔を隠したり,視線をそらす癖を改善するように指示したり,視線の挙動の客観的なデータを提示したり,コミュニケーション上の危険状態が発生した場合その場から脱出する手段を与えてくれる.このシステムのプロトタイプを実装し,評価した結果,いくつかの機能は有効に働き,今後の改善点が得られた.
著者
中川 尊雄 亀井 靖高 上野 秀剛 門田 暁人 鵜林 尚靖 松本 健一
出版者
日本ソフトウェア科学会
雑誌
コンピュータ ソフトウェア (ISSN:02896540)
巻号頁・発行日
vol.33, no.2, pp.2_78-2_89, 2016-04-22 (Released:2016-06-22)

本論文は,NIRS (Near Infra-Red Spectroscopy; 近赤外分光法)による脳血流計測を用い,開発者がプログラム理解時に困難を感じているかの判別を試みた我々の先行研究(レター論文)を発展させたものである.本論文では,20名の被験者に対して,難易度の異なる三種類のプログラムの理解時の脳血流を計測する実験を行った.実験が中断された3名を除く17名中16名において,(1)難易度の高いプログラムの理解時に脳活動がより活発化するという結果(正確二項検定, p < 0.01)が得られた.また,(2)被験者アンケートによって得られた難易度の主観的評価と,脳活動値の間には有意な相関(スピアマンの順位相関係数 = 0.46, p < 0.01)がみられた.
著者
亀井 聡
出版者
日本ソフトウェア科学会
雑誌
コンピュータ ソフトウェア (ISSN:02896540)
巻号頁・発行日
vol.22, no.3, pp.3_8-3_18, 2005 (Released:2005-09-30)

インターネットにおいて,P2P (Peer-to-Peer) 技術の発展がめざましい.P2P技術は様々なメリットを持つ反面,インターネットのトラフィックの主流をこれまで占めていたウェブ等と異なる特性を持つため,ネットワークインフラに様々な影響を及ぼし始めている.本稿ではこのような現状を紹介するとともに,P2P技術とインフラの融合に向けての課題について述べる.
著者
アフェルト レナルド
出版者
日本ソフトウェア科学会
雑誌
コンピュータ ソフトウェア (ISSN:02896540)
巻号頁・発行日
vol.34, no.2, pp.2_64-2_74, 2017-04-26 (Released:2017-06-26)

コンピュータのプログラムと数学の証明の間に密な関係があることはよく知られている.1969年に発見されたCurry-Howard同型対応により,プログラムの型を言明(statement)として見れば,プログラム自体はその言明の証明として見られる.これにより,数学の証明の検査はプログラムの型付けに帰着する.この発想に基づいて,定理証明支援系という検証ツールの開発が行われてきた.近年,定理証明支援系を用いて,ようやく現実的なプログラムと証明の検証が可能となっている.現実的な証明の一例として,2005年から2012年までマイクロソフト・INRIAの共同研究組織で形式化された奇数位数定理が挙げられる.奇数位数定理は膨大な証明により示された重要な群論の定理であるため,その形式化は大きなマイルストーンとなっている.加えて,その形式化の基盤であるMathematical Componentsもまた,形式数学におけるライブラリとして重要な成果である.我々のデジタル社会を支える基本的なコンピュータプログラムであるRSA暗号や楕円曲線暗号や符号などは,整数論や群論や線形代数などの数学に基づいているが,Mathematical Componentsを用いることで,これらのプログラムの厳密な仕様の記述ができるようになった.しかし,Mathematical Componentsのような大規模なライブラリの利用には専門知識が不可欠である.本解説では,Mathematical Componentsによる形式化を紹介する.群論のラグランジュ定理を用いて,そのライブラリの基本的な使い方を説明する.
著者
鳥海 不二夫 西村 啓 浅野 千尋 石井 健一郎
出版者
日本ソフトウェア科学会
雑誌
コンピュータ ソフトウェア
巻号頁・発行日
vol.25, no.4, pp.190-198, 2008

近年市場における個人投資家の割合は増加の一途をたどっている.これにともない,アルゴリズムトレードを利用した取引が注目されている.しかしながら,投資家にとって取引エージェントの作成は障害が多く,自動取引エージェント上に優秀なアルゴリズムを実現するのは困難である.そこで,本研究では投資スキルは十分にあるもののプログラミングのスキルが十分ではない投資家に対して,その投資家の投資戦略を取引エージェント上で実現することを目指し,自動取引エージェントの作成支援システムを提案し,第一回スーパーカブロボコンテスト用で利用した.その結果,コンテスト参加者の60%が本支援システムを利用して取引エージェントを作成した.作成支援システムによって作られた自動取引エージェントは,Javaプログラミングによって作成された自動取引エージェントと比較して同程度の取引を行うことが出来ることを確認した.また,プログラミングスキルの低い投資家に対してもアルゴリズムトレードへの参加を促すことができたことを確認した.
著者
寺岡 文男
出版者
日本ソフトウェア科学会
雑誌
コンピュータ ソフトウェア (ISSN:02896540)
巻号頁・発行日
vol.28, no.2, pp.2_3-2_14, 2011-04-26 (Released:2011-06-26)

インターネットにはさまざまな新しい技術がいわば“つぎはぎ”のように追加されて発展してきた.このままではインターネットは破綻を来してしまうという危惧から,インターネットを一から設計し直そうという考え方(clean slateアプローチ)が2000年ころから出てきた.本稿ではclean slateアプローチに基づいて設計されたネットワークを“新世代ネットワーク”と呼ぶこととし,新世代ネットワークに関するいつかの研究を,(1)ネットワークアーキテクチャ,(2)ネットワーク仮想化,(3)超広帯域ネットワーク,という3つの観点から紹介する.
著者
岩間 太 中村 大賀 竹内 広宜
出版者
日本ソフトウェア科学会
雑誌
コンピュータ ソフトウェア (ISSN:02896540)
巻号頁・発行日
vol.29, no.4, pp.4_258-4_277, 2012-10-25 (Released:2012-11-25)

半形式的な記述や半構造的な自然文を含むテキスト文書のためのパーサーを形式言語/自然言語処理パーサーを組み合わて構築するためのシステムを提案する.特に,形式言語/自然言語処理パーサーを柔軟に組み合わせるためのパーサーコンビネータを設計することで,宣言的な文法記述からテキスト文書用のパーサーを作成するシステムを実現する.現状のパーサーコンビネーターは主にプログラミング言語用のパーサー構築を目的としており,自然文を含むテキスト文書のためのパーサーを構築するには不十分である.特に,既存の様々な自然言語処理パーサーは,形式言語のためのパーサーとは異なった性質をもっており,既存の枠組みでは柔軟に組合わせることが難しい.本論文では,自然言語処理パーサーと形式言語用のパーサーの組合せを可能にし,かつ,部分的なパージングや情報抽出部分の指定など,テキスト文書の処理において有用な機能を実現する演算子を含んだパーサーコンビネーターをParsing Expression Grammarsを基に設計する.また,導入したパーサーコンビネーターを用いて,宣言的な記述から,種々の自然言語処理を部分的に含むパーサーを自動生成するためのシステムを構築し,実際の適用例の一端を示す.このようなパーサーコンビネーションシステムはソフトウエア開発時に作成される文書成果物に対する解析に有用である.
著者
山本 拓朗 大山 博司 安積 卓也
出版者
日本ソフトウェア科学会
雑誌
コンピュータ ソフトウェア (ISSN:02896540)
巻号頁・発行日
vol.34, no.4, pp.4_3-4_16, 2017-10-25 (Released:2017-12-25)

The complexity and scale of embedded software have increased. To improve the productivity, the mruby on TOPPERS embedded component system (TECS) framework, which employs a scripting language (i.e., lightweight Ruby) and supports component-based development, has been proposed. In the current mruby on TECS framework, mruby programs must be compiled and linked every time they are modified, because mruby bytecode are incorporated in the platform. Moreover, while the framework supports multiple virtual machines (VMs), developers must be familiar with the functions of real-time operating systems to effectively execute multiple mruby programs concurrently or in parallel. This paper proposed an extended mruby on TECS framework that improves development efficiency more than the current framework. We implemented a Bluetooth loader receives an mruby bytecode, and a RiteVM scheduler simplifies multitasking. Synchronization of initializing multiple tasks is also implemented using an Eventflag. Experimental results demonstrate the advantages of the proposed framework.