著者
吉岡 信和 田辺 良則 田原 康之 長谷川 哲夫 磯部 祥尚
出版者
日本ソフトウェア科学会
雑誌
コンピュータ ソフトウェア (ISSN:02896540)
巻号頁・発行日
vol.31, no.4, pp.4_40-4_65, 2014-10-24 (Released:2014-12-24)

機器の高速化やネットワークの発展に伴い,多数の機器やコンポーネントを連携させ,高度な機能を提供する並行分散システムが一般的になってきている.そのようなシステムでは,振舞いの可能性が膨大であり,従来のレビューやシミュレーションで設計の振舞いの正しさを保証することは困難である.それに対して,網羅的にかつ自動的に振舞いに関する性質を調べるモデル検査技術が注目されている.本稿では,モデル検査技術の背景と5つの代表的なモデル検査ツールを紹介し,その応用事例や最新の研究動向を解説する.
著者
小田 朋宏 荒木 啓二郎
出版者
日本ソフトウェア科学会
雑誌
コンピュータ ソフトウェア (ISSN:02896540)
巻号頁・発行日
vol.34, no.4, pp.4_129-4_143, 2017

ソフトウェアシステムの開発において仕様記述は重要な工程であり,仕様記述の曖昧さや誤りは開発全体の生産性および信頼性に重大な影響を与えることが知られている.形式仕様を記述することはモデリングの一種であり,数学的な裏付けのある道具立てによって適切な抽象度でシステムの機能を厳密に定義する工程である.厳密で適切な抽象度の仕様記述を得るために,形式仕様記述者は仕様記述の初期段階において問題領域を探索し対象ドメインの知識獲得や要求項目への理解を深めながらモデリングを進める.本論文では,探索的なモデリングを支援するためのツールに求められる性質を示した上で,形式仕様記述言語VDM-SLによる探索的モデリングを支援する統合開発環境ViennaTalkのデザイン指針,設計および実装を示す.
著者
辻田 眸 暦本 純一
出版者
日本ソフトウェア科学会
雑誌
コンピュータ ソフトウェア (ISSN:02896540)
巻号頁・発行日
vol.29, no.4, pp.4_305-4_315, 2012-10-25 (Released:2012-11-25)

高齢化など様々な要因で,独居生活を選択あるいは余儀なくされている人は少なくない.孤独な生活により感情状態が悪化し,うつ病や心の病にかかるなど深刻な問題である.一方,心理学者ウィリアム・ジェイムズの言説で,「人は幸福であるが故に笑うのではなく,笑うが故に幸福である」という考え方がある.これは笑顔形成が感情状態を向上させる可能性を示唆している.そこで本論文では,日常生活のなかで積極的に笑顔をつくることを促進し,感情状態の向上を支援するシステム「HappinessCounter」を提案する.笑顔促進のために,ユーザが日常的に行う作業時に笑顔形成を促し,フィードバックを与えたり,ソーシャルネットワークサービスなどと連携させることで,より積極的に笑顔形成を支援し,感情状態の向上を目指す.さらに試作したシステムを実際の日常生活で利用してもらい評価実験を行った.実験結果から,本システムが笑顔促進に効果的に働き,また家族間のコミュニケーションにも影響があったことが窺えた.
著者
小出 誠二 武田 英明
出版者
日本ソフトウェア科学会
雑誌
コンピュータ ソフトウェア (ISSN:02896540)
巻号頁・発行日
vol.28, no.2, pp.2_236-2_260, 2011-04-26 (Released:2011-05-26)

本研究の目的は,モデル駆動型アーキテクチュアの一種であるオントロジー駆動型ソフトウェア開発をオブジェクト指向プログラミングにおいて可能にすることである.本実現手法では,RDFのクラス/メタクラスをCommon Lisp Object System (CLOS)のクラス/メタクラスに写像し,トリプルをCLOSのオブジェクト/スロット名/スロット値に対応させて,CLOSの標準仕様をMeta-Object Protocol (MOP)を用いて,RDF(S)およびOWLの意味論にあわせて拡張した.RDF(S)およびOWLの公理と多くの伴意ルールを実装し,RDF(S)推論とOWL推論を実現するとともに,CLOSメタプログラミング機能を利用したオントロジーのOWL Fullメタモデリングを可能にした.本論文ではそのシステム実現方法について述べ,あるベンチマーク結果について報告する.また,RDF公理に基づいてオントロジーメタモデリングの指針を導くとともに,本システムによるメタモデリングの実例を述べる.
著者
井出 陽子 向井 国昭
出版者
日本ソフトウェア科学会
雑誌
コンピュータ ソフトウェア (ISSN:02896540)
巻号頁・発行日
vol.28, no.4, pp.4_108-4_113, 2011-10-25 (Released:2011-11-30)

高階述語の呼び出しなどに便利な無名述語(λ項の拡張)の構文および意味を標準のProlog意味論に基づいて定義し,SWI-Prologの上に実装した.無名述語の呼び出しに標準の単一化がそのまま使えるほか,パラメータを持つ無名述語も扱える.無名述語をコンパイル時に通常の述語として展開するので,通常の述語呼び出しと実行効率は同じである.実行時に動的に生成された無名述語に対しては専用のインタプリタで対応する.使用実験の結果,無名述語の利便性や記述力の高さ,安定性が確認できたので,標準環境として使えるように無名述語機能をパッケージ化した.
著者
乾 敦行 工藤 晋太郎 原 耕司 水野 謙 加藤 紀夫 上田 和紀
出版者
日本ソフトウェア科学会
雑誌
コンピュータ ソフトウェア (ISSN:02896540)
巻号頁・発行日
vol.25, no.1, pp.1_124-1_150, 2008 (Released:2008-02-29)

LMNtalは階層グラフ書換えに基づく単純な言語モデルであり,接続構造の表現に論理変数を,階層構造の表現に膜を用いることを特徴としている.LMNtalは,多重集合や並行処理やモビリティなどの概念を持つさまざまな計算モデルの統合を目指すと同時に,階層グラフ書換えに基づく実用的なプログラミング言語を提供してその有用性を示すことを重要な目標としている.本論文の目的は,プログラミング言語としてのLMNtalの諸機能を紹介し,その記述力を多くの例題を用いて示すことである.我々は,算術,ルール適用制御,モジュール,他言語インタフェースなどの重要機能を階層グラフ書換えモデルの中に組み込む方法を設計し実装した.記述力の検証のためにλ計算,π計算,ambient計算,CHRなどの代表的な関連計算モデルのエンコーディングを行い,それらを実際に処理系上で動作させることに成功した.
著者
坂平 文博 寺野 隆雄
出版者
日本ソフトウェア科学会
雑誌
コンピュータ ソフトウェア (ISSN:02896540)
巻号頁・発行日
vol.31, no.3, pp.3_97-3_108, 2014-07-25 (Released:2014-09-10)

人類学・考古学においては,物的資料が残されていない,ある特定の時点間で起きた変化の「プロセス」について客観的な考察を行うことが難しい.そこで,筆者らはこの変化の「プロセス」を抽出する方法として,エージェントベースシミュレーション(ABS)を適用する.本論文では,弥生時代の農耕文化の「主体」についての問題をABSによって検討する.シミュレーションの結果,初期の段階で多くの縄文系弥生人に農耕が伝播した場合の方が,渡来系弥生人が300年後に大多数を占めることが示された.この結果は,農耕文化の「主体」が,初期において縄文系弥生人でその後は混血の人々であった可能性を示す.本研究の人類学・考古学分野へのABSの貢献は以下のとおりである.既存研究の多くが入力データやモデルからシミュレーション結果が歴史事象を説明できるかどうかという問題を扱っているのに対して,本論文ではABSを新しい仮説に繋がる変化の「プロセス」を調べる新しいツールとして利用している.
著者
五十嵐 悠紀 五十嵐 健夫 鈴木 宏正
出版者
日本ソフトウェア科学会
雑誌
コンピュータ ソフトウェア (ISSN:02896540)
巻号頁・発行日
vol.26, no.1, pp.1_51-1_58, 2009-01-27 (Released:2009-03-27)

“あみぐるみ”は毛糸を使って作るぬいぐるみであるが,毛糸の編み方によって形状をデザインしていくため,初心者にはデザインすることが困難である.我々は3次元モデリングプロセスにインタラクティブな物理シミュレーションを組み合わせることであみぐるみを効率的にデザインできるモデラーを作成した.本システムは自動で編み目を計算してあみぐるみモデルをシミュレーション結果として提示するため,初心者にでも直感的にデザインでき,編み図も容易に得ることができる.また,初めてあみぐるみに挑戦する初心者でも製作手順を容易に理解できるようにするために,製作手順を視覚的に提示する製作支援インタフェースも備えた.あみぐるみ初心者でも容易にオリジナルなあみぐるみを作成できることを確認したので報告する.
著者
高橋 祐多 中野 圭介
出版者
日本ソフトウェア科学会
雑誌
コンピュータ ソフトウェア (ISSN:02896540)
巻号頁・発行日
vol.35, no.4, pp.52-71, 2018-10-25 (Released:2018-12-26)

一般に関数の等価性判定問題は決定不能であるが,関数の定義に構文的な制約を加えることで決定可能にすることができる. そのような制約の 1 つとして,木から文字列への決定性トップダウン変換(deterministic top-down tree-to-string transducer,yDT)が存在し, 等価性判定が決定可能な関数としては,比較的広い範囲のものを扱うことができる. この yDT の等価性判定の決定可能性は 2015 年に Seidl らによって示されたが,2 つの半アルゴリズムを組み合わせることによって証明されており, 計算量が特定できず,実用性が確認されていない. そこで,本論文では yDT の等価性判定を行うプログラムを実装し,Seidl らの等価性判定アルゴリズムが実用に堪えうるものか検証する.
著者
番原 睦則 田村 直之 井上 克已
出版者
日本ソフトウェア科学会
雑誌
コンピュータ ソフトウェア (ISSN:02896540)
巻号頁・発行日
vol.24, no.3, pp.3_75-3_86, 2007 (Released:2007-09-30)

本論文では,PrologからJavaへのトランスレータ処理系Prolog Cafeについて述べる.本システムでは,Prologプログラムは,WAMを介して,Javaプログラムに変換され,既存のJava処理系を用いてコンパイル・実行される.つまりProlog Cafeでは,項,述語などPrologの構成要素のすべてがJavaに変換される.このため,Prolog CafeはJavaとの連携,拡張性に優れたProlog処理系となっている.Prolog Cafeはマルチスレッドによる並列実行をサポートしており,スレッド間の通信は共有Javaオブジェクトにより実現される.また任意のJavaオブジェクトをPrologの項として取り扱う機能を有しており,Prologからメソッド呼び出し,フィールドへのアクセスも行える.最後にProlog Cafeの応用として,複数SATソルバの並列実行システムMultisatについて述べる.
著者
小川 秀人
出版者
日本ソフトウェア科学会
雑誌
コンピュータ ソフトウェア (ISSN:02896540)
巻号頁・発行日
vol.28, no.3, pp.3_2-3_11, 2011-07-26 (Released:2011-09-26)
被引用文献数
1

ソフトウェア工学は,ソフトウェア開発を対象とする工学である.しかし,ソフトウェア工学とソフトウェア開発との間に,ギャップを感じることがあるのも事実である.筆者らは,企業内研究所にて,企業におけるソフトウェア開発を対象としたソフトウェア工学研究(本稿では「ソフトウェア開発技術研究」)と,そのソフトウェア開発への適用を進めている.本稿では,企業論文誌の分析を通して企業でのソフトウェア開発技術研究の傾向を示し,ビジネスとしてのソフトウェア開発と学術としてのソフトウェア工学との間にあるギャップの理解を試みる.
著者
竹野 創平 渡部 卓雄
出版者
日本ソフトウェア科学会
雑誌
コンピュータ ソフトウェア (ISSN:02896540)
巻号頁・発行日
vol.33, no.1, pp.1_167-1_180, 2016-01-26 (Released:2016-02-06)

本研究で我々は並行文脈指向プログラミングの概念とその実現手法を提案する.アクターモデルのような非同期通信に基づくシステムで文脈指向プログラミングを実現する際,文脈の変化と他の計算の間の同期に注意する必要がある.提案する手法は,文脈をまたがるメッセージに関する問題を自己反映計算を用いることで解決するものである.本論文ではErlangを用いた実装とその予備評価について述べ,提案手法の有効性を示す.
著者
深津 佳智 箱田 博之 野口 杏奈 志築 文太郎 田中 二郎
出版者
Japan Society for Software Science and Technology
雑誌
コンピュータ ソフトウェア (ISSN:02896540)
巻号頁・発行日
vol.31, no.3, pp.3_325-3_335, 2014

本研究では,スマートフォンをアイズフリーに片手操作する際のタッチ精度向上を目的として,凹凸を付けたスマートフォンケースを作成した.我々は,ユーザがケースの凹凸を触り,タッチの際の手がかりにすることができると考えた.それぞれのケースを装着したスマートフォンを用いて被験者実験を行い,タッチの精度を評価した.
著者
山中 祥太 宮下 芳明
出版者
日本ソフトウェア科学会
雑誌
コンピュータ ソフトウェア (ISSN:02896540)
巻号頁・発行日
vol.33, no.4, pp.4_116-4_121, 2016-10-25 (Released:2017-01-14)

The steering law is a robust model for expressing the relationship between movement time and task difficulty. Recently, a corrected model to calculate the steering time difference between narrowing and widening tunnels was proposed. However, the previous work only conducted a user study with straight paths. This paper presents an investigation of steering performance in narrowing and widening circular tunnels to confirm the corrected model as being either adequate or a limitation. The results show that the steering law achieves a good fit (R2>.98) without the corrected model, thereby indicating the limited benefit of employing the corrected model.