著者

阿草 清滋 小林 隆志

雑誌

情報処理

巻号頁・発行日

vol.52, no.10, pp.1254-1257, 2011-09-15

著者

今井 敬吾 結縁祥治 阿草 清滋

出版者

一般社団法人情報処理学会

雑誌

情報処理学会論文誌プログラミング(PRO) (ISSN:18827802)

巻号頁・発行日

vol.47, no.16, pp.10-28, 2006-10-15

参考文献数

17

---

我々はプログラミング言語Haskellへ,型付き非同期局所化pi計算(typed Asynchronous Localized $\pi$-calculus; ALpi)を,ネットワークプログラミングのためのフレームワークとして埋め込む手法を提案する.本フレームワークは埋め込み言語として実装されることで以下の利点を持つ:(1) Haskellで構築されているため処理系が頑健である,(2) Haskellのリテラル,型や関数といった言語要素をフレームワークに組み込むことができる.さらに,ALpiのmobilityに対する制限はフレームワークの実装を簡単にする.本フレームワークでは,ALpiのプロセスはPiMonadと呼ばれるHaskellのモナドとして実装する.結果として,通信により引き起こされる副作用は型のPiMonadタグで区別される.ALpiのサブタイプ関係はHaskellの多引数型クラスで実現する.サブタイプ関係にある型の対は通信の方向を反映した3つの2引数型クラスに属する.本フレームワークを用いた例としてTCP/IPネットワーク上のインスタント・メッセンジャアプリケーションの構築例を示し,有用性と利点を述べる.We propose an embedding of the typed Asynchronous Localized pi-calculus (ALpi) into the programming language Haskell as a framework for network programming. The framework has following advantages due to the embedded language nature: (1) the framework is robust due to being built upon the Haskell framework, and (2) the framework can incorporate various Haskell language elements, such as literals, types, and functions, in the framework. Moreover, the limitation of mobility in ALpi simplifies the implementation of the framework. ALpi processes are implemented by means of a Haskell monad called PiMonad. As the result, side-effects caused by communications are distinguished by the tags of PiMonad in typing. The subtyping relations is realized by multi-parameter type classes in Haskell, where a pair of subtype-related types belongs to three binary type classes reflecting the directions of communication. We illustrate the usefulness and benefits of our framework with an example of an implementation of instance messenger application over TCP/IP network.

著者

金子 伸幸 桑原 寛明 山本 晋一郎 阿草 清滋

出版者

日本ソフトウェア科学会

雑誌

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

巻号頁・発行日

vol.26, no.3, pp.3_34-3_43, 2009-07-28 (Released:2009-10-05)

被引用文献数

1

---

我々は,Strutsを利用して構築されるWebアプリケーションに対するコーディングチェッカとして,StrutsLintを開発した.StrutsLintは,Strutsの設定ファイルおよびJSP,Javaのソースコードを解析し,言語を跨いだ制御依存グラフ,データ依存グラフを生成する.これらのグラフを基に,制約の一貫性などを検査することで対象アプリケーションの整合性検査を行う.本稿では,StrutsLintで実現した機能を基にStrutsアプリケーションに対するコンポーネントウェアとしての整合性検査について述べる.

著者

大須賀恭輔 結縁祥治 阿草 清滋

出版者

一般社団法人情報処理学会

雑誌

情報処理学会論文誌プログラミング(PRO) (ISSN:18827802)

巻号頁・発行日

vol.43, no.8, pp.119-119, 2002-09-15

---

本発表では実時間ステートチャートの振舞いに対してL¨uttgenらのSPL(Statechart Process Language )を時間遷移において拡張した体系として提案したSPLRTを用いて,実時間ステートチャートの動作シミュレートを行うツールの実装を行う.SPLRTは実時間ステートチャートの振舞いをラベルつき遷移システムによりモデル化した言語である.SPLRTはSPL の2つの動作意義,動作遷移,クロック遷移に遅延遷移を新たに加える.遅延遷移はマイクロステップレベルで稠密時間変数を扱う.これによりマクロステップレベルでの実時間の経過を実現可能とした.また,時間遷移を持つラベルつき遷移システムの動作を解析することにより,検証の基礎とすることができる.検証の基礎としてSPLRTにより動作定義し,設計者の意図どおりに実時間ステートチャートが動作するかをツールによって検証を行う.In this presentation, we implements the tool for a simulation of the behavior of real-time statecharts with SPLRT. SPLRT models the behavior of real-time statecharts as the labeled transition system derived from the operational semantics of SPLRT. SPLRT is an extension of SPL proposed by Luttgen et al in that delay transitions labeled by dense-time are incorporated. Analyzing the behavior of the labeled transition system with timed transition can be as the base of verification. We verify whether the real-time statechart behave as an intension of a designer with a tool.

著者

水野 佑基 金子 伸幸 中元 秀明 小川 義明 山本 晋一郎 阿草 清滋

雑誌

情報処理学会研究報告ソフトウェア工学(SE)

巻号頁・発行日

vol.2006, no.35(2006-SE-151), pp.121-128, 2006-03-24

---

本稿では,GUI抽象化規則を用いて実装言語とGUIツールキットに対して柔軟に抽象GUI記述を生成するする手法を提案する.ウィジットと直接操作を表現するGUIプログラミングモデルと,共通GUIツールキットを定義する.抽象GUI記述はGUIプログラミングモデルに従い,共通GUIツールキットを用いて記述される.実装言語やGUIツールキットごとに異なるGUIコードと抽象GUI記述の対応付けをGUI 抽象化規則として定義する.GUI抽象化規則に基づきGUIコードから抽象GUI記述を生成するシステムを提案し,異なる実装言語とGUIツールキットで実装された同一のGUIアプリケーションを同じ抽象GUI記述へと変換できることを確認した.

著者

関 文貴 日高 隆博 山本 晋一郎 小林 隆志 手嶋 茂晴 阿草 清滋

雑誌

研究報告ソフトウェア工学(SE)

巻号頁・発行日

vol.2010-SE-167, no.27, pp.1-9, 2010-03-11

---

車載ソフトウェアでは,コストの観点から浮動小数点演算を用いることができず,アルゴリズムを固定小数点演算で実装しなけれならないことが多い.実数演算を取り扱うアルゴリズムを固定小数点演算へ変換する作業は非常に労力を必要とする.そこで,本論文では浮動小数点演算で記述されたソフトウェアを固定小数点演算へ変換するための手法の提案と自動で変換を行うためのツール開発を行う.

著者

桑原 寛明 結縁祥治 阿草 清滋

出版者

情報処理学会

雑誌

情報処理学会論文誌 (ISSN:18827764)

巻号頁・発行日

vol.45, no.6, pp.1498-1507, 2004-06-15

被引用文献数

2

---

本論文では実時間システム開発にオブジェクト指向開発技術を適用する基礎とするために,形式計算モデルであるπ計算に基づきリアルタイムオブジェクト指向言語の振舞いを定式化する.π計算に離散時間の振舞いを拡張し,単純なリアルタイムオブジェクト指向言語OOLRTの振舞いを記述する.実時間システムは一般に時間制約を持つ複数のオブジェクトの並行動作によって実現される.OOLRTによって実時間システムの特性を直接的に記述し,時間拡張されたπ計算によってその振舞いを厳密に定義することで,システムの動作の解析や検証を形式的に行うための枠組みを与える.In this paper, we aim at providing a foundational framework of the object-oriented technique for system development with timing constraints. We formalize timed behavior of objects via the behavior of π-calculus extended with time. It is common to model a real-time system by composing concurrent objects with timing constraints. To capture the features of real-time objects, we define a simple programming language OOLRT to give the operational semantics by translating a program of OOLRT into a term of our timed π-calculus. By this translation, we obtain an abstract behavioral model for real-time objects to analyze and verify the behavioral properties of real-time systems.

著者

阿草 清滋 落水 浩一郎 片山 卓也 中田 育男 佐伯 元司 鯵坂 恒夫

出版者

名古屋大学

雑誌

重点領域研究

巻号頁・発行日

1997

---

阿草は、既存ソースプログラムを解析しその結果を蓄積するために、細粒度のリポジトリを開発した。CASEツール作成者は、このリポジトリを使うことにより、構文解析や依存解析などのモジュールを作成する手間を省くことができる。ソースプログラムの解析によりライブラリの典型的な利用パターンを発見した。片山は、要求仕様変更とプログラム変更の関係を代数束により形式化し、ソフトウェア発展関係の理論的基礎を与えた。ソフトウェアの段階的詳細化において各段階でプログラムテストを可能とする方式として、抽象実行に基づくソフトウェア構成法を開発した。また、オブジェクト指向開発法の形式化を試み、分析モデルの統合と分析モデルの検証法を与えた。落水は、近年のソフトウェア開発は、分散環境における共同作業であることに注目し、このような環境下でのソフトウェア開発支援のために、開発状況を保持する情報リポジトリを用いて漸進的に情報の矛盾や不確実さの解消を行うモデルを提案し、それに基づく支援環境を構築した。中田は、スライディングウィンドウを持つ計算機の命令レベルの並列化のために、ループのソフトウェアパイプライニングのレジスタ割付方式としてスパイラルグラフを提案した。また、コメントの処理などに必要とされる字句解析器の最短一致法を開発した。佐伯は、再利用プロセスの形式化をユースケースのパターン化とその構造変換規則として行った。分析パターンや設計パターンの構造をパターン化し、必要に応じてホットスポットを埋める手法を提案した。また、ソフトウェアアーキテクチャをカラーペトリネットで形式化し、非機能要求の検証を可能とした。

著者

阿草 清滋 坂部 俊樹 小谷 善行 大岩 元

出版者

名古屋大学

雑誌

重点領域研究

巻号頁・発行日

1991

---

より高度なシステムの仕様化を支援するために,継承により階層化された代数的仕様の直接実現による検証,代数的仕様の類似性の定義とそれに基づく仕様ベ-スについて研究を進めた.また,プログラム理解のモデルを定義することによりソフトウェアの開発・保守に有効なソフトウェアデ-タベ-スを開発した.その他,文書執筆協調作業の作業割当問題を定義し,その近似解を高速に求めるアルゴリズムを提案した.ユ-ザ主導の対話システムとして,自由知識獲得システム第2版の作成と評価を行った.これは対話を通しテフレ-ム構造の知識を集積していく創造性開発指向の教育ツ-ルである.また,ソフトウェア(要求)仕様獲得するシステムの概念設計を行った.これはこの自由知識獲得システムにソフトウェアや仕様の枠組みを与えたもので構成され,仕様を獲得するとともに,利用者に仕様を自動的に意識化・具体化させるものである.前年度に作成した仕様形成のためのカ-ド操作ツ-ルKJエディタのワ-クステ-ション版を完成させた.また,いくつかの機能拡張を加えたパソコン版を実際のソフトウェアの仕様作成に適用した.要求分析の途中経過を示すカ-ド配置は,思考過程の記録としてその内容を把握し易く,エディタが仕様作成のツ-ルとして有効であることが知れた.要求仕様の直接実行による検証の理論的モデルとして,動的項書換え計算(Dynamic Term Rewriting Calculus,DTRC)について研究をすすめ,停止性と合流性に関するいくつかの結果を得た.また,値表現の体系として項書換え系を含むCCSを提案し,テスト正確度という新しい概念に基づく意味論について検討した.さらに,ブロ-ドキャスト通信機構を持つ並行プロセスの体系としてCCS+bを提案し,並行演算,選択演算の結合則と可換則,ならびに,展開則が成立することを示した.