著者
堀内 公平
出版者
Japan Society for Software Science and Technology
雑誌
コンピュータ ソフトウェア (ISSN:02896540)
巻号頁・発行日
vol.29, no.2, pp.2_158-2_167, 2012

本研究では複数ベンダのクラウドを用いて構成する高速で高信頼な分散ストレージMyCloudを提案する.従来のクラウドコンピューティングでは,単一のクラウドベンダに依存することによる,転送遅延問題,可用性問題,プライバシー問題が指摘されている.これらの問題を解決するため,本研究では次の3点を実現した.(1)高速性: 並列分散処理によりダウンロード速度を9倍程度高速化した.(2)高可用性: データを冗長化して分散し,システムの一部であるクラウドサービスが一定数以下停止しても,継続して利用できるシステムを構成した.(3)強秘匿性: 暗号化と分散配置により,クラウドからデータが漏洩,あるいはベンダがユーザのデータを無断利用しようとしても,有為な情報を読み取れないシステムを実現した.
著者
山下 義行 佐々 政孝 中田 育男 Yoshiyuki Yamashita Masataka Sassa Ikuo Nakata 筑波大学電子情報工学系 筑波大学電子情報工学系 筑波大学電子情報工学系
雑誌
コンピュータソフトウェア = Computer software (ISSN:02896540)
巻号頁・発行日
vol.4, no.3, pp.212-224, 1987-07-15

「なかよしグループ問題」は,ある条件下での集合の彩色問題を一般化し,より親しみやすい表現に直したものである.この問題ではなかよしグループの子供達に最適な色のキャンディを配ることを考えるが,配色に関する制約条件,局所的な最適条件および大局的な最適条件が絡みあい,必ずしも簡単には解けない.そこで,なかよしグループの中からキーとなる子供達を見つけ出し,その子らについて彩色問題を解くだけで総ての子供達への配色が決まる,という一般的な解法を提案する.応用として,ECLR属性文法に基づくコンパイラ生成系Rieの属性スタック自動割り当てプログラムを作成し,PL/0,Pascalサブセットコンパイラについて最適な割り当てを行った.
著者
飛世 速光 竹川 佳成 寺田 努 塚本 昌彦
出版者
日本ソフトウェア科学会
雑誌
コンピュータ ソフトウェア (ISSN:02896540)
巻号頁・発行日
vol.31, no.2, pp.2_57-2_66, 2014-04-24 (Released:2014-06-24)

ギター演奏において運指(指使い)は演奏に影響する重要な要素である.また,触弦(指が弦に触れている状態)や押弦,離弦(指と弦が離れている状態)といった状態や,複数の指が1本の弦上にあるなど,左手の指と弦との関係は多彩である.これらの情報を演奏支援システムが取得することで,ミュート(触弦により弦の振動を防ぎ消音すること)のために弦上に配置された指や,次の発音の準備のために弦上に配置されている指など,発音に関わらない運指情報を判別でき,効率的な独習支援や,細かい演奏技術が盛り込まれた楽譜の自動生成に応用できる.そこで本研究では,押弦,触弦,離弦を認識可能な,ギターのための触弦認識システムの構築を目的とする.本研究では弦やフレットの導電性に着目した電気的な機構による触弦認識手法を新たに提案する.また,実装したプロトタイプを用いて,システムの認識率を調査する実験を行い,高精度に触弦認識できることを確認した.さらに,本研究の枠組みを利用したアプリケーションを提案した.
著者
水野 雅之 住井 英二郎
出版者
日本ソフトウェア科学会
雑誌
コンピュータ ソフトウェア (ISSN:02896540)
巻号頁・発行日
vol.34, no.2, pp.2_114-2_119, 2017-04-26 (Released:2017-05-11)

コンパイラの形式的検証は盛んに研究されているが,入出力等の副作用がある高階関数型プログラミング言語のコンパイラの検証はあまり行われていない.これは無限に入出力を行うプログラムの意味論の形式化が自明でないためである.我々は,入出力等の副作用を持つ外部関数の呼び出しや再帰関数,高階関数,組を持つ値呼びの関数型プログラミング言語に対するK正規化を定理証明支援系Coqを用いて形式的に検証した.K正規化とはlet式を用いて全ての中間式に対し陽に名前を与えるプログラム変換であり,束縛の操作を伴う点で形式化が自明でない.本研究では,余帰納的大ステップ操作的意味論によりプログラムの意味を外部関数呼び出しの無限列として与えた.また,束縛の表現としては,他の手法と比較検討した上でde Bruijnインデックスを採用した.
著者
沢田 篤史 野呂 昌満
出版者
日本ソフトウェア科学会
雑誌
コンピュータ ソフトウェア (ISSN:02896540)
巻号頁・発行日
vol.32, no.1, pp.1_35-1_46, 2015

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

近年の人工知能分野においては,記号データ中に存在する不確実性をどう扱うかが大きな課題となっている.不確実性を扱うためには,まず確率モデルを構築し,その上で確率推論を行う方法が考えられる.更に近年では,記号列データや関係データベースなど,従来の単一の表データとしては表現できない,構造をもつデータの重要性が増しており,それらを扱うための一般的手法として,一階述語論理と確率の統合を目指す枠組みが数多く提案されている.その中の1つに確率論理プログラミング処理系PRISMがあるが,PRISMは宣言的な意味論,論理プログラムの高い記述力,効率的な組み込みの確率推論機構を備えており,確率モデリングに要する労力を大幅に省くことが期待される.本論文ではPRISM処理系のツールとしての側面に注目し,PRISMプログラムの記述例,処理系が提供する機能,処理速度に関するベンチマーク評価について述べる.
著者
上野 乃毅
出版者
Japan Society for Software Science and Technology
雑誌
コンピュータソフトウェア (ISSN:02896540)
巻号頁・発行日
vol.26, no.4, pp.30-38, 2009-10-27

ソフトウェアへの機能追加のために実装の大規模な刷新が必要になることがある.実装刷新において後方互換性を完全に保つのは難しく,作業の途中で頓挫する例が後を断たない.実装刷新に失敗すると,開発プロジェクトでは巻き戻しの作業が発生するだけでなく,実装刷新を担当した開発者がモチベーションを欠き,長期的な生産性低下に繋がる恐れがある.本論文では,オープンソース開発における実装刷新の失敗事例を調査し,共通の要因とその対処法を明らかにした.調査の有効性を示すために,世界中に膨大な数のユーザを抱えるソフトウェアGNU Emacsの暗号化サブシステム(約4500行)に関して,提案手法に従って刷新を行なったところ,作業を円滑に完遂できた.
著者
森川 知哉 荒堀 喜貴 権藤 克彦
出版者
日本ソフトウェア科学会
雑誌
コンピュータ ソフトウェア (ISSN:02896540)
巻号頁・発行日
vol.31, no.1, pp.1_103-1_109, 2014-01-27 (Released:2014-03-03)

未定義動作を伴う整数オーバーフロー(時限爆弾)は重大な脆弱性の原因となる.本論文では時限爆弾を軽量に効率よく検出する手法として6つの固定的な整数値(整数境界値)を使う方法を提案し,19のオープンソースに適用して定量的に評価した.その結果,整数境界値は従来のランダム法に比べて,平均で36.7%多くの時限爆弾を検出した.さらに,整数演算の未定義動作のうち,比較・ビット演算が61.3%を占めることと,比較・ビット演算とその他の演算での,整数境界値による時限爆弾の検出率には有意差がないという結果を得た.
著者
泉田 大宗 森 彰 二木 厚吉
出版者
日本ソフトウェア科学会
雑誌
コンピュータ ソフトウェア (ISSN:02896540)
巻号頁・発行日
vol.29, no.4, pp.4_199-4_218, 2012-10-25 (Released:2012-11-25)

本稿では動的解析と静的解析を組み合わせたマルウェアの振る舞い解析手法について述べる.静的解析部ではバイナリコードを低レベルの記号式で解釈した上で静的単一代入形式に変換し,後方解析を行うことで間接ジャンプの行き先を可能な限り解決している.静的解析では解析しきれない制御フローに関しては動的解析によって補遺する.従来のバイナリコード解析手法ではC言語などの高級言語からコンパイルされたバイナリのみを対象としていたが,本手法ではマルウェアのようにそのような前提条件を満たさないバイナリも解析可能である.また,動的解析部としてハイパーバイザ機構を使った仮想環境を用いる試みについても述べる.
著者
片山 卓也
出版者
日本ソフトウェア科学会
雑誌
コンピュータ ソフトウェア (ISSN:02896540)
巻号頁・発行日
vol.29, no.4, pp.4_32-4_39, 2012-10-25 (Released:2012-12-25)

長年にわたるソフトウェア進化の研究や実務経験にもかかわらず,ソフトウェアを適切に進化させることは容易ではなく,多くのシステムが進化作業の直後に障害を起こしている.この原因がどこにあるかをソフトウェア進化の基本に立ち戻って考え,なぜ進化は困難であるのか,それを克服するための技術課題はなにかを考えた.システムの開発に使われたプロセスの再実行という考えが,進化を考える上で基本的であることに着目し,プロセス主導進化の概念を提案し,これに基づいて進化のあり方や技術チャレンジについて述べた.
著者
岩間 太 立石 孝彰
出版者
日本ソフトウェア科学会
雑誌
コンピュータ ソフトウェア (ISSN:02896540)
巻号頁・発行日
vol.32, no.2, pp.2_114-2_127, 2015-04-24 (Released:2015-06-30)

単体テスト時に利用する入力テストデータをCOBOLソースコードから生成するためのCOBOL記号実行器を構築した. この記号実行器の特徴はbit-vector logicに基づいてメモリ内バイトデータの記号値を扱うという点でありこれにより,バイトデータを直接操作するコードのテストデータ生成が可能になる.このような記号実行器によるテストデータ生成ツールはデータ表現の違いなどによる不具合が生じることの多いマイグレーションプロジェクト等において有用なものとなる.
著者
田村 直之 丹生 智也 番原 睦則
出版者
日本ソフトウェア科学会
雑誌
コンピュータ ソフトウェア (ISSN:02896540)
巻号頁・発行日
vol.27, no.4, pp.4_183-4_196, 2010-10-26 (Released:2010-12-26)

本論文では,SAT変換に基づく制約ソルバーであるSugarの概要とその性能評価結果について述べる.Sugarは,制約充足問題(CSP),制約最適化問題(COP)および最大制約充足問題(Max-CSP)を,命題論理の充足可能性判定問題(SAT問題) に変換し,MiniSat等の高速なSATソルバーを用いて求解を行うシステムである.SAT変換には,order encodingと名付けた新しい方法を用いており,従来広く用いられているdirect encodingやsupport encodingよりも,多くの問題に対して高速な求解が可能である.本論文では,order encodingの説明を含めたSugarの概要について述べた後,2008年に開催された第3回国際CSPソルバー競技会およびMax-CSPソルバー競技会での結果を基にSugarの性能評価結果を報告する.なお,Sugarは同競技会の10部門のうち4部門で第1位となった.
著者
阪上 紗里 浅井 健一
出版者
Japan Society for Software Science and Technology
雑誌
コンピュータソフトウェア (ISSN:02896540)
巻号頁・発行日
vol.26, no.2, pp.3-17, 2009-04-24

「プログラムの残りの計算」を表す継続を扱う為の基礎言語体系として,対称λ計算(Symmetric λ-calculus, SLC)がFilinskiによって提案されている.SLCにおいては項と継続が完全に対称な形をしており,項を扱うのと同じように継続を扱うことができる.そのため,項と継続を統一的に議論するのに適していると思われるが,これまでSLCについての研究はほとんどなされていない.ここでは,まずSLCをsmall step semanticsで定式化し直し,型付き言語の基本的な性質であるProgressとPreservationを満たすことを証明する.次に,SLCが継続計算を議論・表現するのに適していることを示すため,(1) FelleisenのCオペレータを含むcall-by-value言語,Λ<SUB>C</SUB>計算,および(2) Parigotのcall-by-name λμ計算が,どちらも自然にSLCに変換できることを示す.近年call-by-valueとcall-by-nameの双対性が項と継続の対称性と絡めて注目されているが,ここでの結果はそれに対する洞察を与えるものと期待される.