著者

宋 剛秀 番原 睦則 田村 直之 鍋島 英知

出版者

日本ソフトウェア科学会

雑誌

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

巻号頁・発行日

vol.35, no.4, pp.72-92, 2018-10-25 (Released:2018-12-26)

---

命題論理式の充足可能性判定(SAT)問題を解くプログラムであるSATソルバーは,2000年以降その性能面において飛躍的に進化した.それに伴い,解きたい問題をSAT符号化によりSAT問題へと変換し,SATソルバーを用いて解くSAT型システムが,プランニング,ソフトウェア・ハードウェア検証,スケジューリング問題など様々な分野で成功を収めるようになった.本稿では,まずSATソルバーの最新動向として,性能面と機能面における進化をその要因の1つであるSATソルバーの国際競技会の視点から説明を行う.次に SAT ソルバーの利用技術の視点から,SAT ソルバーの機能面の進化と符号化技術を組み合わせることで,複雑な問題を解くことが可能になることの説明を行う.そのような例として多目的最適化問題のパレート解をSATソルバーを利用して求める方法を説明する.

著者

千葉 滋

出版者

日本ソフトウェア科学会

雑誌

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

巻号頁・発行日

vol.39, no.1, pp.1_78-1_83, 2022-01-25 (Released:2022-03-25)

著者

田村 直之 番原 睦則

出版者

日本ソフトウェア科学会

雑誌

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

巻号頁・発行日

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

著者

権藤 克彦

出版者

日本ソフトウェア科学会

雑誌

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

巻号頁・発行日

vol.38, no.4, pp.4_1, 2021-10-22 (Released:2021-12-22)

著者

萩原 早紀 栗原 一貴

出版者

日本ソフトウェア科学会

雑誌

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

巻号頁・発行日

vol.33, no.1, pp.1_52-1_62, 2016-01-26 (Released:2016-03-26)

---

本論文では,俗に“コミュ障”と呼ばれている人間の性質に注目し,その中で他人と視線を合わせられない症状をもつ人々を社会福祉学的な観点から支援するためのシースルー型HMD を使用したシステムの提案を行う.この“コミュ障”支援システムは,彼ら/彼女らが他人と視線を合わせられないというコミュニケーション上の問題を緩和・改善するために,顔検出技術と視覚情報提示により相手の顔を隠したり,視線をそらす癖を改善するように指示したり,視線の挙動の客観的なデータを提示したり,コミュニケーション上の危険状態が発生した場合その場から脱出する手段を与えてくれる.このシステムのプロトタイプを実装し,評価した結果,いくつかの機能は有効に働き,今後の改善点が得られた.

著者

中川 尊雄 亀井 靖高 上野 秀剛 門田 暁人 鵜林 尚靖 松本 健一

出版者

日本ソフトウェア科学会

雑誌

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

巻号頁・発行日

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

---

本論文は,NIRS (Near Infra-Red Spectroscopy; 近赤外分光法)による脳血流計測を用い,開発者がプログラム理解時に困難を感じているかの判別を試みた我々の先行研究(レター論文)を発展させたものである.本論文では,20名の被験者に対して,難易度の異なる三種類のプログラムの理解時の脳血流を計測する実験を行った.実験が中断された3名を除く17名中16名において,(1)難易度の高いプログラムの理解時に脳活動がより活発化するという結果(正確二項検定, p < 0.01)が得られた.また,(2)被験者アンケートによって得られた難易度の主観的評価と,脳活動値の間には有意な相関(スピアマンの順位相関係数 = 0.46, p < 0.01)がみられた.

著者

亀井 聡

出版者

日本ソフトウェア科学会

雑誌

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

巻号頁・発行日

vol.22, no.3, pp.3_8-3_18, 2005 (Released:2005-09-30)

---

インターネットにおいて,P2P (Peer-to-Peer) 技術の発展がめざましい.P2P技術は様々なメリットを持つ反面,インターネットのトラフィックの主流をこれまで占めていたウェブ等と異なる特性を持つため,ネットワークインフラに様々な影響を及ぼし始めている.本稿ではこのような現状を紹介するとともに,P2P技術とインフラの融合に向けての課題について述べる.

著者

アフェルト レナルド

出版者

日本ソフトウェア科学会

雑誌

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

巻号頁・発行日

vol.34, no.2, pp.2_64-2_74, 2017-04-26 (Released:2017-06-26)

---

コンピュータのプログラムと数学の証明の間に密な関係があることはよく知られている.1969年に発見されたCurry-Howard同型対応により,プログラムの型を言明(statement)として見れば,プログラム自体はその言明の証明として見られる.これにより,数学の証明の検査はプログラムの型付けに帰着する.この発想に基づいて,定理証明支援系という検証ツールの開発が行われてきた.近年,定理証明支援系を用いて,ようやく現実的なプログラムと証明の検証が可能となっている.現実的な証明の一例として,2005年から2012年までマイクロソフト・INRIAの共同研究組織で形式化された奇数位数定理が挙げられる.奇数位数定理は膨大な証明により示された重要な群論の定理であるため,その形式化は大きなマイルストーンとなっている.加えて,その形式化の基盤であるMathematical Componentsもまた,形式数学におけるライブラリとして重要な成果である.我々のデジタル社会を支える基本的なコンピュータプログラムであるRSA暗号や楕円曲線暗号や符号などは,整数論や群論や線形代数などの数学に基づいているが,Mathematical Componentsを用いることで,これらのプログラムの厳密な仕様の記述ができるようになった.しかし,Mathematical Componentsのような大規模なライブラリの利用には専門知識が不可欠である.本解説では,Mathematical Componentsによる形式化を紹介する.群論のラグランジュ定理を用いて,そのライブラリの基本的な使い方を説明する.

著者

鳥海 不二夫 西村 啓 浅野 千尋 石井 健一郎

出版者

日本ソフトウェア科学会

雑誌

コンピュータ ソフトウェア

巻号頁・発行日

vol.25, no.4, pp.190-198, 2008

---

近年市場における個人投資家の割合は増加の一途をたどっている.これにともない,アルゴリズムトレードを利用した取引が注目されている.しかしながら,投資家にとって取引エージェントの作成は障害が多く,自動取引エージェント上に優秀なアルゴリズムを実現するのは困難である.そこで,本研究では投資スキルは十分にあるもののプログラミングのスキルが十分ではない投資家に対して,その投資家の投資戦略を取引エージェント上で実現することを目指し,自動取引エージェントの作成支援システムを提案し,第一回スーパーカブロボコンテスト用で利用した.その結果,コンテスト参加者の60%が本支援システムを利用して取引エージェントを作成した.作成支援システムによって作られた自動取引エージェントは,Javaプログラミングによって作成された自動取引エージェントと比較して同程度の取引を行うことが出来ることを確認した.また,プログラミングスキルの低い投資家に対してもアルゴリズムトレードへの参加を促すことができたことを確認した.

著者

寺岡 文男

出版者

日本ソフトウェア科学会

雑誌

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

巻号頁・発行日

vol.28, no.2, pp.2_3-2_14, 2011-04-26 (Released:2011-06-26)

---

インターネットにはさまざまな新しい技術がいわば“つぎはぎ”のように追加されて発展してきた.このままではインターネットは破綻を来してしまうという危惧から,インターネットを一から設計し直そうという考え方(clean slateアプローチ)が2000年ころから出てきた.本稿ではclean slateアプローチに基づいて設計されたネットワークを“新世代ネットワーク”と呼ぶこととし,新世代ネットワークに関するいつかの研究を,(1)ネットワークアーキテクチャ,(2)ネットワーク仮想化,(3)超広帯域ネットワーク,という3つの観点から紹介する.

著者

岩間 太 中村 大賀 竹内 広宜

出版者

日本ソフトウェア科学会

雑誌

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

巻号頁・発行日

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

---

半形式的な記述や半構造的な自然文を含むテキスト文書のためのパーサーを形式言語/自然言語処理パーサーを組み合わて構築するためのシステムを提案する.特に,形式言語/自然言語処理パーサーを柔軟に組み合わせるためのパーサーコンビネータを設計することで,宣言的な文法記述からテキスト文書用のパーサーを作成するシステムを実現する.現状のパーサーコンビネーターは主にプログラミング言語用のパーサー構築を目的としており,自然文を含むテキスト文書のためのパーサーを構築するには不十分である.特に,既存の様々な自然言語処理パーサーは,形式言語のためのパーサーとは異なった性質をもっており,既存の枠組みでは柔軟に組合わせることが難しい.本論文では,自然言語処理パーサーと形式言語用のパーサーの組合せを可能にし,かつ,部分的なパージングや情報抽出部分の指定など,テキスト文書の処理において有用な機能を実現する演算子を含んだパーサーコンビネーターをParsing Expression Grammarsを基に設計する.また,導入したパーサーコンビネーターを用いて,宣言的な記述から,種々の自然言語処理を部分的に含むパーサーを自動生成するためのシステムを構築し,実際の適用例の一端を示す.このようなパーサーコンビネーションシステムはソフトウエア開発時に作成される文書成果物に対する解析に有用である.

著者

山本 拓朗 大山 博司 安積 卓也

出版者

日本ソフトウェア科学会

雑誌

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

巻号頁・発行日

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

---

The complexity and scale of embedded software have increased. To improve the productivity, the mruby on TOPPERS embedded component system (TECS) framework, which employs a scripting language (i.e., lightweight Ruby) and supports component-based development, has been proposed. In the current mruby on TECS framework, mruby programs must be compiled and linked every time they are modified, because mruby bytecode are incorporated in the platform. Moreover, while the framework supports multiple virtual machines (VMs), developers must be familiar with the functions of real-time operating systems to effectively execute multiple mruby programs concurrently or in parallel. This paper proposed an extended mruby on TECS framework that improves development efficiency more than the current framework. We implemented a Bluetooth loader receives an mruby bytecode, and a RiteVM scheduler simplifies multitasking. Synchronization of initializing multiple tasks is also implemented using an Eventflag. Experimental results demonstrate the advantages of the proposed framework.

著者

吉岡 信和 田辺 良則 田原 康之 長谷川 哲夫 磯部 祥尚

出版者

日本ソフトウェア科学会

雑誌

コンピュータ ソフトウェア (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.15, no.6, pp.6_547-6_560, 1998-11-16 (Released:2018-11-05)

著者

井出 陽子 向井 国昭

出版者

日本ソフトウェア科学会

雑誌

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

巻号頁・発行日

vol.28, no.4, pp.4_108-4_113, 2011-10-25 (Released:2011-11-30)

---

高階述語の呼び出しなどに便利な無名述語(λ項の拡張)の構文および意味を標準のProlog意味論に基づいて定義し,SWI-Prologの上に実装した.無名述語の呼び出しに標準の単一化がそのまま使えるほか,パラメータを持つ無名述語も扱える.無名述語をコンパイル時に通常の述語として展開するので,通常の述語呼び出しと実行効率は同じである.実行時に動的に生成された無名述語に対しては専用のインタプリタで対応する.使用実験の結果,無名述語の利便性や記述力の高さ,安定性が確認できたので,標準環境として使えるように無名述語機能をパッケージ化した.

著者

西崎 真也 植田 友幸

出版者

日本ソフトウェア科学会

雑誌

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

巻号頁・発行日

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

---

従来,関数型言語のためのバイトコードを解釈する仮想機械として、SECDマシンやCAMマシンなど多くのものが提唱され,それらに基づく実装や理論的な側面に関する研究がなされてきた.本論文では,SECDマシンを単純化した仮想機械SAM(Simple Abstract Machine)を提唱する.変数参照機能を単純化することにより,仮想機械におけるファーストクラス継続を簡潔に扱うことが可能になっている。

著者

香川 考司

出版者

日本ソフトウェア科学会

雑誌

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

巻号頁・発行日

pp.13-19, 2005 (Released:2006-03-29)

---

多相ヴァリアントはGUI、データベース、インタプリタなど潜在的に多くの応用分野を持っている。実際、Haskellはパラメトリック型クラスを導入すると、多相ヴァリアントを模倣することができる。しかし現実に多相ヴァリアントを使用することはほとんどない。これは多相ヴァリアントを模倣するコードを手で書くことはたいへん面倒であり、また型の曖昧さが問題となるためであると思われる。この論文では、そこで、Haskellで多相ヴァリアントを模倣するための方法について、解説し、またそれを直接サポートし結果として通常のHaskellのクラスを出力することができる型クラスの拡張について述べる。