著者

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

出版者

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

雑誌

情報処理学会論文誌プログラミング(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.

著者

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

出版者

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

雑誌

情報処理学会論文誌プログラミング(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.

著者

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

出版者

情報処理学会

雑誌

情報処理学会論文誌 (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.