著者
小形 真平 松浦 佐江子
出版者
日本ソフトウェア科学会
雑誌
コンピュータ ソフトウェア (ISSN:02896540)
巻号頁・発行日
vol.27, no.2, pp.2_14-2_32, 2010-04-27 (Released:2010-06-27)

業務システム開発では,顧客と開発者の間の要求の誤解,顧客の暗黙的要求の存在,開発者の要求の誤った仕様化を原因として,要求仕様の品質が低下する問題がある.そこで,顧客が妥当性を確認した要求分析モデルによるシステム開発手法の確立を目的として,業務系Webアプリケーション開発を対象に,UML要求分析モデルからWeb UIプロトタイプを自動生成する手法を提案する.本研究では,業務を構成する業務遂行手順および業務データをそれぞれ,サービスを構成するユーザとシステムのやり取りおよびやり取り中の入出力データとみなす.そして,この振舞いとデータの観点から,アクティビティ図・クラス図・オブジェクト図を用いて要求分析モデルを定義し,要求分析モデルの妥当性を確認するためのHTML形式のUIプロトタイプを生成する.本稿では,複数の適用事例を通して提案手法の有効性について議論する.
著者
古澤 仁 高井 利憲 Hitoshi Furusawa Toshinori Takai 鹿児島大学理学部数理情報科学科 産業技術総合研究所システム検証研究センター Department of Mathematics and Computer Science Faculty of Science Kagoshima University Research Center for Verification and Semantics AIST.
出版者
日本ソフトウェア科学会
雑誌
コンピュータソフトウェア (ISSN:02896540)
巻号頁・発行日
vol.23, no.3, pp.14-34, 2006-07-26
参考文献数
46

クリーニ代数は正規言語を公理的に取り扱うための代数的枠組みである.正規表現が計算機科学のいたるところに現れることを考えると,クリーニ代数が計算機科学に現れる構造の自然なクラスの性質を公理的にとらえ得るであろうことが容易に推測されるであろう.クリーニ代数の定義は,等式とホーン節で与えられるため,ある現象をクリーニ代数においてモデル化すると,その現象が簡単な式変形によって検証できるという特徴をもつ.本稿ではクリーニ代数の基本的な性質とそのプログラム理論への応用例について紹介する.A Kleene algebra is an algebraic framework to handle regular languages. Considering that regular expressions appear everywhere in fields of computer science, it may be easy to infer that a Kleene algebra can captures properties of natural class of structures appear in computer science. Since Kleene algebras are defined by equations and Horn clauses, if a phenomenon is interpreted in Kleene algebra, reasoning of the phenomenon is performed by simple transformations of expressions. We introduce basic properties and application examples of Kleene algebras to theory of programs.
著者
小笠原 寛弥 鈴木 育男 山本 雅人 古川 正志
出版者
日本ソフトウェア科学会
雑誌
ネットワークが創発する知能研究会(JWEIN10)講演論文集
巻号頁・発行日
pp.4, 2010-08-20

「行為を決定するのは,行為者の属性と自身を取り囲む関係構造である.」これは複雑ネットワーク科学の 研究がなされる以前から社会学等でも扱われてきた,ネットワーク科学における基本的な考え方である.本研究では,こうした関係構造を結合振動子を用いてモデル化し,その性質や構造,成長におけるダイナミクスを明らかにする.更に,ノード間の相互作用とネットワークの成長の関係性について明らかにする.
著者
戸田 貴久 斎藤 寿樹 岩下 洋哲 川原 純 湊 真一
出版者
日本ソフトウェア科学会
雑誌
コンピュータ ソフトウェア (ISSN:02896540)
巻号頁・発行日
vol.34, no.3, pp.3_97-3_120, 2017-07-25 (Released:2017-08-09)

列挙問題とは,与えられた条件を満たす対象(解)をすべて求める問題であり,電力網解析など社会のさまざまな問題への応用がある.さまざまな組合せ列挙問題に対して,問題の解集合を表現するデータ構造ZDDを高速に求める方法(トップダウンZDD構築法)を通して元の問題を効率的に解く汎用的な手法の研究が近年盛んに行われている.本論文ではトップダウンZDD構築に焦点を絞り,基礎となるアルゴリズムから,複雑な問題制約に対処するための発展的手法,プログラミングツールTdZddの基本的な使い方,さらに,具体的な応用問題を例にしたプログラミングまで解説する.
著者
阿萬 裕久 野中 誠 水野 修
出版者
日本ソフトウェア科学会
雑誌
コンピュータ ソフトウェア (ISSN:02896540)
巻号頁・発行日
vol.28, no.3, pp.3_12-3_28, 2011-07-26 (Released:2011-09-26)

ソフトウェアメトリクスは,ソフトウェアの品質マネジメントを実践する上で必要不可欠な存在である.しかしながら,実際のところ広く積極的に活用されているとまでは言い難い.その背景には“何を測り,どう活用するのか?”というシンプルではあるが容易でない問題がある.本論文はそのための一助として,ソフトウェアメトリクスとそこでのデータ分析の基礎,特に,どういったソフトウェアメトリクスや数理モデルがあり,分析で何に気を付けるべきかを中心に解説を行っている.また,ソフトウェアメトリクスの円滑な活用に役立つツールもいくつか紹介している.
著者
横尾 真 岩崎 敦 櫻井 祐子 岡本 吉央
出版者
日本ソフトウェア科学会
雑誌
コンピュータ ソフトウェア (ISSN:02896540)
巻号頁・発行日
vol.30, no.2, pp.2_33-2_51, 2013-04-25 (Released:2013-08-25)

本稿では,ゲーム理論の主要領域の1つである協力ゲームについて解説する.協力ゲームは,主に2つの研究領域からなる.1つは,提携内のプレイヤ間で,協力によって得られた利益をどのように分配するかである.本編では,解概念と呼ばれる,協力的なエージェント間で利得を配分する望ましい方法について概説する.古典的な協力ゲーム理論では,コア,シャプレイ値,仁など,さまざまな解概念が提案されている.これらの解概念によって与えられる利得の配分を求めるアルゴリズムと計算量について考察する.2つ目は,全体提携が最適ではない場合,プレイヤがどのような協力関係(提携)を形成するかである.これは,提携構造形成問題(CSG)と呼ばれる.本編では,CSGを効率的に解く制約付き最適化アルゴリズムを紹介する.また,本編ではゲームの簡潔表現法を利用することで解概念やCSGに関する問題を効率的に解くことができるため,協力ゲームの簡潔な記述方法を概説する.
著者
妻木 俊彦
出版者
日本ソフトウェア科学会
雑誌
コンピュータ ソフトウェア (ISSN:02896540)
巻号頁・発行日
vol.29, no.2, pp.2_43-2_64, 2012-04-25 (Released:2012-06-25)

要求工学は,ソフトウェアシステムの外部仕様である振る舞いや制約を定義するための技術の集合である.そして,そこで定義された要求は,われわれが実際に生存している現実世界における意味や価値を反映したものでなければならない.極めて多岐にわたる要求工学の技術を,本稿では,正確な要求を定義するための技術,変動する要求に対処するための技術,および,視点の多様性に対応するための技術という3つの観点から概観する.
著者
高橋 和也 南出 靖彦
出版者
日本ソフトウェア科学会
雑誌
コンピュータ ソフトウェア (ISSN:02896540)
巻号頁・発行日
vol.38, no.2, pp.2_53-2_70, 2021-04-23 (Released:2021-06-23)

文字列の検索等に広く用いられる正規表現マッチングはその多くがバックトラックに基づくアルゴリズムで実装されており,対象文字列の長さに対して線形時間でマッチングを完了できない場合がある.これを事前に検知するために,マッチングに要する計算量を静的解析する手法が複数の先行研究によって提案されている.本研究では先行研究を拡張し,先読みや後方参照など,現実のソフトウェアで使用されている拡張された正規表現に対しても解析が行える手法を提案する.さらに,既存の解析アルゴリズムを高速化し,より実用的な速度で解析を行える手法を提案する.そして,これらの改良を施した計算量解析のツールをScalaで実装し,Weidemanらによる既存のツールよりも多くの正規表現が解析できることを実験により確認した.
著者
逢坂 美冬 上野 雄大 大堀 淳
出版者
日本ソフトウェア科学会
雑誌
コンピュータ ソフトウェア (ISSN:02896540)
巻号頁・発行日
vol.35, no.3, pp.3_79-3_95, 2018-07-25 (Released:2018-09-25)

一般にWebアプリケーションにおけるWebページの動的生成は,テンプレートエンジンを用い,事前に用意されたテンプレートに対して動的に値を埋め込むことで行う.テンプレートはテキストファイルとして用意され,実行時に読み込まれる.そのため,テンプレートに対する操作は一般に型無しの文字列操作となる.従って,たとえホスト言語が強い型付けを持つ関数型言語であったとしても,実際のテンプレート構造とプログラムの想定の間の不整合は静的に検出されない.本論文では,動的に読み込まれるテンプレートに対して,部分動的レコードに基づく動的型検査を行うことで,型付きのテンプレート操作を実現する言語機構を提案する.この機構は,テンプレートにホール名をラベルとするMLの部分動的レコード型を与え,テンプレートに値を埋め込む操作をレコードの更新演算と同様に型付けする.テンプレートに存在しないホールへの値の埋め込みは型エラーとなる.プログラムが想定するテンプレートの型と実際のテンプレートの構造の整合性は,テンプレートファイル読み込み時に動的に検査する.本論文ではさらに,この機構をML系関数型言語SML#のコンパイラを拡張することで実装し,実例を通じて実用性を検証するとともに,実用上の課題について議論する.
著者
叢 悠悠 浅井 健一
出版者
日本ソフトウェア科学会
雑誌
コンピュータ ソフトウェア (ISSN:02896540)
巻号頁・発行日
vol.36, no.2, pp.2_47-2_60, 2019-04-26 (Released:2019-06-25)

CoqやAgdaなどの定理証明支援系では,依存型を使ってプログラムの性質を正確に記述することができる.一方,依存型付き言語の多くは,副作用を許さないという制約もつ.これは,副作用の動的な振る舞いによって型が静的に定まらなくなることによるが,副作用の欠如は実用的なプログラムの実装の妨げとなるため,適切な制約を設けながら,依存型付き言語に副作用を導入する試みがなされてきた.本研究では,限定継続命令 shift/resetをもつ依存型付き言語を考える.shift/resetはさまざまな副作用の模倣を可能にするが,その応用例や型システムは単純型付き言語で考えられてきた.本稿では,shift/reset と依存型を組み合わせるために必要な制約を明らかにし,健全な型システムを定義する.また,設計した言語に対するCPS変換を与え,変換が型を保存することを証明する.
著者
松原 克弥 髙川 雄平
出版者
日本ソフトウェア科学会
雑誌
コンピュータ ソフトウェア (ISSN:02896540)
巻号頁・発行日
vol.39, no.1, pp.1_18-1_32, 2022-01-25 (Released:2022-03-25)

コンピュータ技術進歩の過程において,基盤ソフトウェアであるオペレーティングシステム(OS)の研究開発が盛んに行われ,数多くのOS実装が利用可能となった.デスクトップPCやスマートフォン,エンタープライズサーバなどの一部のプラットフォーム向けでは,WindowsやLinuxなどの少数のOSが寡占状態にあるが,すべてのシステムにおいて特定のOSが独占して採用されることはなく,現在でも,システムの目的や用途,プラットフォームの特性などに応じて複数のOSを使い分けている.著者らは,特性の異なる複数のOSを状況の変化に応じて動的に切り替えることで,OS上で稼働するサービスの負荷耐性や性能の改善を試みる手法を提案している.本論文では,LinuxとFreeBSDを対象として,サービス稼働中にそのシステム基盤であるOSの動的な切り替えを可能とすることを目的として,FreeBSDにおけるLinux互換プロセスのマイグレーション機構の実現手法についてまとめる.Linuxにおけるプロセスマイグレーション機構の標準ツールであるCRIUとのチェックポイントデータの相互互換性を維持することで,LinuxとFreeBSD間で同一のプロセスをマイグレーションする仕組みを実現する.本実現法では,FreeBSDカーネルとLinuxカーネルのOS機能の違いだけでなく,内部構造やインタフェース仕様の違いにも着目し,CRIUの各機能と同等の機能をFreeBSD上で実現する際の課題や実装の詳細を述べる.