著者

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

出版者

日本ソフトウェア科学会

雑誌

コンピュータ ソフトウェア (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研究のためのプロトタイプ実装やシミュレータ,テストベッドなどの紹介を行い,今後の研究指針や技術展開の可能性などを考察する.

著者

阿部 洋丈 Hirotaka Abe 科学技術振興機構 CREST JST CREST

雑誌

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

巻号頁・発行日

vol.23, no.1, pp.1-14, 2006-01-26

---

本稿では,近年注目を集めているPeer-to-Peer型分散システムを構築するための基盤技術,分散ハッシュテーブル(Distributed Hash Tablel; DHT)についての入門的な解説を行う.分散ハッシュテーブル技術は,システム全体を管理する中央サーバを持たないようなPeer-to-Peerシステム(pure Peer-to-Peerシステム)において,効率的なオブジェクト発見の実現を可能にする.

著者

大山 恵弘

出版者

日本ソフトウェア科学会

雑誌

コンピュータ ソフトウェア (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)

---

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

著者

溝口 文雄 Fumio Mizoguchi 東京理科大学理工学部経営工学科

雑誌

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

巻号頁・発行日

vol.2, no.3, pp.539-542, 1985-07-15

著者

岩崎 英哉 Hideya Iwasaki 東京大学大学院工学系研究科情報工学 Department of Information Engineering Mathemaical Engineering University of Tokyo

雑誌

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

巻号頁・発行日

vol.15, no.6, pp.547-560, 1998-11-16

著者

千葉 滋

出版者

日本ソフトウェア科学会

雑誌

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

巻号頁・発行日

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

著者

新屋 良磨

出版者

日本ソフトウェア科学会 ; 1984-

雑誌

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

巻号頁・発行日

vol.35, no.1, pp.82-85, 2018-02

著者

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

出版者

日本ソフトウェア科学会

雑誌

コンピュータ ソフトウェア (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:02896540)

巻号頁・発行日

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

---

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

著者

河原 英紀

出版者

Japan Society for Software Science and Technology

雑誌

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

巻号頁・発行日

vol.32, no.3, pp.3_23-3_28, 2015

著者

五十嵐 悠紀 五十嵐 健夫 鈴木 宏正 Yuki Igarashi Takeo Igarashi Hiromasa Suzuki 東京大学大学院工学系研究科 東京大学大学院情報理工学系研究科:JST ERATO 東京大学大学院工学系研究科 Dept. of Engineering The University of Tokyo Dept. of Information Science and Technology The University of Tokyo:JST ERATO Dept. of Engineering The University of Tokyo

雑誌

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

巻号頁・発行日

vol.26, no.1, pp.51-58, 2009-01-27

---

"あみぐるみ"は毛糸を使って作るぬいぐるみであるが,毛糸の編み方によって形状をデザインしていくため,初心者にはデザインすることが困難である.我々は3次元モデリングプロセスにインタラクティブな物理シミュレーションを組み合わせることであみぐるみを効率的にデザインできるモデラーを作成した.本システムは自動で編み目を計算してあみぐるみモデルをシミュレーション結果として提示するため,初心者にでも直感的にデザインでき,編み図も容易に得ることができる.また,初めてあみぐるみに挑戦する初心者でも製作手順を容易に理解できるようにするために,製作手順を視覚的に提示する製作支援インタフェースも備えた.あみぐるみ初心者でも容易にオリジナルなあみぐるみを作成できることを確認したので報告する.

著者

香川 考司 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として表現し,その位置にあるデータを局所的状態として扱うことにより,複合的,階層的なデータをその構造に自然な形で状態として扱う方法を提案する.その結果,プログラムの部品化を容易に行なうことができるようになる.結果としてのプログラミングのスタイルは,オブジェクト指向プログラミングを思い起こさせるものとなる.ここでは,オブジェクト指向との対応についても述べる.