Model-Checking Real-Time Control Programs - Verifying LEGO Mindstorms Systems Using UPPAAL
LEGO Mindstroms 上で動くプログラムを UPPAAL で検証したという論文。スケジューラのモデル化と、NQC 用の API のモデル化を行ってプログラムを全部時間オートマトンに変換して UPPAAL でモデル検査する。
author="Torsten K. Iversen and K{\aa}re J. Kristoffersen and Kim G. Larsen and Rune G. Madsen and Steffen K. Mortensen and Paul Pettersson and Chris B. Thomasen",
title = "{Model-Checking Real-Time Control Programs -- Verifying LEGO Mindstorms System Using UPPAAL}",
booktitle = "Proc. of 12th Euromicro Conference on Real-Time Systems",
publisher = "IEEE Computing Science Press",
pages = "147--155",
year = "2000"
Verification of the legOS Scheduler using Uppaal
legOS のスケジューラは固定優先度方式で優先度の高いタスクから処理するため、優先度の低いタスクにプロセッサが割り当てられない飢餓状態が発生する可能性がある。このことをUPPAALで確認して、解決策として長く実行されないタスクの優先度を徐々に高くするスケジューラを実装しましたという論文。
author="Lone Halkjaer and Karen Haervi and Anna Ingolfsdottir",
title="{Verification of the legOS Scheduler using Uppaal}",
journal="ENTCS",
volume="39",
number="3",
pages="273--292",
year="2000"
On the Semantics of Software Adaptation
10 日前の A Formal Approach to Component Adaptation の理論面について議論している…ことになっているがどうにも不完全燃焼な感じ。
author="Antonio Brogi and Carlos Canal and Ernesto Pimentel",
title="{On the Semantics of Software Adaptation}",
journal="Science of Computer Programming",
volume="61",
number="2",
pages="136--151",
year="2006"
muABC: A Minimal Aspect Calculus
アスペクト指向を形式的に扱うための体系の導入と、既存のアスペクト指向言語からの変換、およびπ計算の変種へのエンコーディングの話。Extended abstract を読んだけど、よくわからない点が多いので full version も読んだほうがよさそう。
# Full version を refer しているけど、書いてある URI に見つからないので困る。
author="Glenn Bruns and Radha Jagadeesan and Alan Jeffrey and James Riely",
title="{$\mu$ABC: A Minimal Aspect Calculus}",
booktitle="CONCUR 2004",
volume="3170",
series="LNCS",
publisher="Springer",
pages="209--224",
year="2004"
A Formal Approach to Component Adaptation
これも形式手法を用いた component adaptation の話。前に挙げた論文と著者が一部同じ。コンポーネントのインタフェースと振舞いをπ計算で書いて、接続したいコンポーネントのインタフェースのマッピングを与えるとアダプタが自動生成できて、生成されたアダプタと接続したいコンポーネントを並行合成してもデッドロックフリーで、かつ与えた通りにマッピングされています、っていう展開。でも自動生成手法が省略されているので本当に主張どおりか確かめられず面白くない。主張も例が中心でまったく形式的に展開されないのでそのまま信じていいのか不明。
author="Andrea Bracciali and Antonio Brogi and Carlos Canal",
title="{A Formal Approach to Component Adaptation}",
journal="The Journal of Systems and Software",
volume="74",
number="1",
pages="45--54",
year="2005"
A Calculus of Untyped Aspect-Oriented Programs
アスペクト指向プログラミングを形式化したという話。AspectJ のようなアスペクトを記述する仕組みを持つ言語の意味論を定義し、さらに weaving を class-base な言語への変換として定義。その上で weaving が reduction によって壊されないことを示した。ただし、pointcut としてメソッドの call と execute のみを扱っている。
author="Radha Jagadeesan, Alan Jeffrey, and James Riely",
title="A Calculus of Untyped Aspect-Oriented Programs",
booktitle="Proceedings of the European Conference on Object-Oriented Programming",
volume="2743",
series="LNCS",
publisher="Springer",
pages="54--73",
year="2003"
追記(2006/11/02)： 同じ著者による A Typed Calculus of Aspect-oriented Programs というのもある。こっちは型付き。
Component Adaptation through Flexible Subservicing
Component adaptation の話をプロセス代数の世界で展開している。インタフェースが異なるコンポーネントをどのようにして接続するかという話。コンポーネントのインタフェースと動作をπ計算ライクなプロセス代数と session type を使って記述して、インタフェースのマッピングをチャネル名のマッピングとして与えることで、2 つのコンポーネントの間をつなぐ bridge を自動生成する。Bridge が正しく生成されていれば deadlock-freeness が保証される。
author="Antonio Brogi and Carlos Canal and Ernesto Pimentel",
title="{Component Adaptation through Flexible Subservicing}",
journal="Science of Computer Programming",
volume="63",
number="1",
pages="39--56",
year="2006"