著者

グリュック ロバート 横山 哲郎

出版者

日本ソフトウェア科学会

雑誌

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

巻号頁・発行日

vol.33, no.3, pp.3_108-3_128, 2016-07-25 (Released:2016-08-10)

---

A linear-time reversible self-interpreter in an r-Turing complete reversible imperative language is presented. The proposed imperative language has reversible structured control flow operators and symbolic tree-structured data (S-expressions). The latter data structures are dynamically allocated and enable reversible simulation of programs of arbitrary size and space consumption. As self-interpreters are used to show a number of fundamental properties in classic computability and complexity theory, the present study of an efficient reversible self-interpreter is intended as a basis for future work on reversible computability and complexity theory as well as programming language theory for reversible computing. Although the proposed reversible interpreter consumes superlinear space, the restriction of the number of variables in the source language leads to linear-time reversible simulation.

著者

椎尾 一郎 浜田 玲子 美馬 のゆり

出版者

日本ソフトウェア科学会

雑誌

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

巻号頁・発行日

vol.23, no.4, pp.4_36-4_46, 2006 (Released:2007-06-11)

被引用文献数

2

---

キッチンは生産の場であり,調理を媒介とした教育とコミュニケーションの場でもある.このため,家庭環境の中でも,実用的なユビキタスコンピュータアプリケーションの可能性が高い場所と考えられる.そこで筆者らは,コンピュータ,ネットワーク,センサを組み込んだ未来のキッチン,Kitchen of the Futureを開発している.このコンピュータ強化されたキッチンにより,単に調理の効率を向上させるだけではなく,キッチンを学びとコミュニケーションの場として復活させることができると考えている.本論文では,Kitchen of the Futureを利用して実装した,調理の記録とネットワークでの公開と共有,調理過程の再生,遠隔地キッチンを接続しての調理支援,調理教材の効果的な提示を実現するアプリケーションについて報告する.

著者

鍋島 英知 岩沼 宏治 井上 克巳

出版者

日本ソフトウェア科学会

雑誌

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

巻号頁・発行日

vol.29, no.4, pp.4_146-4_160, 2012-10-25 (Released:2012-11-25)

---

命題論理の充足可能性判定問題(SAT問題)を解くソルバーは,その飛躍的な性能向上に伴い,システム検証やプランニング・スケジューリング問題,制約充足・最適化問題等の様々な分野において活躍している.GlueMiniSat 2.2.5は,単位伝搬を促し矛盾の発生を促進する学習節を積極的に獲得する戦略に基づくSATソルバーである.学習節の評価尺度には,AudemardとSimonが開発したSATソルバーGlucoseで導入されたリテラルブロック距離を改良した尺度を用い,単位伝搬を促進する学習節を獲得・保持する.また良い学習節の獲得を促すため,非常に積極的なリスタート戦略を採る.我々は代表的SATソルバーであるMiniSat 2.2を基にこれらの手法を実装し,GlueMiniSat 2.2.5を開発した.GlueMiniSat 2.2.5は充足不能性の証明に強く,SAT 2011競技会のApplication部門において逐次型ソルバーとしてUNSATクラスで1位,SAT+UNSATクラスで2位を獲得している.また並列型ソルバーを含めても同部門UNSATクラスで2位を獲得している.

著者

小田 朋宏 荒木 啓二郎

出版者

日本ソフトウェア科学会

雑誌

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

巻号頁・発行日

vol.34, no.4, pp.4_129-4_143, 2017-10-25 (Released:2017-11-03)

---

ソフトウェアシステムの開発において仕様記述は重要な工程であり,仕様記述の曖昧さや誤りは開発全体の生産性および信頼性に重大な影響を与えることが知られている.形式仕様を記述することはモデリングの一種であり,数学的な裏付けのある道具立てによって適切な抽象度でシステムの機能を厳密に定義する工程である.厳密で適切な抽象度の仕様記述を得るために,形式仕様記述者は仕様記述の初期段階において問題領域を探索し対象ドメインの知識獲得や要求項目への理解を深めながらモデリングを進める.本論文では,探索的なモデリングを支援するためのツールに求められる性質を示した上で,形式仕様記述言語VDM-SLによる探索的モデリングを支援する統合開発環境ViennaTalkのデザイン指針,設計および実装を示す.

著者

和田 英一

出版者

日本ソフトウェア科学会

雑誌

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

巻号頁・発行日

vol.2, no.4, pp.4_632-4_639, 1985-10-15 (Released:2018-11-05)

著者

松田 一孝 胡 振江 中野 圭介 浜名 誠 武市 正人

出版者

日本ソフトウェア科学会

雑誌

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

巻号頁・発行日

vol.26, no.2, pp.2_56-2_75, 2009-04-24 (Released:2009-06-24)

---

双方向変換は,元のデータの一部を抽出し加工する順方向変換と,順方向変換で得られたデータに対する変更を元データに書き戻す逆方向変換の二つの変換から構成される.双方向変換を用いることで,XML文書の同期や相互変換を行える.さらには,双方向変換はプレゼンテーション指向の文書作成やソフトウェアエンジニアリングにも利用できる.著者らは2007年に,順方向変換を記述するプログラムが与えられたときに自動的に逆方向変換を得る系統的な手法を提案した.しかし,そこで扱われている順方向のプログラムは制限が強く,制限の一つとして変数を二度以上使用することが禁止されていたため,複製を含む変換は記述できなかった.そこで本論文では,前手法を拡張し,複製を含むプログラムにおいても自動的に逆方向変換を得る手法を提案する.

著者

今井 健男 酒井 政裕 萩谷 昌己

出版者

日本ソフトウェア科学会

雑誌

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

巻号頁・発行日

vol.30, no.2, pp.2_207-2_226, 2013-04-25 (Released:2013-08-25)

---

本稿では,プログラムの事前条件推定を行う新たな手法を提案する.本手法では,プログラムのテキストから生成した述語の集合とプログラムに相当する論理式,および事後条件の否定の連言を作り,そのMinimal Unsatisfiable Core(MUC)から事前条件を求める.MUCは一般的に複数存在するが,本手法ではまずMUCを列挙し,その中から事前条件として適格で,かつ最も弱い条件を選択する.こうして得られる事前条件は理想的な最弱条件ではないが,与えられた述語群の組み合わせの中で最も弱いという点で,我々はこれを「準最弱」な事前条件と呼ぶ.我々は,C言語向け有界検査ツールCForgeを援用し,上記手法を実現するツールSMUCEを試作した.その上で,教科書的なアルゴリズムを実装するC言語関数9個に,2種類の事後条件と共に適用し,人手で求めた事前条件との比較による評価を行った.結果,延べ18個中10個において,人手で求めた事前条件と同等か,より弱い条件が推定され,提案手法が原理上,実用的な事前条件を推定できることが確認できた.

著者

近藤 正夫

出版者

日本ソフトウェア科学会

雑誌

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

巻号頁・発行日

vol.2, no.4, pp.4_640-4_642, 1985

---

<p></p>

著者

上嶋 祐紀 住井 英二郎

出版者

日本ソフトウェア科学会

雑誌

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

巻号頁・発行日

vol.26, no.1, pp.1_139-1_154, 2009-01-27 (Released:2009-03-27)

---

C言語サブセットのプログラムを安全なJava言語のプログラムに変換する方式を実装した.そのような変換のためには,C言語独特の操作であるポインタ演算を,Javaプログラムで安全に模倣する必要がある.これを実現するために,まずC言語のポインタやメモリブロックを表現するJavaのクラスを定義した.次に,これらのクラスを利用するようなJavaへの変換規則を定め,規則に従ってトランスレータを実装した.また,C言語ではポインタと整数を相互にキャストすることが可能なので,整数もポインタと同様のオブジェクトに変換しなければならない.しかし,すべての整数をポインタと同様に表現すると大幅に効率が悪化する.そこで,データフロー解析により,ポインタが代入されない基本型の変数は,Javaの通常の基本型変数に変換する,などの最適化を実装した.9個のベンチマークプログラムで実験したところ,最適化前の変換結果コードは元のCプログラムに対し3.3倍~585倍程度の実行時間がかかったが,最適化後は(元のCプログラムに対し)1.3倍~5.9倍程度に改善した.

著者

高田 崚介 志築 文太郎 高橋 伸

出版者

日本ソフトウェア科学会

雑誌

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

巻号頁・発行日

vol.35, no.3, pp.3_45-3_56, 2018-07-25 (Released:2018-09-25)

---

データグローブを構築するための,導電繊維が編み込まれた手袋を用いて手形状を認識する手法を示す.提案手法は,手形状として指の曲げおよび指同士の接触を推定する.指の曲げ推定には,指を曲げた際に手袋表面の導電繊維同士が短絡することによって電気抵抗が減少する現象を用いる.また,指同士の接触推定には,各指ごとに異なる周波数の交流信号を印加し,指同士が接触した際に信号が伝搬する現象を用いる.我々は実験により,指の関節の角度と導電繊維の抵抗値の関係を明らかにした.さらに導電繊維の抵抗値と曲げセンサの抵抗値を比較した.また,それぞれ異なる周波数の交流信号を印加した人指し指–小指のどの指骨に親指が接触したかを機械学習を用いて推定し,実験により触れた位置の推定精度が80.5%であることを明らかにした.さらに電源的に独立した手袋同士の接触についても検証し,信号が伝搬されることを確認した.

著者

大田 昌幸 杉本 周 福田 健介 廣津 登志夫 明石 修 菅原 俊治

出版者

日本ソフトウェア科学会

雑誌

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

巻号頁・発行日

vol.28, no.2, pp.2_129-2_139, 2011-04-26 (Released:2011-05-26)

---

本稿では,インターネット上の小規模な観測アドレス空間(Darknet)を用いて,その近隣のアドレス空間へ到着する異常パケットの振る舞いを推定できる可能性を示す.我々はこれまで,各組織の断片的未使用アドレス空間に到着する異常パケットの振る舞いを観測することで,近隣のアドレス空間に到着する異常パケットを推定・防御する分散協調監視アーキテクチャを提案してきた.異常パケットの振る舞いを推定するには,小規模な観測アドレス空間とその近隣へ到着する異常パケット間の時系列相関強度を調査する必要がある.そこで,アドレス空間をスキャンする異常パケットを対象に,Darknetの観測空間を小規模なサブ観測空間に分け,そのサブ観測空間の間の時系列解析から相関強度を求めた.さらに,サブ観測空間のサイズを変更させ,その相関強度のサイズ依存性を調査した.その結果,十分小さなサブ観測空間でも,近隣へ到着する異常パケットの振る舞いを推定できることが分かった.また,特定の観測位置をベースとした解析を行うことで非常に高い相関強度を得られた.これらの結果から,小規模な観測空間を用いる分散協調監視アーキテクチャでも異常パケットの振る舞いを推定できる可能性が示せた.

著者

佐藤 洸一 菊池 健太郎 青戸 等人 外山 芳人

出版者

日本ソフトウェア科学会

雑誌

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

巻号頁・発行日

vol.32, no.1, pp.1_179-1_193, 2015

---

項書き換えシステム上の帰納的定理の自動証明手法として書き換え帰納法(Reddy, 1989)が提案されている.しかし,書き換え帰納法は末尾再帰による関数定義が含まれると有効に働かない場合が多い.一方,プログラムの自動検証を容易にすることを目的としたプログラム変換法として,文脈移動法および文脈分割法(Giesl, 2000)が提案されている.これらの手法は,末尾再帰プログラムを自動検証に適した単純再帰プログラムへと変換する.本論文では,項書き換えシステムに対する文脈移動法・文脈分割法の正当性を証明し,それらが書き換え帰納法による帰納的定理の証明に有効であることを明らかにする.

著者

倉橋 節也

出版者

日本ソフトウェア科学会

雑誌

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

巻号頁・発行日

vol.25, no.4, pp.252-260, 2008

---

本研究では,中国の家系記録「族譜」をもとに,科挙合格者を多く輩出したひとつの家系を約500年に渡ってエージェント技術を用いて分析を行った.家系ネットワークと個人のプロファイルデータをそれぞれ隣接行列と属性行列として表現し,実プロファイルデータを目的関数とする,マルチエージェントモデルによる逆シミュレーションを実施した.その結果,家庭内において子供への文化資本の伝達には,祖父と母が大きな影響を持つことがわかり,家族が維持する規範システムの一部を発見できた.本モデルによって,逆シミュレーション手法を用いたエージェントベースモデルが歴史学や人類学の分野において,新たな知識の発見に貢献できることを示した.

著者

小川 祐樹 山本 仁志

出版者

日本ソフトウェア科学会

雑誌

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

巻号頁・発行日

vol.31, no.3, pp.3_178-3_186, 2014-07-25 (Released:2014-09-10)

---

本研究では,人は身近な近接他者や集団の多数派から影響をうけるという関連研究をふまえ,Axelrodのシミュレーションモデルを拡張し,集団の集約情報と相互作用するモデルを導入した.そして提案モデルをもとにシミュレーションを行うことで,集約情報が社会における意見や嗜好の分布多様性に与える影響を検討した.シミュレーションの結果,集約情報は文化種類の多様性の維持において有効であるが,集約情報の範囲によってその効果に違いがみられることがわかった.具体的には,局所的・中域的・大域的の異なる範囲における集約情報の効果を分析し,中域的範囲の集約情報が,文化の多様性を維持するうえで有用であることがわかった.

著者

磯部 祥尚 ローゲンバッハ マーカス

出版者

日本ソフトウェア科学会

雑誌

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

巻号頁・発行日

vol.25, no.4, pp.85-92, 2008

著者

石川 拓也 本田 晋也 高田 広章

出版者

日本ソフトウェア科学会

雑誌

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

巻号頁・発行日

vol.29, no.4, pp.4_161-4_181, 2012-10-25 (Released:2012-11-25)

---

近年,組込みリアルタイムシステムにおいてもメモリ保護機能が重要となっており,メモリプロテクションユニット(MPU)という,メモリ保護機能の実現をサポートするハードウェアを搭載したプロセッサが存在する.MPUを用いる場合,同じアクセス権を設定する必要のあるコードやデータを連続した番地に配置するように,静的にメモリ配置を行う必要がある.本論文では,メモリ保護機能を持ったリアルタイムOSとして開発した,TOPPERS/HRP2カーネル(HRP2)について述べる.HRP2カーネルは,MPUによるメモリ保護をサポートできるように,静的コンフィギュレーション時において,メモリ配置を静的に行い,同じアクセス権を設定する必要のあるコードやデータを連続して配置する.そして,メモリ保護属性の異なるコンテキストへ切り替わるとき,同時にMPUの設定情報を書き換えることによって,MPUを用いたメモリ保護機能を実現している.HRP2において,メモリ保護機能を持つことによって生じるオーバヘッドを,メモリ保護機能を持たないリアルタイムOSと比較することで評価した.

著者

福田 健介

出版者

日本ソフトウェア科学会

雑誌

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

巻号頁・発行日

vol.30, no.2, pp.2_23-2_32, 2013-04-25 (Released:2013-08-25)

---

本論文ではインターネットバックボーンにおける異常トラフィックについて説明し,それらを効率良く検出するための種々の異常検出アルゴリズムを紹介する.さらに,公開されている10年にわたる国際線バックボーントラフィックデータに対して,複数の異常検出アルゴリズムを適用した結果をもとにバックボーントラフィックにおける異常の振る舞いについて説明する.

著者

中島 浩

出版者

日本ソフトウェア科学会

雑誌

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

巻号頁・発行日

vol.25, no.3, pp.3_43-3_48, 2008-07-25 (Released:2008-09-30)

著者

小関 悠 角 康之 西田 豊明 間瀬 健二

出版者

日本ソフトウェア科学会

雑誌

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

巻号頁・発行日

vol.24, no.3, pp.3_41-3_50, 2007 (Released:2007-09-30)

---

本稿では研究発表会や博物館見学といったイベント空間において取得可能な体験データを,ユーザーが閲覧・編集するためのシステムを提案・実装する.種々のカメラやセンサー機器の発達により大量の取得が可能となった体験データを,ユーザーの扱いやすい形にすることで,その編集や共有を促すことが狙いである.システムは大きく二つの部分に分けられる.一つは体験データを自動的に要約してユーザーに提示するシステムであり,特にセンサー情報を用いることで映像データを「ぱらぱらアニメ」,すなわち,シーンを表現する複数枚の特徴的なスナップショットのセットへと変換する手法について述べる.もう一つは要約された体験データの鑑賞・編集システムであり,こちらでは「ぱらぱらアニメ」の特性を生かし漫画的なレイアウトを組むことで体験データを好みの観点で観賞・編集が出来ることを中心に述べる.本システムは体験データの閲覧や編集へのアクセシビリティを高めるため,Webアプリケーションとして実装した.

著者

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

出版者

日本ソフトウェア科学会

雑誌

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

巻号頁・発行日

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

---

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