著者

小須田 光 亀井 靖高 鵜林 尚靖

出版者

日本ソフトウェア科学会

雑誌

コンピュータ ソフトウェア (ISSN:02896540)

巻号頁・発行日

vol.32, no.4, pp.4_131-4_140, 2015

---

本論文では,ユーザによるクラッシュレポートの送信を促すために,ユーザが送信したクラッシュレポートの開発者による利用に関する知見を示す.そうすることで,開発者にとっては不具合発生状況のより正確な把握,ユーザにとっては不利益を被っている不具合の優先的な修正といった恩恵をもたらすことが期待できる.本論文では,ユーザから送信されたクラッシュレポートに対して,クラッシュレポートの送信頻度と関連付けされる割合との関係や,関連付けられているクラッシュレポートが関連付けまでに要するクラッシュレポートの送信件数に関して調査を行った. Firefoxを対象に行ったケーススタディの結果,送信されたクラッシュレポートが関連付けられている割合は約63%であることや,不具合に関連付けられているクラッシュタイプの90%は,1,000件以内のレポートが送信される間に関連付けられていることがわかった.

著者

渡辺 知恵美 森本 千佳子 中島 明日香 木塚 あゆみ

出版者

日本ソフトウェア科学会

雑誌

コンピュータ ソフトウェア (ISSN:02896540)

巻号頁・発行日

vol.32, no.2, pp.2_2-2_7, 2015-04-24 (Released:2015-06-30)

著者

朝枝 仁 松園 和久

出版者

日本ソフトウェア科学会

雑誌

コンピュータ ソフトウェア (ISSN:02896540)

巻号頁・発行日

vol.33, no.3, pp.3_3-3_15, 2016-07-25 (Released:2016-09-25)

---

「情報指向(もしくはコンテンツ指向)ネットワーク技術:Information- (Content-) Centric Networking (ICN/CCN)」は,コンテンツ名を通信の識別子として利用することで所望のコンテンツを近隣ルータなどから直接取得し,迅速かつ効率的な情報提供を可能とする新しいネットワークアーキテクチャである.本論文では,ICN/CCNの概念と特徴に加え,ICN/CCN研究のためのプロトタイプ実装やシミュレータ,テストベッドなどの紹介を行い,今後の研究指針や技術展開の可能性などを考察する.

著者

永田 章人 小林 直樹 米澤 明憲

出版者

日本ソフトウェア科学会

雑誌

日本ソフトウェア科学会大会講演論文集 日本ソフトウェア科学会第20回記念大会 (ISSN:13493515)

巻号頁・発行日

pp.7, 2003 (Released:2003-12-17)

---

型付き言語MLにおけるメモリ管理手法として,リージョン推論に基づく方式がTofteらによって提案,実装されている.この手法では,通常のMLの型システムにメモリ情報(リージョン)を付加して拡張した型システムに基づいて型推論を行うことで,各オブジェクトの生存区間を推定し,メモリの解放・獲得のためのコードをコンパイル時に挿入する.リージョンに基づくメモリ管理は,ガーベジコレクションに比べて早期にオブジェクトを解放でき,また,参照カウントによるメモリ管理方式に比べて実行時のオーバーヘッドが少ない.しかしながら,リージョン推論はMLの静的な型推論の拡張であるため,他の言語,特にSchemeのように動的に型付けされた言語に適用できるかどうかは自明でなかった.本研究では,CartwrightらのSoft typeとリージョン付き型システムとを統合することにより,動的型付き言語に対してもリージョン推論に基づくメモリ管理が行なえることを示す.

著者

大山 恵弘

出版者

日本ソフトウェア科学会

雑誌

コンピュータ ソフトウェア (ISSN:02896540)

巻号頁・発行日

vol.20, no.4, pp.375-392, 2003-07-25 (Released:2012-02-15)

著者

野田 夏子 岸 知二

出版者

日本ソフトウェア科学会

雑誌

コンピュータ ソフトウェア (ISSN:02896540)

巻号頁・発行日

vol.30, no.3, pp.3_3-3_17, 2013-07-25 (Released:2013-09-25)

---

ソフトウェアプロダクトライン開発は,ビジネス目的を共有し,また技術的にも類似性を持ったプロダクト群を全体最適の視点から体系的に開発するものである.資産の体系的な再利用が行われることから,ソフトウェアの構築の効率化を図ることができる.一方でソフトウェア開発においては構築より検証に多大なコストがかかる場合も多い.さらに,プロダクトライン開発においては資産から構築しうる膨大なプロダクトをどのように検証するのか,また資産そのものをどのように検証するのかなど,従来のソフトウェアの検証の課題に加えて特有の課題を持つ.本稿では,プロダクトライン開発において検証をどのように行えば良いのか,現時点の技術動向を紹介する.

著者

(取り下げ)

出版者

日本ソフトウェア科学会

雑誌

コンピュータ ソフトウェア (ISSN:02896540)

巻号頁・発行日

vol.35, no.1, pp.1_169-1_193, 2018-01-25 (Released:2018-02-16)

---

本記事は,著者の申し出により,取り下げました.

著者

久岡 雅也 前田 雅史 梅尾 博司

出版者

日本ソフトウェア科学会

雑誌

日本ソフトウェア科学会大会講演論文集 (ISSN:13493515)

巻号頁・発行日

vol.2003, pp.54-54, 2003

---

従来から数多くの研究がされている一斉射撃問題は, 主として1次元格子点上にセルを配列した1次元アレイを考察の対象とし, そのための同期アルゴリズムが考案されてきた. また2次元アレイに対しては, 正方形, 長方形など単純な形状を持つ2次元アレイ上では, 比較的容易に同期アルゴリズムの設計が可能であるが, 任意の形状を持つ2次元連結アレイに対しては,(1) 長方形などと同様なアルゴリズム設計が可能か?(2) 同期アルゴリズムの実現に必要な状態数は?(3) 同期に必要なステップ数は?など, 考察すべき問題が多く残されている. そこで本研究の目的は, 1次元アレイにおけるアルゴリズムを新しい埋め込み手法に基づいて設計することで, 2次元アレイ上において動作可能なセルの連結が任意の状態においても同期を実現でき, 初期状態において将軍位置が任意であることも示すことである.

著者

金城 拓実 河野 真治

出版者

日本ソフトウェア科学会

雑誌

日本ソフトウェア科学会大会講演論文集 (ISSN:13493515)

巻号頁・発行日

vol.22, pp.161-165, 2005

---

私達は家庭用ゲームマシン向けのオープンなゲーム開発環境に関する研究を行ってきた。ゲームマシンは、特殊なアーキテクチャで実現されており、ハード性能を追求するとプログラムコードは必然的にハードへの強く依存する。強い依存性のあるコードは汎用性がなく再利用は難しい。ここで私達はプログラムのtest surface を保存しながらtechnology mapping を実現する手法を提案したい。

著者

千葉 滋

出版者

日本ソフトウェア科学会

雑誌

コンピュータ ソフトウェア (ISSN:02896540)

巻号頁・発行日

vol.35, no.1, pp.1_1-1_1, 2018-01-25 (Released:2018-03-26)

著者

松崎 智広 鈴木 徹也 徳田 雄洋

出版者

日本ソフトウェア科学会

雑誌

コンピュータ ソフトウェア (ISSN:02896540)

巻号頁・発行日

vol.19, no.4, pp.266-282, 2002-07-15 (Released:2012-01-10)

---

Webアプリケーションのプログラムを作成するには,アプリケーションロジック以外にもデータ入出力,セッション管理,セキュリティ管理等のプログラムを作成する必要があり,その作成に多くの手間とWeb関連知識が必要となる.我々は,Webアプリケーションの実行をパイプ/フィルタアーキテクチャに基づくプログラムの実行とみなすことにより,Webページとアプリケーションロジックの記述からWebアプリケーションを構築する生成系PF-Webを設計し実現した.Webアプリケーションの記述にはWebページとプログラム間の値の流れを図示したWeb遷移図とフィルタの出力値を定める等式を用いる.これらの記述にはCGI等のWebの規格に関する知識は不要であり,データ入出力,セッション管理,セキュリティ管理等のプログラムは自動生成されプログラマが作成する必要はない.図を用いる全体的動作の定義と値の依存関係に基づく計算の定義によってWebアプリケーションを容易に構築できる.

著者

二木 厚吉 緒方 和博 中村 正樹 Kokichi Futatsugi Kazuhiro Ogata Masaki Nakamura 北陸先端科学技術大学院大学情報科学研究科 北陸先端科学技術大学院大学情報科学研究科 北陸先端科学技術大学院大学情報科学研究科 Graduate School of Information Science Japan Advanced Institute of Science and Technology (JAIST) Graduate School of Information Science Japan Advanced Institute of Science and Technology (JAIST) Graduate School of Information Science Japan Advanced Institute of Science and Technology (JAIST)

出版者

日本ソフトウェア科学会

雑誌

コンピュータソフトウェア = Computer software (ISSN:02896540)

巻号頁・発行日

vol.25, no.2, pp.1-13, 2008-04-24

参考文献数

6

被引用文献数

3

---

CafeOBJ言語システムを用いた形式手法,すなわち形式仕様の作成法と検証法,を全6回にわたり解説する.CafeOBJ言語はOBJ言語を拡張した代数仕様言語であり,振舞仕様,書換仕様,パラメータ化仕様などが記述できる最先端の形式仕様言語である.CafeOBJ言語システムは,等式を書換規則として実行することで等式推論を健全にシミュレートすることができ,対話型検証システムとして利用出来る.第1回の今回は,「待ち行列を用いる相互排除プロトコル」を例題として,言語や検証法の細部に立ち入ることなく,CafeOBJ仕様の作成と検証が全体としてどのように行われるかを説明する.第2回以降では,言語の構文と意味(第2回),等式推論と項書換システム(第3回)について説明し,証明譜を用いた簡約のみに基づくCafeOBJの検証法(第4回)を解説する.さらに,認証プロトコル(第5回)と通信プロトコル(第6回)の2つの典型的な検証例も示すことで検証の技法についても解説する.The formal method, or the method for writing and verifying formal specifications, with the CafeOBJ language system is described in a series of six tutorials. The CafeOBJ language is a most advanced formal specification language which extents the OBJ language, and behavioral, rewriting, and parameterized specifications can be written in it. The CafeOBJ language system can simulate equational reasoning by executing equations as rewrite rules, and be used as an interactive verification system. This first tutorial presents an overview of the CafeOBJ formal method by using an example of "mutual exclusion protocol with a waiting queue" without getting into details of the language and the verification technique. In the following tutorials, the language and its semantics (2nd tutorial), equational reasoning and term rewriting systems (3rd tutorial) are presented, and the CafeOBJ's verification method with proof scores which only uses reductions (4th tutorial) is explained. Furthermore, CafeOBJ's verifications of an authentication protocol (5th tutorial) and a communication protocol (6th tutorial) are also presented, and several verification techniques are explained.

著者

鈴木 遼 長 幾朗

出版者

日本ソフトウェア科学会

雑誌

コンピュータ ソフトウェア (ISSN:02896540)

巻号頁・発行日

vol.34, no.4, pp.4_17-4_38, 2017-10-25 (Released:2017-12-25)

---

Siv3Dは,音,画像,様々なヒューマン・インタフェース・デバイス(HID)を扱うアプリケーションを開発できるオープンソースのC++フレームワークであり,複雑なインタラクションを数行から数十行のコードで記述できる特徴を有する.既存のフレームワークよりもコーディングの労力を減らし,一方でコードの可読性を向上させるために,豊富な機能セットを提供するだけでなく,最新のC++言語規格の採用,C++標準コンテナライブラリの拡張,名前付き引数等を用いた実験的かつ進取的なC++ Application Programming Interface (API)設計がなされている.また,実行時の動作についても,非効率なコードやエラーを開発者にわかりやすく通知する仕組みが実装されている.本フレームワークは2013年から2016年までの期間において12,000ダウンロードされた実績があり,ユーザコミュニティによりドキュメント整備・サポートが継続して行われている.

著者

吉田 真也 桑原 寛明 國枝 義敏

出版者

日本ソフトウェア科学会

雑誌

コンピュータ ソフトウェア (ISSN:02896540)

巻号頁・発行日

vol.34, no.4, pp.4_47-4_53, 2017-10-25 (Released:2017-12-25)

---

本論文では,Javaプログラムに対する情報流解析のためのJavaアノテーションを提案する.情報流解析を用いることでソフトウェア内の機密情報の流出を検出できる.情報流解析では機密度束の定義とプログラム中のデータに対する機密度の指定が必要であるため,機密度の指定と機密度束の定義のためのアノテーションを定義する.アノテーションで機密度が指定されたJavaプログラムに対する情報流解析をOpenJDKのJavaコンパイラを拡張して実装し,適用例を示す.

著者

土屋 達弘

出版者

日本ソフトウェア科学会

雑誌

コンピュータ ソフトウェア (ISSN:02896540)

巻号頁・発行日

vol.29, no.1, pp.1_19-1_29, 2012-01-26 (Released:2012-03-26)

---

本解説記事では,論理式の充足可能性判定を利用したモデル検査について説明する.モデル検査とは,アルゴリズムやシステムの設計に対して,その状態空間を探索することで,与えられた性質が満たされるかどうかを判定する自動検証手法である.近年高速化が著しい充足可能性判定ツール(SATソルバやSMTソルバ)を用いることで,高速な検証が実現できる.本稿では,まずモデル検査や充足可能性判定について概説した後,プログラムのソースコードをモデル検査する手法について説明する.次に,より一般的なシステム記述を検証対象とした場合について,有界モデル検査と呼ばれる手法を紹介する.これは,初期状態からの有限の決められた回数の遷移による動作について検証を行う手法である.更に,この制約を取り除き,システムの全動作を対象とした検証を実現する手法について説明する.

著者

鷲崎 弘宜 中川 知基 斉藤 勇樹 深澤 良彰

出版者

日本ソフトウェア科学会

雑誌

日本ソフトウェア科学会大会講演論文集 (ISSN:13493515)

巻号頁・発行日

vol.21, pp.7-7, 2004

---

リモートコンポーネントを組み合わせて得られるコンポーネントベースシステムは、長期の運用を実現するために高い保守性を持つことが望ましい。保守性の判定法として、複雑度の測定がある。従来の測定法は、オブジェクト指向クラス集合、もしくは、一般的な抽象化によって得られる構造を測定対象とし、コンポーネントを単位とした保守作業の容易さを適切に反映しない。本稿では、リモートコンポーネントの特徴を考慮してコンポーネントベースシステムを段階的に抽象化し、得られる構造に対して要素間の関連に基づく複雑度を測定する手法を提案する。複数のEJBアプリケーションについて測定実験を行った結果、得られる複雑度が保守性を適切に反映することを確認した。

著者

中村 裕美 宮下 芳明

出版者

日本ソフトウェア科学会

雑誌

コンピュータ ソフトウェア (ISSN:02896540)

巻号頁・発行日

vol.33, no.2, pp.2_43-2_55, 2016-04-22 (Released:2016-06-22)

---

本論文では,電気味覚を用いて味覚情報を提示するソフトウェアやハードウェアを構築する際に参考となる生理学的知見を紹介する.味覚メディアの構築には,化学物質の受容に関する知見,他感覚が味覚に与える感覚間相互作用に関する知見が活用されているが,近年電気刺激によっておこる電気味覚も用いられつつある.電気味覚を活用した味覚メディアの構築を進めるためには,インタラクティブシステムの構造設計や刺激のデザインの参考となる知見を,生理学分野で250年超にわたり蓄積された研究群から効率的に探し出し,取り入れる必要がある.そこで本論文では,電気味覚の機序や他感覚との比較例を紹介した上で,刺激の制御とシステム構成を軸に工学的応用の助けとなる生理学的知見を紹介する.そして,工学分野における電気味覚メディアの方向性について議論する.

著者

香川 考司 Koji Kagawa 京都大学数理解析研究所 Research Institute for Mathematical Sciences Kyoto University.

出版者

日本ソフトウェア科学会

雑誌

コンピュータソフトウェア = Computer software (ISSN:02896540)

巻号頁・発行日

vol.11, no.5, pp.377-386, 1994-09-16

参考文献数

18

---

破壊的代入,入出力などの副作用を関数型言語で模倣するプログラムを書く際に,副作用をmonadというある種の条件を満たす型構成子として表現すると,プログラムの可読性,変更のしやすさなどが増すことがわかってきている.しかし,従来では代表的な副作用である"状態"を扱う場合に,1つの(平板な)構造しか状態として扱うことができず,関数型言語の特徴の1つである,組やリストなどの階層的データをその構造を生かして状態として扱うことは難しかった.その結果,状態を扱うプログラムをこれらのデータ型を介して部品化することができないため,あるデータ型の状態を対象として書かれたプログラムの部品を,他のデータ型を状態として持つ場合に再利用することが難しく,関数型言語にmonadを導入する動機の1つである命令的プログラムの書換え,再利用の容易性が達成されたとはいい難かった.例えば,配列を2つ以上扱いたい時に,どのように配列を1つだけ扱うプログラムの部品を再利用してプログラムを書けばいいのか,その方法がわからなかった.この論文では,階層的なデータ型の中の構成要素の"位置"をmonad morphismとして表現し,その位置にあるデータを局所的状態として扱うことにより,複合的,階層的なデータをその構造に自然な形で状態として扱う方法を提案する.その結果,プログラムの部品化を容易に行なうことができるようになる.結果としてのプログラミングのスタイルは,オブジェクト指向プログラミングを思い起こさせるものとなる.ここでは,オブジェクト指向との対応についても述べる.

著者

飛世 速光 竹川 佳成 寺田 努 塚本 昌彦

出版者

日本ソフトウェア科学会

雑誌

コンピュータ ソフトウェア (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インデックスを採用した.