著者

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

出版者

日本ソフトウェア科学会

雑誌

コンピュータ ソフトウェア (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による形式化を紹介する.群論のラグランジュ定理を用いて,そのライブラリの基本的な使い方を説明する.

著者

米澤 明憲 武市 正人

出版者

一般社団法人日本ソフトウェア科学会

雑誌

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

巻号頁・発行日

vol.11, no.3, pp.163-164, 1994-05-16

著者

渡部 卓雄

出版者

一般社団法人日本ソフトウェア科学会

雑誌

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

巻号頁・発行日

vol.11, no.3, pp.165-174, 1994-05-16

被引用文献数

16

著者

寺岡 文男

出版者

日本ソフトウェア科学会

雑誌

コンピュータ ソフトウェア (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.2, no.4, pp.582-598, 1985-10-15

被引用文献数

3

---

ConcurrentSmalltalkはSmalltalk-80に並行プログラミング能力を付加したプログラミング言語/システムであり,並行構文,アトミック・オブジェクト,および外部参照解決機構により,分散環境での並行プログラミングを可能にしている.本論文では,オブジェクト指向計算と並行プログラミングについて述べた後,ConcurrentSmalltalkの設計方針と言語仕様について,主に並行プログラミング機能を中心に述べている.最後に,ConcurrentSmalltalkの実装についても述べている.

著者

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

出版者

日本ソフトウェア科学会

雑誌

コンピュータ ソフトウェア (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の上に実装した.無名述語の呼び出しに標準の単一化がそのまま使えるほか,パラメータを持つ無名述語も扱える.無名述語をコンパイル時に通常の述語として展開するので,通常の述語呼び出しと実行効率は同じである.実行時に動的に生成された無名述語に対しては専用のインタプリタで対応する.使用実験の結果,無名述語の利便性や記述力の高さ,安定性が確認できたので,標準環境として使えるように無名述語機能をパッケージ化した.

著者

乾 敦行 工藤 晋太郎 原 耕司 水野 謙 加藤 紀夫 上田 和紀

出版者

日本ソフトウェア科学会

雑誌

コンピュータ ソフトウェア (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.1, pp.1_82-1_85, 2018-01-25 (Released:2018-03-26)

著者

高橋 祐多 中野 圭介

出版者

日本ソフトウェア科学会

雑誌

コンピュータ ソフトウェア (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 らの等価性判定アルゴリズムが実用に堪えうるものか検証する.