qm劇
NewsJetterfromSoftwareEnglneerSAssociation

vbl．14，N。mber8Ma，Ch，2006

目

次l

第4回デザインワークショップ（DW2005）
つ

山崎利治

佐原伸

5

ワークショップ参加報告

J

DW2005の演習問題

一
ヽ
J
h

張暁晶

5

ワークショップ参加報告

′

重囲隼人

5

ワークショップ参加報告

5

野中菅

4

三好健吾

5

ワークショップ参加報告
DW2005課題の回答

3

山崎利治

0

2

課題「電子錠物置」について

U

4
7
U

伊藤昌夫

9

伊藤昌夫

Promela簡介

2

PromelaおよびSpinについてのノート

4
O
ノ

5

今後のSEAForumの予定

0
∩

L

フ

U

編集後記

／

ノ

SS2006in熊本での新しい試み

ソフトウエア技術者協会
SoftwareEngineersAsociation
ソフトウェア技術者協会（SEA）は，ソフトウェアハウス，コンピュータメ一九

計算センタ，エンドユーザ，大学，研究所など，それぞれ異なった環境に置かれているソフトウェア技術者または研究者が，そうした社会組織の壁を越えて，各自の経験や技術を日射二交流しあうための「場」として，1985年12月に設立されました．
その主な活動は，機関誌SEAMAILの発行，支部および研究分科会の運営，セミナー／ワークショップ／シンポジウムなどのイ

ベントの開催，および内外の関係諸団体との交流です．発足当初約200人にすぎなかった会員数もその後増加し，現在，北は北海
道から南は沖縄まで，350余名を越えるメンバーを搾するにいたりました．法人賛助会員も17杜を数えます．支部は，東京以外に，関西，横浜，名古屋，九州，広島，東北の各地区で設立されており，その他の地域でも設立準備をしています．分科会は，東京，関西，名古屋で，それぞれいくつかが活動しており，その他の支部でも，月例会やフォーラムが定期的に開催されています．
「硯在のソフトウェア界における最大の課題は，技術移転の促進である」といわれています．これまでわが国には，そのための適切な社会的メカニズムが欠けていたように思われます．sEAは，そうした欠落を補うべく，これからますます活発な活動を展開して行きたいと考えています．いままで日本にはなかったこの新しいプロフェノショナル・ソサイエティの発展のために，ぜひとも，あなたのお力を貸してください．

代表幹事： 田中一夫

常任幹事： 荒木啓二郎 熊谷章 高橋光裕 玉井哲雄中野秀男
幹事：

石川雅彦

清水浩一郎 窪田芳夫 蔵川圭 小林修 小林允 近藤康二
桜井麻里 酒匂寛 塩谷和範 篠崎直二郎 新谷勝利 新森昭宏 杉田義明
鈴木裕信 中来田秀樹 奈良隆正野中菅 野柑行憲 野呂昌満 端山毅
平尾一浩 藤野誠治・松原友夫 渡達雄一

事務局長： 岸田孝一

会計監事： 吉村成弘 橋本勝
分科会世話人

環境分科会（SIGENV）：塩谷和範 田中慎一郎 渡達雄一
教育分科会（SIGEDU）：君島浩 篠崎直二郎 杉田義明 中園順三
ネットワーク分科会（SIGNET）：人見庸 松本理恵
プロセス分科会（SEA−SPIN））：伊藤昌夫 塩谷和範 新谷勝利 高橋光裕 田中一夫 端山毅 藤野誠治
フォーマルメソノド分科会（SIGFM）：荒木啓二郎 伊藤昌夫 熊谷章 佐原伸 張漢明 山崎利治
オープンソース分科会（SIGOSS）：石川雅彦

支部世話人

岸田孝一

杉田義明

鈴木裕信

中野秀男

関西支部：小林修 中野秀男 横山博司
横浜支部：野中哲 藤野晃延 北條正顕

名古屋支部：石川雅彦 角谷裕司 野呂昌満
九州支部：荒木啓二郎

武田淳男

平尾一浩

広島支部：佐藤康臣 谷純一郎
東北支部：布川博士 野村行書
賛助会員会社：ジェーエムエーシステムズ
オムロンソフトウェア

ダイキン工業
リコー

オムロン

NTTデータ

SRA西日本

キヤノン

新日鉄ソリューションズ

富士電機

ヤマハ

SRA東北

SRA PFU

ブラザー工業

オープンテクノロジーズ

エフビクス（以上17社）

SEAMAIL

Vol．14，No．8

2006年3月25日発行

編集人岸田孝一

発行人ソフトウェア技術者協会（SEA）〒160−0004

東京都新宿区四谷3−12

T：03−3356−1077F＝03−3356−1072

印刷所市田印刷株式会社

定価

丸正ビル5F

E−mail‥Sea＠sea．orjp〒114−0014

500円（禁無断転載）

URL：http：／／www．sea．jp／

東京都北区田端2−3−25

WorkshopReportⅥ）1．14，No．8

平成17年02月24−26日

第4回デザインワークショップ

ソフトウエア仕様検証技術の最新動向
PROMELA／SP川を用いてスケジュール：
2月24日（木）
1330

受付開始

1400−1430

あいさつ，案内，その他

1430−1530

Promela模型を作るために（1）1530−1600

お茶1600−1700

Promela模型を作るために（2）

1800−

夕食＋雑談

2月25日（金）930−1030

基礎をすこし1030−1100

お茶

1100−1200

SPINで検査を1200−1300

昼食

1300−1700

演習

1800−

夕食

2月28日（土）930−1200

成果報告

感想と討論（SP川

Promela DW2005批判など）．1．

WorkshopReport

Vol．14，No．8

デザインワークショップ

DW2005「ソフトウエア仕様検証技術の最新動向−−PROMELA／空し牡を用いて」

主催：ソフトウエア技術者協会
異なるプロセスがあり，それぞれが通信することで構成されるシステムを如何に設計するかは，昔から議論されてきた話題です．但し，かつては一部の人たちの知識や経験だったものが，現在では多くのソフトウエア設計者が身に付けておくべき技術となりました．組込みシステムや，分散システムが一般化したことが理由として挙げられます．
今E］は，室賀牡というLTLとCSPに従った模型検査が可能なツールを利用する
ことで，日頃の我々の設計作業の中で生かし，より安全で信頼性の高いシステ
ムを作るための手段と方法について議論したいと思います．
以下は，GeneralDescriptionにある概要（のごく最初の部分）を訳したもので

Sp叫ツール】は，効率的なソフトウエアの検証を目指しています（ハードウエア検証ではありませんトツールはシステムの仕様を記述するための高次の言語PROMELA（aPROcessMEta
LAnguage）を使用します．Spinは，分散システムの設計における論理的な設計上の誤りを見つけ出すために用いることができます
具体的な例としては，基本ソフトウエア，データ通信プロトコル，
交換システム，並列アルコリズム，鉄道信号プロトコルといったものを挙げることができます．ツールは仕様における論理的な一貫性を検査します．デッドロック，仕様化されていない【イペン卜の】受け取り 不完全なフラグ，競合状態，プロセスの相対的な速度についての保証されていない仮定について，ツールを通して知ることができます．

課題となる問題を用意して、実際に仕様を記述し、SPINで仕様のチェックするという実習を行います．できるかぎり，SPLNのインストールされたPCをご持参下さい．
日時：2005年2月24日一26日（2泊3日）土曜日昼解散

場所：ウエルハートピア熱海（厚生年金ハートピア熱海）
http：／／www・kjp・Or・jp／hpT9＿9！

定員：15名．2．

Vol．14，No．8

ⅥbrkshopReport

DW2005のための問題（山崎利治さん作成）

ご利用に際してあなたの物置番号は125です．いま扉は閉まっていて施錠してあります（施錠灯が点いています）

唇庖丁﹂妻⊥胃や

0『｛■
搬鶴野

漉帝鞋

1

2

3

4

5

6

7

8

9

C

O

L

図1．物置
物置番号の書かれた物置の扉にはパネルがあり，そこに，施錠灯0から9までの押ボタン，C，しの押ボタン・
10進数字4桁の液晶表示窓，90度回転する取っ手が付いています．

扉の開けかた（1）数字ボタンを1234（施錠鍵といいます）と左から順に押してください・（2）押した数字を表示窓で確認してください．
（3）それが1234であれば施錠灯が消えます（開錠）．
（4）そこで扉の取手を時計回りに90度廻して手前に引けば扉が開きます・（5）数字ボタンを押し間凍えたときは，Cボタンをおして，始からやり直してください（Cボタンを押すと表示窓の数字が消えます）．

・3・

WorkshopReport

ⅥIl．14，No．8

扉の閉めかたと施錠（1）扉を閉め取手を逆時計回りに90度廻します（磯城的な施錠）．
（2）Lボタンを押します（電子的な施錠）．
（3）ここで施錠灯が点きます（直前に扉を開けたときのあるいは，次項によって変更した鍵による施錠）．
（4）その後は開錠手続きをしない限り，取手を廻して引いても扉は開かないはずです．

鍵の変えかた
施錠灯が消えているときに，つぎのようにして好みの鍵にすることができます．

（1）数字ボタンを4回押す．この4数字が新しい施錠鍵になりますので必ず表示窓で確認の上ご
記憶ください．
（2）ついでLボタンを押します．そこで鍵が登録され，表示窓の数字が消えます．
以

．4＿

上

WorkshopReport

Vol．14，No．8

デザインワークショップ2005参加報告
佐原伸
日本フイツツ株式会社
情報技術研究所
TEL：03−3623−4683
shin．Sal1ara＠jfits．co．jp

2005年3月15日

た模型の検査をSPINで行ってみる」ことで、模型構築と模型検査の重要性を実感しよう了1というも概要のであった。

ソフトウェア技術者協会（SEA）主催のデザイ
ンワークショップ2005参加報告である。本ワー
クショップは、AT＆TのUNIXチームが開発し、NASAが全宇宙システムの開発に使用している模型検査（ModelChecking）言語Promelaとそのツー

ルSPIN聞【3】を使って、並行プロセスを持つシス

テムのモデル（以下、模型という）化とその検査を味見しようというものであり、極めて有意義だったので報告する。
なお、本ワークショップの報告はSEA機関誌
SEAMAILに掲載される予定で、6月のソフトウェ
アシンポジウム2005でも開運セッションが予定されている。

当日は、日本最初のプログラマーであり形式手法にも詳しい山崎利治さんより、基礎理論にも触れな
がら、簡潔で分かりやすい講義が4時間あり、2日日午後から3チームに分かれて山崎さん提示の演習
問題の模型構築に挑戦した。
各チームは。はじめての模型検査（modelcheck−ing）言語とツールに苦戦して、4時間の予定を大幅に超過し、事実上徹夜で模型構築を行ったが、全チームが翌朝までに模型構築および模型検査を完了した。

2．1講義要約
山崎さんの講義概要を以下に示す。
2．1．1

1ワークショップ日時・場所・参加者

なぜSPINか？

実時間分散システムは、多スレッド・プログラムになり、設計の誤りを起こしやすい。嫌み（dedlock）・

1．1

発散・仕様の過不足・制約違反などであるが、これ

日時

2005年2月24日（木）〜26日（土）1．2

らの誤りは模型検査（ModelChecking）によって発見できる。
他方、並行系でなくても、オブジェクト間相互作

場所

ウェルハートピア熱海（厚生年金ハートビア熱海）
1．3用、つまり、系全体の挙動の記述にPromela言語

参加者が利用できる。

（株）デンソ一、九州大学2名、九州工業大学、奈良先端大学、ニル・ソフトウェア（株）、（株）SRA
2名、フリーのソフトウェア技術者2名、佐原の11名。その内、（株）SRAの岸田氏はワークショッ
プの記録係のため演習問題には挑戦しなかった。

分間の協調、UMIJ相互作用図・交信図・時間図・状態図などの利用時に模型検査が利用できることに2開されていて使用実績も多く、毎年ワークショップが開催されていてノウハウを吸収しやすい環境がワークショップ要約

従って、Jm多重スレッド、オブジェクトや成なる。
SPINは、教科書や教育資料が多く、ツールが公簡易な電子錠システムの演習問題【8】と、ニル・
ソフトウェア（株）伊藤氏によるSPINのQuick■lpromelaは実システムそのものの仕様は書けず、模型のReferenceの翻訳【1】がワークショップl〜2ケ月

仕様，記述に限定することで、扱押！検禿を効率化している。

前に配布されていて予習できるようになっていた。

一方、VDM【6】【7】は動的な模型検査は手で行う代わりに、

ワークショップの目的は「Promela，言語で記述し．5・

実システムそのものの仕様を番くことができる。

WorkshopReportⅥ）1．14，No．8

整っている。

aBSertion violatlonS

2．1．2 模型検査とは？

＋（if vithi18COpQ Of clal皿）システムの有限状態模型とそれが満たすべき性
質を与え、自動判定する技術であり、システム検

non−prOgreBB CyCleS

証の一方法である。SPINでは、Promelaで模型を作成し、線形時間（時相）論理式IJrL（lineartime
temporallogiC）で模型が満たすべき条件を記述し、−（d18ablod by nQVer Clalm）

それをPromelaに変換して模型検査を行う。この検査は、かなり自動で行われるが、人手の介入も必要である。
2．1．3 時間論理式「「Lとは？

表1．時間演算子

pN9

Promela での表現

U（注）エラー検出
Sta．te−VeCtOr72byte．depth reachedlO5．error8：1−省略〜Ⅰ∬いま、通常の論理式を拡張して、時間を考慮した論理式を書けるようにしたものである。時間演算子には、以下のようなものがある。

時間演算 子＋（falm888diBabled）

invalld ond StatQ8（注）下記がエラーの状況
unreaCb8dln proctype BllttOn
lln096，8tat8105，日Lch！10Ck…
11m894，8tate120，MBch？D，d

意味

qがやがて真になり、それまではpがずっと真である

11m8

94，8tat0120，■■Bcb？L−1

11m0

94，8tat0120，■tBch？Ct

11ne33，8tate151，nD＿STEP＝
11nelO7，8tate159，日−endJ■（490f1598tateS）

◇p

＜＞p

pがやがて（未来のある時

点で）真になる

lmreaCbedln proctype Locklinel15，□p

Up

帳簿中の明細記録の総件数を返す

1in8117，（3

2．1．4 模型検査の手原

SPINによる模型検査の手順は、以下のようになる。

pan＿ln■㌧

State7，■■18＝1■

11m8114，何paェ＿inH，8tat09，I−Lcb？lockM
pan＿in，BtatQll，…−OndJ■

0董118tateS）

lmrOaCbedln proctypQ DoorllnQ130，−●pan＿in一㌧

8tate14，●●−QndJ（l of148tateB）●Promelaで模型を作る

lmrOaCbedin proctype uBer

●正当性を保証する仕様をmLで記述する

11n0141，●模型検査系SPINで検査する

1inQ142，●結果を分析する

11m8143，

結果の分析は、以下のように行う。

1ine144，●検査で、模型が仕様を満たせば、終了●満たさないときは、反例をSPINが表示するので、検討する

1ine149，●模型と仕様を再構成し、上記手順を繰り返す

11m8151，

11ne149，
1ine150，11m8152，

例えば、山崎さんの解答例で模型に嫌み（dead−lock）があるのをSPINツールが検出した例が下記である。

11m8154，1ine153，
1in。156，（Spln Version4・2・4…14Febmary2005）

11ne158，

Varning：Search not completed

11m8158，＋

Partial Order Reductlon

Hpa皿●in，●panJn，pan＿1n●1，■暮panJn ，
MpaLin●●，Hpan＿inH，Hpan」血■■，Hpan＿in，¶pan＿in■ ，−pan＿in■ ，
lpan＿inM，

11ne160，■一pan＿1nH，

1ine161，
1ino162，

11n8163，．6．

Hpan＿1が，1inQ157，（注）下記で＋で表されているのが検査した性賞＋

Hpan＿in■■，■−pan●in●1，

Fuil statespace BearCh for：never claim■ panJn●●，…pan＿1m■1，

pan＿in…，■■paムー1nM，8tat09，5tatelO，
Statell，

8tate12，8tatQ19，
8tate

20，

8tate

21，

Bta．t0

22，

Btate

23，

Btate

25，

8tate

26，

8tate

28，

8tate

30，

8tate

31，

Btate32，
8tat8
8tate

34，
35，

8tate36，8tat037，

ttBch！D，lH

HBcb！D，1●lBcb！D，11−■■Bcb！D，1…Bch！D，1＝prlntf（一Bend Dり
一喝cb！D，111

Bcb！D，1日■IBcb！D，1

lIDcb！OPENH
H（（18三三0））■■

川Bcb！D，9m
t】Bcb！L川

川prlntf（一閃nd Lり■（（dS＝コ0））…

Bch！D，8tl…Bcb！D，7I−
川Bcb！D，6日■LendJ■

WorkshopReport

（190f

37

Ⅵ）1．14，No．8

chan Bch＝［1】of（mtype，Short）；

BtateS）

ⅥnreaCbedln proctypo：inlt：chan Dch＝［0】of（mtype）；（l ofl18tateB）

Clmn Lch＝［01of（mtype）；

0．12real O・01118er O・06syS

boolls

上記のテキスト形式だけでは、見にくいので、

r＝true，ds＝＝false，

falSe；

ページ15のような交信図も自動的に表示され、どshort K【N】，Ks【N1，d，W；

こでおかしくなったかが分かるようになっている。

bytei；

図の例では、一番右側のuserプロセス（98ステップ目）から、左側から2番目のButtonプロセス（106inline new（）t

ステップ目）にメッセージL（鍵を掛けるためのメッ

d＿Step（セージ）がチャネルを通して送られ、そこで嫌み

i

＝

0；

do

（deadlock）が発生していることが分かる。

：：i＜N

このような模型上の欠陥を修正していけば、模型：：i

検査が終了することになる。

−＞K【il＝−＞−1；i十十breakod

山崎さんの講義は、基礎理論にも触れながら、初心者が演習するための上記内容をわずか4時間で伝えるという優れたものだった。

））

inline ass（）／＊

以下、模型検査終了まで何とか達成した演習の状

neW key ass亀gnf＊／（

況を報告する。
2．2＝Nd＿Step f
i

演習要約

＝

0；

do

我々のチームの場合は、山崎さんもメンバーだったのと、残りの3人の自力では4時間で模型検査終山崎さんの模型のPromelaソースを以下に示す。
山崎利治さんの模型

inlinein（d）
id＿Step（assert（！complete）；＊／

i

雛Iefine N4＃define complete（Kl01！＝
御efinelockingls

＝

−1）

false

＝

：：i＜（N−1）−＞K【il＝K【i＋11；i＋＋

i＝（N−1）−＞（ls＝true）

Od；＃define unlocked（ls＝false）

K【N−1］＝d＃define opening ds＝true＃define closing ds＝

）

false

＃define opened（ds＝true）

0；

do

＝true

＃define unlockingls＃definelocked

break

）

のGUIツールで検査した。

e−Jocたer

−＞

＝N

）

の解答例をXSPINというⅩ一Windowシステム上／＊−＞Ks【il＝K【i】；i十十i

od

了までは到底無理そうとの判断から、まず山崎さん

Listingli＜N）

耕lefine closed（ds＝false）＃define matched（r＝true）

inline eq（）（

mtype＝（D，L，C，OPEN，CLOSE，lock，uTllock）；

bool rr；dTStep t

breakWorkshopReport

rr

＝

i＝

0；

Ⅵ）1．14，No．8

true；new（）；gOtO S3：：Bch？L（W） −＞dogoto s4

：：i

＜N

ri

一＞

rr＝rr＆＆（KS【i】＝K【i】）；

fi

i十十
：：i

）

＝N

一＞

break

Od；
r

＝

proctype Lock（）rri
lsl：ir）：：Lch？unlock）−＞

unlocking；gOtO182
fi；

proctype BllttOn（）

182：ir

（

end：
Sl‥

：：Lch？lockneW（）；−＞

locking；gOtOIsl

iffi：：Bch？D（d）−＞in（d）；gOtO S2‥‥

Bch？L（W）−＞）

goto sl＝：Bch？C（W）−＞goto sl

proctype Door（）

ri；

f

S2：ir

dsl：ir：：COmplete−＞：：Dch？OPEN一＞

eq（）；

if

if

：：r ＝ true：：unlocked−＞

opening；gOtO ds2：：Dch？CLOSE−＞

closing；gOtO dsl−＞

progressl＝fi

Lch！ulllock；gOtO S3

r＝false

−＞

goto

sl

ri；

ri

ds2：if：：e18e−＞if：：Bch？D（d）−＞in（d）；gOtO S2‥‥

Bch？C（W）−＞

goto sl＝

Bch？IJ（W）−＞

goto s2ri）

ri

proctype uSer（）fi；（

Bch！D（1）；S3：if‥＝ Bch？D（d） −＞Bch！D（2）；
Bch！D（3）；new（）；in（d）；gOtO S4：：Bch？L（W） −＞Bch！D（4）；progress2‥

if

Lch！lock；aSS（）；：：unlocked

goto sl：：Bch？C（W） −＞−＞Dch！OPEN

ri；

Bch！D（1）；goto s3fi；

Bch！D（1）；

S4：if

Bch！D（1）；：：COmplete−＞：：else−＞if：Bch？D（d）

goto s3

Bch！D（1）；Dch！CLOSE；

T＞

ir

in（d）；gOtO S4：：Closed：‥ Bcl17C（W） −＞−＞Bch！L（W）；primtf（．8．

senduLl）；

WorkshopReport

Vol．14，No．8

l

D

B

l

D

l

C

ln

D

B

ln

C
C

ln

B

l

D

C

B

f

i

︶ ︶ ︶ ︶

l

・−．m

︐

f

張すれば良いと判断したためである。
primtf（sendJ））；

以下が、その縮小模型のPromelaソースである。

Listing2

佐原の簡易版模型／＊g￡ore E−ムocたer＊／：：unlocked−＞

Dch！OPEN

fi；

Short key，digit
boollockStatus，doorStatus

Bch！D（9）；ir：：Closed−＞

Bch！L（W）；printf（

send＿L）＃definelockinglockStatus＝true＃define unlockinglockStatus

＝

false

＃definelocked（lockStatus＝true）

fi；＃define unlocked（lockStatus＝falSe）

Bch！D（8）；＃define opening doorStatus

Bch！D（7）；雛Iefine closing doorStatus

Bch！D（6）；＃define opened（doorStatus＝true））＃define closed（doorStatus＝false）

＝true
＝

false

＃defime matched（key＝digit）
init

mtype＝（D，OPEN，CLOSE，lock，unlock）（

d−Step（Ks【0】＝1；

Chan ButtonCh＝［1】of（mtype，Short）；

Ks【11＝2；

Chan LockCh＝［0】of（mtype）；

Ks【21＝3；

Chan DoorCh＝［0】of（mtype）；

Ks【3】＝4；
imit）；

atomic t（run BllttOn（）；run Lock（）；

key＝1；

run Door（）；run uSer（）atomic（rum User（）

）
）

）
）

結果は前記の通りであるが、山崎さんを含め
XSPINツールには誰も習熟していないため、欠陥を修正するには至らなかった。■2proctype User（）f

ButtonCh！D（1）；printf（

そこで、プロセスの数を減らして＊3欠陥の修正を容易にすることと、錠と取手それぞれの開閉のみを

tryuunlockl）；

if：：unlocked

行う縮小した模型を構築することにした。山崎さん−＞

DoorCh！OPEN；の解答例レベルの模型は、縮小模型ができてから拡

printf（try−door−Openl）ri；＊2ヮークショップ後に見直したところ、模型は、Bdに引数があるメッセージと引数の無いメッセージを送っていたのだが、引数の無いメッセージを送ったときに前の引数が残っていて、その受け手がいないため嫌んでいることが発見できた。そこで、引数の無いメッセージにも使わない引数を付けたところ、模型のエラーは無くなった。
＊3プロセスが多いと再利用性は増えるものの、閃掛こ合まれない余分な並行性も発生するため、初心者には予期できない模型の動きが多発するので、欠陥修正が難しい。

DoorCh！CLOSE；printf（

tryuclosel）；

ir：：Closed−＞printf（tryulockillg）；LockCh！lockri；

ButtonCh！D（1）；printf（

ir：：unlocked−＞

try−unlock2）；

WorkshopReport

Ⅵ止14，No．8

DoorCh！0円宣N；
printf（try−dooruopen2

）

fi
）

active proctype Ctrl（）（

lockS：

ir：：BllttOnCh？D（digit）−＞

if：：matChed

この模型の最後から14行目のnever以降は、否−＞

printf（：：elSeunlocking）；gOtO CloseS

定要求（neverclaim）といって、検査仕様のIXL−＞式から生成された仕様である。ここでは「鍵が掛gotolockS

かっていたら（loecked）いつかは鍵が開けられるfi
ri；（unlod【ed）」という命題に反することはない、すな

closeS：

わち「鍵が閲かなくなる」ことは絶対にないことがir：：LockCh？lock

保証される。
つまり、検査したいことを否定要求として記述す−＞printf（locking）；

ることで、「起きて欲しくないことは起きない」とgotolockS：：DoorCh？OPEN

いう保証が得られる訳である。

−＞

Opening；printf（

opening）；

最後の模型は、最終日午前中の発表の45分前にgoto openS；書き始めた。ここに至るまでに、3つの模型を書き

fi；

OpenS：（内一つは動かず）、大きな修正を5回行ったため、

ir

ほぼ徹夜となったが、そのおかげで、Promelaと：：DoorCll？mE−＞

XSPINにある程度習熟し始めたのである。

closing；printf（

closinglocked）；3

goto closeS

VDM模型との比較

fi；

実は、ワークショップの前と後で、演習問題の）VDM＋＋【5］による模型を作っていた。VDM十十による並行処理模型の作り方にはまだ習熟していな／＊＊

Form≠h Aβ

＊

OChd

＊

me

＊

To

rypedご−＞＜＞ⅣelJer CJαim
717もe

いし、まずは並行性を排除した模型で正しさを確認

むnJocたed

すべきだというVDMTboIsの生みの親LarSen博

βeヱ0u Corre叩Omdβ

士の文書【41を信じて、節3・1のようなVDM＋＋〃印α孟ed Form餌gd

模型を作った。
／rJocんed−＞＜＞ungOCたedノ

VDM＋＋には習熟しているので、この模型は「鍵rJormαg豆Z篭れダリ乳OJα七号071β＊

OJの押し間違えの修正」機能を除いて、ほぼ問題文に拍e or綾乃αり

忠実に作った。

＊／

結果として、SPIN模型では発見できないであろneveri／＊／r ochd−＞＜＞う5個の誤りを発見した。いずれも、事後条件の間
umJocたedノ＊／違いである。

accept＿init：

SPINは並行プロセスの状態遷移に内在する矛盾

TO＿init：．10．

Ⅵ）1．14，No．8

ⅥbrbhopReport

検出に役立ち＊4、VDM十十は状態遷移したときの動作（操作や関数）に必要な制約（事後条件）を明確化するのに役立つ。

3．1佐原のVDM＋＋模型●4ただし、鋸火の問題では「状態の触発」がiJ′ほ、恥史上検査ができなくなるので、模型簡易化（modelslicing）を行

うことによって、状態数を減らす必要がある。

．11．

WorkshopReport

3．1．1

Vol．14，No．8

施錠鍵を登録する：「鍵」ユ（）
施錠鍵を登録する（α鍵）仝

Store

Storeは、電子錠の付いた物置で、かつ、そのテスト用のクラスである。本来は、テスト機能は別クラスに分離（表示窓．ボタン列を設定する（α鍵）；
ボタン．ボタンを設定する（ムボタン）；

すべきであるが、手を抜いた。

錠．登録する（）

newStore（）．testOとすることで、想定した全てのテストを行う。

）；

以下はテスト機能である。

ClassgoreissubClassof∬eyCommOn

instancevariables

Publk

publk錠：『錠』：＝neW『錠』（）；

土eβ±‥（）ヱ取public取手：『取手』‥＝neWF取手』0；

紬扇0仝

pubHC施錠灯：『施錠灯』：＝neW『施錠灯JO；（returnfl（）∧￡2（）∧f30∧ま4（）∧ほ（）∧上60

publk表示窓：『表示窓』：＝neW『表示恵』（）；
publkボタン‥『ボタン』：＝neW『ボタン』（）；

）；

PUblk

f1：（）ユ迅

OPeration5

fl（）仝

九記‥（）エ0

血克0仝（ 血叫）；
解錠する（【1，2，3，41）；（取手Jm呵施錠灯）；

return施錠灯．消えている（）錠．九呵施錠灯，取手，表示窓，ボタン）；
施錠灯点ける（）；
取手を閉める0；
表示窓．消す（））；

PUblic￡2：（）ヱ取は（）仝

）；（ 九扉（）；

PubliC解錠する：「鍵」ヱ（）解錠する（α鍵）仝

解錠する（【1，2，3，4］）；

取手を開ける（）；
return施錠灯．消えている（）∧（表示窓．ボタン列を設定する（α鍵）；

取手．開いている0錠．解錠する（）
）；

）；

PUblk

PUbIicは：（）ヱ隠施錠する：（）ヱ（）施錠する（）仝

士3（）仝

（ 九虎0；（ ボタン．ボタンを設定する（エボタン）；錠．施錠する0

解錠する 1，2，3，4】）；

取手を開ける（）；）；

施錠鍵を登録する（［1，9，1，9】）；Publicreturn施錠灯．消えている0＜

取手を開ける‥0ヱ（）

取手を開ける（）仝取手．

錠．鍵が一致（【1，9，1，9】）

開く（）；

）；

PublicPUblic

取手を閉める：（）ユ（）
取手を閉める0仝取手．
閉める0；
Publk

．12．

WorkshopReportⅥ）1．14，No．8

f4：（）ヱ迅

りPeS

t4（）仝

publk「鍵」＝即end〝eyCommom（ 九虎（）；
解錠する（［1，2，3，41）；

3．1．3

取手を開ける（）；
施錠鍵を登録する（【1，9，1，9】）

取手を閉める（）；
施錠する（）；

F錠』

電子錠である。
class『錠』issubclassofgeyCommom

instanCe Variables

publk施錠鍵：「鍵」；

return施錠灯．点いている（）∧publk取手：『取手』；

表示窓．消えている0

publk施錠灯：『施錠灯』；）；

publk表示窓：『表示窓』；

PUblicpublkボタン：『ボタン』；
f5‥0ヱ迅inv正しい鍵（施錠健）ほ（）仝
（ 九呵）；

functions

解錠する（【1，2，3，4】）；

PUblicstatic

取手を開ける（）；

正いゝ鍵：「鍵」→迅

施錠鍵を登録する（【1，9，1，9］）

正しい鍵（α鍵）仝

取手を閉める（）；
施錠する（）；
解錠する（［1，9，1，91）；

Ienα鍵＝鍵桁数postIenα鍵＝鍵桁数
OPerations

PUblk

return施錠灯．消えている（）＜

鍵が一敦：「鍵」ヱ取取手．閉まっている0

鍵が一敦（α鍵）仝
return施錠鍵＝α鍵；）；

PubliCPub‖C

f6：（）ヱB

九記：『施錠灯』×『取手』×『表示窓』×『ボタ

f6（）仝

ン』ヱ（）

（ 九虎（）；

丸正（α施錠灯，α取手，α表示窓，αボタン
解錠する（【1，2，3，4】）；

取手を開ける0；）仝（施錠鍵：＝［1，2，3，41；

施錠鍵を登録する（【1，9，1，91）；

取手を閉める（）；
施錠する（）；

施錠灯：＝α施錠灯；
取手：＝α取手；
表示窓：＝α表示窓；

解錠する（［1，9，1，9］）；

ボタン：＝αボタン

return施錠灯．消えている（）∧）；

取手・閉まっているO publk『錠』：（）ヱ『錠』）『錠』（）仝

end gね7℃

3．1．2

KeyCommon（

共通の型や値を定義する。
Class打eyCommOm

returnSelf）；

PUblic『錠』：「鍵」ヱ『錠』

vahes『錠』（α鍵）仝

PUblk

鍵桁数＝4；（施錠鯉：＝α鍵；
return self

PUblk
エボタン＝ エ ；）Pre正しい鍵（α鍵）；PUblic

Cボタン＝，C，

PublicWorkshopReportⅥ）1．14，No．8

施錠する：（）ユ（）
施錠する（）仝

点ける：（）ユ（）

点ける（）仝
点灯：＝trUePOSt点いている（）；（if取手．閉まっている（）then（表示窓．消す（）；

PUblk

施錠灯．点ける0

消す：（）ユ（）消す（）仝

）elseSkip

点灯：＝bIsepost消えている（）；
Publk

）

点いている：0ユ迅

Pre

表示恵点いている0 ∧ 施錠灯消えている0 ∧

点いている0仝

取手瀾まっている（）∧ボタン．エ（）

retum点灯post点灯；
PUbHC

POSt

消えている‥（）ヱ取

表示窓潤えている（）∧ 施錠灯．点いている（）＜
取手・閉まっている（）；

消えている（）仝
returnr点灯postr点灯

end F施錠灯』

Publk

解錠する：（）ヱ（）解錠する（）仝

3．1．5

F表示恵』

cbss『表示窓』issubdassofgeyCommom（if表示窓・点いている（）＜鍵が一致（表示恵・内容）∧正しい鍵（施錠鍵）

instancevariables

PUblk内容：「鍵」：＝【】；

then（表示窓．消す（）；

施錠灯消す（）OPerations
PUbHC

elseskip

設定する：rボタンJ 「ボタン」ユ（）設定する（αボタン）仝

）Pre

表示窓．点いている0

iflen内容≧鍵桁数

施錠灯・点いている（）∧正しい鍵（施錠鍵）

thenskip

else内容＝＝内容へtαボタン】
POSt

Pre『ボタンj

表示窓・消えている（）∧施錠灯．消えている（）；
PU帥C

POSt

登録する：（）ヱ（）登録する0仝
施錠鍵：＝表示窓，内容Pre

iflen内容≧鍵桁数
then内容＝内容
else内容＝内容へ【αボタン】；

表示恵点いている（）

以下の操作は、ボタン列の最後から鍵桁数分だけを内施錠灯・消えている（）∧ボタン・エ（）

容に設定する。Dropは、自作ライブラリで定義されている関数で、Drop（n）（列）と呼ぶと、列から頭のn個を削POSt除した列を返す。

鍵が一致（表示恵．内容）

PubHC

endr錠』

3．1．4

数字（αボタン）

ボタン列を設定する：FボタンJ『施錠灯d「ボタン」＊ヱ0

ボタン列を設定する（αボタン列）仝

dassr施錠机issubclassof〝eyCommon
instanCeVariables

内容：＝且甲はmCe

PUblic点灯：取；

肋叩【N】

（

len内容＋lenαボタン列一

鍵桁数）

OPerations

PUblk

（

内容へαボタン列）．14．

WorbhopReportⅥ）1．14，No．8

エ‥（）ヱ恥pre『ボタン』 数字列（αボタン列）エ（）仝
return内容＝エボタン；

POSt

内容＝

PUblk
ダ方querCe

ボタンを設定する：「ボタン」一㌔（）

肋叩［N】

ボタンを設定する（αボタン）仝

（内容：＝αボタン

Ien内容＋knαボタン列一鍵

end『ボタン』

桁数）

3．1．7

（

F取手J

Class『取手』issubdassofgeyCommom

内容へαボタン列）；

instanCeVariables

PUbliC

消す＝0ユ（）PUbHC開閉：取：＝ねlse；

消す（）仝

publk施錠灯：『施錠灯』；

内容：＝□post消えている0；
OPerations

PUblk

PUblic

点いている‥0ヱ取血豆Z：『施錠灯』ユ0点いている（）仝

九記（α施錠灯）仝

return内容≠ロpost内容≠□；

施錠灯：＝α施錠灯；

Publk

消えている：（）ヱ皿

PU鋸⊂

開く：（）ヱ（）開く（）仝

消えている（）仝
return内容＝OpoSt内容＝n

if施錠灯J消えている（）end『表示恵』

then開閉：＝trUe

3．1．6 Fボタン」

else開閉：＝bkepostif施錠灯消えている（）clasS『ボタン』issubclassof打eyCom7乃0m

then開閉＝trUe
りPeS

else開閉＝bIse；
publk「ボタン」＝阿lChar

invボタン仝数字（ボタン）∨

ボタン

∈

PUblk

閉める：（）ヱ（）閉める（）仝

（ C ， 上 ）instancevariables

開閉：＝ねIsepost閉まっている（）；publk内容：「ボタン」：＝，上，；
PUblk

開いている‥（）ヱ皿

funCtions

開いている（）仝
PublicStatic

return開閉post開閉；

数字：「ボタン」一十皿

数字（αボタン）仝
αボタン∈（0，‥．，9）；

PUblk

閉まっている＝（）ヱ皿

閉まっている（）仝

PUblicstatic

数字列：「ボタン了一→恥

数字列（αボタン列）仝
∀あ∈elems・αボタン列・数字（あ）
OPerations

PUblk

C‥（）ヱB

C（）仝
return内容＝Cボタン；
PUblk

retumr開閉postr開閉

end『取手』

WorkShopReport

Vol．14，No．8

が、今回のワークショップの意義を表している。

4

まとめ

並行処理プログラムの作成は、開発現場で行われているような、経験や根性といった「体で覚える」

4．1他チームとの比較
最終日の発表と討議により、他チームの進め方や方式の開発では、必ず欠陥が発生することを実感し考え方あるいは失敗から、良い教訓を学ぶことがでた。理論と定理と、それらを支援する言語とツールきた。

を使い、その上に立脚した経験をもとに開発するこ

例えば、伊藤さんのチームは、以下のようなしっかりしたプロセスで模型作成を行い、他人に開発過とが必要だろう。
4．3

なぜ現場で使わないのか？

しかし、既にかなり使い込まれていて、無料で使程を見せることができる模型作成を行っていた。

用でき、理論的にもしっかりしている模型検査ツー●問題領域にあるオブジェクトを認識する●それをベースに、プロセスを見つけ、その間のチャネルとメッセージを考える●重要なプロセス群を見つけ、そこをまず模型化する

ルが、なぜか日本ではほとんど使われていない。
今回のようなワークショップを、仮にUMLを対象として行った場合、ほとんどの参加者は模型構築に至らないだろう。反対に、今回は参加者のほとん
どが模型構築に成功した。そこが、UMLのような野中さんのチームは、模型検査を一番精密に行っ意味の曖味な図形言語を核とした手法と、形式手法ていたように思うが、野中さんの失敗例が一番おの違いであろう。とっつきにくいが、結局は早いのもしろかった。すなわち、野中さんの最初の模型は「正しい鍵とは異なる鍵を使って、いつかは鍵が開だ。しかも、あとで見直すことが容易である。

いてしまう」例が提示されたそうだ。これは、鍵が査や形式手法を日本で普及させなければならない、掛かっているときにも、鍵の変更ができてしまう模という確信を持った。

型を書いたための失敗だが、もっと複雑なシステム
では、このような単純な失敗を人手で見つけること

今回のワークショップをきっかけとして、模型検5

ワークショップ後の改良モデル
ワークショップの後、改良した山崎さんの模型をは難しいので、SPINの威力を感じた例であった。
我々のチームは、行き当たりばったりで「3人中誰かは模型作成できるであろう」という方針を取っ以下に示す。筆者のモデルは、まだ改良していない
ので、次回SEAMAILで報告することとしたい。

た。大規模システムの開発には向かないが、4時間

Listing3

山崎利治さんの最終模型

で模型検査まで行くには、この方式も良いだろうと／＊思ったのである。

多くの試行錯誤を行ったが、結果として他チーム

＊

釘d二g−

e−Jocたer

OC玩r・pmg，VJ・川2005／Pg／75g＊／

より多くの版のPromelaソースを書き、SPINの初歩の経験を積むには艮かった。囲碁や将棋の世界で＃derine N2

は「下手なうちに考えるな。多くのゲームをし、試＃definelockingls

行錯誤を行って、その世界の感覚をつかめ」という＝true＃define unlockingls

＝

false

＃definelocked（ls＝true）

上達のための極意があるが、それをそのまま使って＃define unlocked（ls＝false）

みたわけである。

獅Iefine opening ds

4．2＃define closing ds＝

模型検査は必須

＝true
false

＃define opened（ds＝true）「このような模型検査系を使わずに、どうして並＃define closed（ds＝false）

行処理プログラムを設計し得るのでしょうか？」と＃define eq（Ks＝K）

いう奈良先端科学技術大学院大学蔵川先生の言葉＃define kfull（i＝N）．lti・

WorkshopReport

Vol．14，No．8＝

Bch？L（t）−＞

progress2＝

mtype＝†D，L，C，OPEN，CLOSE，lock，unlock）；

if：：kfull −＞ChanBch＝［1】of（mtype，bit）；

Lch！lock；Ks＝K；gOtO

Chan Dch＝［0】of（mtypel；：：elseChan Lch＝［0】of t mtype）；−＞

goto bs3ri：：Bch？C（t）−＞

boolls＝true，ds＝goto bs3

fi；

ralse；

ShortIく，Ks；

bs4：ifbytei；：：kfull−＞

bit，d，t；：：elSe−＞if

goto bs3：：Bch？D（d）−＞in（d）；gOtO bs4：：Bch？C（t）−＞

new（）；gOtO bs4：：Bch？L（t）−＞

goto bs4

fi

inlinelleW（）（d−StePt K＝0；i＝0

fi

日
）

inlinein（d）（d−Stept K＝2＊K十d；i十十日

proctype Lock（）（lsl：ir：Lch？unlock

proctype Button（）−＞unlocking；gOtOIs2

（

end：
bsl‥

：：Lch？lock−＞

gotoIsl−＞gotoIs2−＞

opening；gOtO ds2

ri；neW（）；

if

ls2：if：‥

Bch？D（d）−＞in（d）；gOtO bs2：‥

Bch？C（t）−＞

goto bsl：＝

Bch？L（t）−＞

goto bsl：：Lch？lock−＞locking；gOtOIsl：：Lch？unlock

fi

fi；

bs2：if）：：kf1111−＞

ir

proctype Door（）：：eq −＞（
dsl：irprogressl：Lch！unlock；：：Dch？OPEN −＞goto bs3：：else−＞if

goto bsl

fi：：unlocked：：else −＞：：elseif−＞

goto dsl

fi＝：Bch？D（d）−＞ill（d）；gOtO bs2：：Dch？CLOSE−＞：：Bch？C（t）−＞

ri；

：＝

goto bsl

Bch？L（t）−＞

goto bs2

goto dsl

ds2：if：：Dch？CLOSE

ri
−＞

fi；

closing；gOtO dsl：：Dchbs3：ir：：Bch？D（d）−＞
new（）；in（d）；gOtO bs4

fi
）

70PEN

−＞

goto ds2

bslⅥ）1．14，No．8

ⅥbrkshopReportproctype user（）

参考文献

i Bch！D（1）；Bch！C（t）；

Bch！D（1）；［1］伊藤昌夫（翻訳）Gerth・Promela簡介，Fbb・Bcll！D（1）；2005．

unlocked；Dch！OPEN；［2］GerardJ・HoIzmann・

Bch！D（1）；

αmd

TTle

郎m Model〟αm↓αJ．

仇ecたer二

Bch！D（0）；Addison−Wesley，Sep．2003．

Bch！D（0）；戸わmer

月（重代mCeBch！C（t）；［3】GerardJ・HoIzmann著，水野忠則・東野輝夫・

Bch！L（t）；

佐藤文明・太田剛訳．コンピュータプロトコル

Dch！Cu）SE；の設計法．カットシステム，Nov．1997．

Bch！D（0）；Bch！D（0）；［4］IFAD・Developmentguidelinesforreal−timeu11locked；Dch！OPEN

SyStemSuslng VdmtooIs．Tbchnicalreport，）CSK，2000．
［5］IFAD・771eZFAD VDM＋＋Langua9e・CSK，proctype watch（）

V6．8edition，2001．

（do：：timeout−＞

printf（deadlocku？

）［6］CliffJones．Syslematic SqPwa柁Develop−

od

mentusmgVDMPrenticeHallInternational，

）

1990．

［7］ジョン・フイツツジェラルド，ピーター・ゴー

proctypellSerO（）

ム・ラーセン．VDM十十関数型回帰テスト支援

t do：：Bch！D（0）ライブラリ．岩波書店，2003．

：：Bch！D（1）：＝【81山崎利治．Dw2005のための問題，Rb・2005・

Bch！C（t）：：Bch！L（t）：：Dch！OPEN：：Dch！CLOSE
od）trace（do：：Lch？unlock；Lch？lock

od
）

init
（Ks＝3；
atomic（run Button（）；rum Lock（）；run Door（）；run uSer（）；run watch（）））．18・

WorkshopReportⅥ）1．14，No．8

eOO

ゝMessageSequtn⊂eChan

転玩蒜詞 ＝2l＿鱒

9；サー ￣l
1

B

l

2

ヨ

I

ヨ

ユ

l

5

l 7l

■

5

l

7

＄

l

1

2

9

ヨ

一

2！otI一五血書

■￠

貼れ 】

暮 l毒

糾 ：書1∋！¶ 5

6

7

1●

19

l番

＄ f〆 9 1 3l l H l

ll

Ⅰ

11

油＄l

l

塑曳禦竺竺」A」鵬紺Ve屋〆項｝

WorkshopReportⅥ）1．14，No．8

課題「電子錠物置」
山崎利治

以下は私のDW2005の演習課題の解答です．肝心のPromela／SPINの理解不足に，それに輪をかけた垂線によって拙く虫までいるといった代物ですが，おもちゃの小問題でも並行プロセスになれていないと手を焼くことになる見本としてど笑覧ください．じつに汗顔のいたりです．

課題の検討
課題のPromela模型を構成するために（逐次的には進まないが）つぎのような作業を行った・

1． 事象・作用を洗い出し
2．

利用事例の検討

3． 状態変数と状態述語術語の検討
4．LamportによるTLA風の仕様記述
5．

Statechartを書く

6． 検査項目の洗い出し
7．

Promelaコード作成

事象・作用を洗い出し
これは物置の利用者の操作と，それらに対する物置側の応答がすべてで「ご利用に際して」から汲み取れる．模型を簡略化するためにつぎのように考えた．

1． 押し釦はすべてそのまま採用する．

2． 取っ手は廻すを捨象，「開ける」と「閉める」に簡略化．

3． 施錠灯は施錠中は点灯，開錠中は消灯として無視，ただし，利用者の挙動としては「消灯を確認して」（鍵を変更する）があるので記憶しておく．

4． 上の利用者の操作に対して対応する物置の作用を用意する．
5． あとで気が付いて加えた物置の作用がある．

利用事例の検討
つぎのような利用事例が想定できる．

．20．

WorkshopReport

ⅥIl．14，No．8

1．開錠：：施錠・開扉状態で数字釦をN回押して施錠鍵を構成し開錠する．

2． 開扉：：開錠状態で「開ける」と扉が開く．

3．鍵の変更：：開錠状態（施錠灯は消灯）において「消灯を確認して」数字釦をN回押して新しい鍵を構成する．ここでL釦を押すとこの鍵によって施錠される．
4． 開扉：：「閉める」と扉が閉まる．

状態変数と状態述語術語の検討
模型を構成するために物置の状態変数と必要な状態述語を考える．つぎが想定できる（詳細は「TLA風の仕様記述」参照）．

定数
鍵の桁数N，10進数字集合Digits，数字釦を押した回数の変域Ⅰ，交信信号集合M・

状態変数（1）鍵の状態ls，扉の状態ds，施錠鍵Ks（初期値kk），押した数字による構成鍵K（初期値0），数
字釦を押した回数i（初期値0）．

（2）利用者と物置間の交信の媒体となる待行列qB（釦関係），qD（取っ手関係「開ける」，「閉める」）．

（3）できるだけプロセスを自明なものにするためにいくつかのプロセスをつくることにする・鍵プロセス，扉プロセス，釦プロセスがそれである．補助的に待行列qLを用意する．

図1プロセスと通信路．21．

WorkshopReport

Ⅵ止14，No．8

状態述語
施錠中locked，開扉中opened，施錠灯消灯中indoだ，構成鍵の初期状態newk，N桁構成鍵を構成したkhll，施錠鍵と構成鍵が合致したkeq．

TLA風の仕様記述
つぎが上のように考えて書いた課題の仕様である（本来記述すべき安全性や活性はここには書いていない・つまり，模型部分だけである）．プロセスUserとLockerが交信を繰り返し，その目的を果たすわけである．Userがその行為として，SendB（d），SendL，SendC，SendO，SendClを行う．また，RcvXxはそれに答えるLockerの行為で，さらにいくつかの副次的なLockerの行為がある（SendU，SendLk，RcvU，RcvL，Akfu11）．

8−locker

COⅣSTAⅣTS

byteⅣ；
Digit8＝＝（0‥91；
Ⅰ＝＝（0‥ⅣI；

M＝＝（D，C，L，OPEN，CLOSE，lock，unlockl；
Bbort kk；

VARIABLES
b00118，dS；
Bbort K8，K；

i：Ⅰ；

d：Digits；
qB：queue（M＊Digits）；
qD：queue（H）；
qL‥

queue（M）；

STATE PREDICATES
locked＝＝（15＝＝true）；
Opened＝＝（d8＝＝true）；
indoff＝＝（18＝＝fa18e）；
nevk＝＝（i＝＝0＆＆K＝＝0）；kfull＝＝（i＝＝Ⅳ）：

keq＝＝（Ks＝＝Ⅹ）；．22．

WorkshopReport

ⅠⅣIT

Ⅵ）1．14，No．8

＝＝
Ks

＆＆

＝岩

kk

locked地！opened
血色

newk

紬

qB＝＝neVq

馳

qD＝＝neWq

地qL＝＝neWq

ACTIOⅣS

SendB（d）＝＝

eXi8tS d：DigitS．qB，＝言enq（申，（D，d））；

SendL

＝＝

qB，＝＝emq（qB，（し，0））；

SendC

＝＝

qB，＝＝enq（qB，（C，0））；

SendO

三三

qD，＝＝enq（qD，OPEN）；

SendCl三三qp，＝＝enq（qD，CLOSE）；

SendU

＝＝

qL，＝＝enq（中りunlock）；

SendLk＝…

中ノ＝＝enq（qL，lock）；

RcvD（Ⅹ：M＊Digits）＝＝Cl H c2ll c3ll c4

Vhere

pp＝＝！emp（qB）的qB，＝三deq（qB）＆＆exiSt d：Digits．（Ⅹ…＝front（qB）＆＆Ⅹ＝＝（D，d）

Cl＝＝pp地locked＆＆newk地X，＝三10＊K＋d地i，＝三i＋lC2＝＝pp＆＆locked地！newk地KJ＝＝10＊K＋d＆＆iI＝＝i＋1＆＆（iリ＝Ⅳll Akfull）

C3＝＝pp＆＆！locked地kfull＆＆X，＝＝d地i，＝＝l
C4＝＝pp地！locked＆＆！kfull的KI＝＝10＊Ⅹ＋d地iI＝＝i＋1；

Akfull＝＝locked

＆＆

kfull

＆＆

ⅥわrkshopReportⅥ）1．14，No．8

如く（keq地SendU）ll（！keq地X，＝＝0烏愈i，三三0））；

RcvC＝＝（！emp（申）抽front（qB）＝＝（C，0）ト＞（X，＝＝0地1，＝＝0

RcvL

馳qB，＝＝deq（qB））；＝；；＝（！emp（申）地front（qB）；＝＝＝（し，0）地！locked）−＞（SendLk＆＆Ⅹ＝＝0地i，＝＝0地中，ココdeq（申））；RcvLk＝＝！emp（qL）＆＆front（qL）＝＝lock＆＆（locked H18，三＝！18）＆＆qL，＝＝deq（qL）；

RcvU＝＝lockcd＆＆（！emp（qL）＆＆front（qL）＝＝unlock−＞（lockQdl115，＝＝！18）地qL，＝＝deq（￠）；RcvO＝＝（！emp（qD）馳front（qD）＝＝OPEⅣ地（openedll dS，＝＝us）

地qD，＝＝deq（qD）；

RcvCl＝＝（！emp（qD）＆＆front（qD）＝＝CLOSE＆＆（！openedll dS，＝＝！ds）＆＆qD，＝＝deq（qD）；

Ⅳext＝＝SendB（d）ll SendLll SendCll SendO

H SendCl H SendU H ScndLk H Send
H RcvB（Ⅹ）ll RcvLll RcvCll RcvU

ll RcvLk H RcvOll RcvCl H Akfull

SPEC＝＝ⅠⅣIT＆＆［］Ⅳext＆＆WF（Ⅳext）＊甲eueは先入先出待行列でふつうの演算n帥q，enq，deq，front，（iS）e叩（ty）をもつ．

＊ACTIOⅣSで，を付けた変数はACTIOⅣの実行後の値を表す．また，を付けた変数以外の変数
値はACTIOⅣによって変わらない．

Statechartを書く

以下は課題のstatechartである．Promelaコードを書くために便利と思ったからである．そこ
でプロセスとして，Button，Lock，Doorを書いた．Userは自明であるから書かなかった．

．24．

WorkshopReportⅥ）1．14，No．＄

Bch？L（t）ltrue／skip］

濫読ed三f…冒㌻e）E…30錆課。｝
newk△（】＝0）

図2

in（d）△（K＝10＊K＋d；汁＋）釦の状態遷移図

Lch？lock［tnユe／skip］

Lch？unlock［true／skip］

locked△（ls＝true）

unlocking△tls＝餌se）locking

図3△恥＝true）

鍵の状態遷移図

Dch？CLOSE［true／skip］

Dch？OPEN［hVe／skip］

opened△（ds＝＝tme）
OPeTing△ids＝trUe）
closIng△（ds＝hlsei

図4

扉の状態遷移図．25．

WorkshopReportⅥ）1．14，No．8

検査項目の洗い出し
安全性の主張は［］Ⅳextとしたものと，それらによって状態変数の型が不変であることが考えられるが，この検査は省略する．
活性についての主張にはさまざま確かめたい．たとえば，利用事例で記した項目を検査したい．
1． 鍵を知っていれば開錠でき扉も開けられる．

2． 鍵を知らなければ開錠できず，したがって扉を開けられない．

3． 開錠状態において「消灯を確認して」数字釦をN回押して新しい鍵を構成できる．ここでL釦を押すとこの鍵によって施錠される．
そこで，
1．openedに！lockodが先行する．

2．！lockedにkeqが先行する．

などと考え，
1．0penedに！lockedが先行する．
く＞opened−＞（locked U（！locked＆＆！opened））

2．！lockedにkeqが先行する．
く＞opQnd−＞（！keqU（keq＆＆！opened））

を検査してみる．

Promelaコード

つぎが先のstatechartを忠実にコード化したものである．ただし，模型を小さくするために10進数字を2進数字にし，桁数も2とした．コード中に検査向きに実際には模擬実行させないプロセ
スもある．initプロセスを書き換えて実行させてみようと思ったからである．プロセス，通信路，

大域変数，状態述語などは図示の通りである．
／＊

e−locker＊／＃defineⅣ＃dQfine kk

2

3＃definelocking18＝truQ＃define unlocking18＝false＃definelocked（18＝＝true）＃define unlocked（18＝＝fa18e）．26．

Ⅵ止14，No．8

WorkshopReport＃define opening dS＝tru虐＃dofine cloBing dS＝fa188＃define opened（dS＝＝tme）♯dQfine cloSed（dS＝＝fa18e）＃define keq（XB三＝K）＃define kfull（i＝三Ⅳ）mtype＝t D，し，C，OPE∬，CLOSE，lock，unlockI；

cban Bcb＝【1］of t mtype，bit）；
Chan Dcb＝［0］of t mtypQI；

Cbm Lch＝［0］of（mtypeI；

boo118＝true，dB＝fa188；
Sbort X，XS；

bytQi；
bit d，t；inline kinit（）（Ⅹ8＝kkI

inline nev（）

t d●Btept X＝0；i＝0〉I

inlin8in（d）
t d＿8tept K＝2＊K＋d；i＋＋ナナ

proctype ButtonOfend：

b81：neW（）；

if：：Bch？D（d）−＞in（d）；gOtO b82‥‥Bcb？C（t）−＞goto bSl：：Bcb？しくt）−＞goto bBl．27．

WorkshopReportⅥ）1．14，No．8

fi；
b82：if：：kfu11−＞if：：keq−＞progre881‥Lch！unlock；gOtO b83：：818〇一＞goto bSlfi：：e18e −＞if：‥Bcb？D（d）一＞in（d）；gOtO b82：：Bch？C（t）−＞goto b81：：Bcb？しくt）−＞goto b82

fifi；
b83：if：：Bcb？D（d）−＞new（）；in（d）；gOtO b84：：Bcb？L（t）−＞
progre882：

if：：kfull−＞Lch！lock；KS＝K；gOtO b81：：e188−＞goto b83

fi：：Bcb？C（t）−＞goto bs3

fi；
b84：if：：kfu11−＞goto b83：：e188−＞if：：Bcb？D（d）−＞in（d）；gOtO b84：：Bch？C（t）−＞nev（）；gOtO bS4‥：Bcb？L（t）−＞goto b84

fi

fi
）

proctype Lock（）（

181：if−28．

Vol．14，No．8

ⅥbrkshopReport：：Lch？un1ock−＞unlocking；gOtO182：：Lcb？lock−＞gotoIsl

fi；
182：if：：Lch？lock：‥−＞locking；gOtOlSl

Lch？皿lock−＞goto182

fi）

proctype DoorOtdSl：if：：Dcb？OPEy −＞if：：unlocked−＞opening；gOtO d82：：e18e−＞goto dSlfi：：Dch？CLOSE−＞goto dsl

fi；
d82：if：：Dcb？CLOSE−＞cloSing；gOtO dSl：：Dcb？OPEⅣ−＞goto ds2

fi）

proctype UBer（）t Bch！D（1）；

Bcb！C（t）；
Bcb！D（1）；
Bcb！D（1）；unlocked；Dch！OPEⅣ；
Bch！D（1）；
Bcb！C（t）；

Bcb！D（0）；Bch！D（0）；Bch！しくt）；

Dch！CLOSE；

WorkshopReport

Vol．14，No．8

Bcb！D（0）；Bcb！D（0）；unlocked；Dcb！

OPEy

I

proctype vatcb（）

t do：：timeotlt−＞printf（

deadlock？

）

Od〉

proctypo U88rO（）t do：：Bch！D（0）：：Bcb！D（1）：：Bch！C（t）：：Bcb！しくt）：：Dcb！OPE∬：：Dcb！CLOSE
Od）

trace（do：：Lcb？unlock；Lcb？lock

od
I

init

t kinitO；
atomict
nm ButtOnO；nm Lock（）；nm DoorO；nm U8er（）；nm TatCb（）ナ
ナ−30．

WorkshopReport

Vol．14，No．8

検査の実際
Promela模型ができたら，まずは模擬実行である．小さな課題だからと侮っていたら散々であった．実際は佐原さんに熱海で動かしていただいたのであるが．もっと以前に野中さんにSPINを動かせるようにしていただいていたのに怠慢至極であった．熱海から帰って考え直して書いたものが上である．
正しい利用形態では動くようなので，望みの性質をもつかを確かめることにする．
1． 出鱈目な釦操作で凍みを起こさないか？
2．openedに！lockedが先行する．

3．！lockedにkeqが先行する．

1．の検査のためにUserOOを書いた．

2．の検査はLTL式から否定要求を生成して行う．通信路Lchの交信の順序を確かめるために跡表明もつけてみた．これらの検査については不勉強でSPINが出す説明が読めていない．みなさまの助けを請わなければならない．
つぎは検査実施の一例である．
＃define o（dS＝＝true）＃define k（KB三三K）／＊＊Fomla AS Typed：く＞0−＞（！k U（k地！0））

＊TbeⅣeVer Claim Belov Corresponds＊To The Negated Fomula！（く＞0−＞（！k U（k

＆＆

！0）））

＊（formalizing violationB Of tbe original）＊／

never t／＊！（く＞

0

−＞

（！k U

（k

＆＆

TO＿init：if‥‥（（0））一＞goto accept●S8：：（（k）＆＆（0））−＞goto accept●all：‥（（0））−＞goto accept＿S21‥‥（！（（k）））−＞goto TO●init：：くくk）地（0））一＞goto accept●S27fi；

accepLS8：if・31−！0）））＊／

WorkshopReportⅥ）1．14，No．8：：（（（！（（k）））ll（（0））））−＞goto accept＿S8＝‥（（k）抽（0））−＞goto accept＿allfi；accepLS21：
if‥：（（0））−＞goto accept●S8：：（（k）＆＆（0））−＞goto accepLall‥：（（（！（（k）））ll（（0））））−＞goto TO＿init：‥（（k）地（0））−＞goto TO＿S27

fi；accept＿S27：

if：：（（0））−＞goto accept＿all：：（1）−＞goto TO●S27fi；
TO＿S27：
if‥：（（0））−＞goto accept●all：‥（1）−＞goto TO＿S27

fi；accept＿all：

8kip
I＃ifdef

ⅣOTES

USe Load to open a file or a template・＃endif＃ifdef RESULT
VaLrning：for p・0・reduction to be valid the never claim muSt be

Stutter−invariant（never claim8generated from LTL fomulae are stutter−invariant）（Spin Version4．2．2−−12December2004）＋

Partial Order Reduction

Fu118tatespace search for：trace assertion
never claim

＋
＋

．32−

WorkshopReportⅥ）1．14，No．8

asSertion violations＋（if vithin scope of claim）
acceptance cycles＋（fairnesS diBabled）

invalid end states−（disabled by never ciaim）

State−VeCtOr40byte，depth reached O，errOrS：0l stateS，StOred

O state8，matChedl tran8itions（＝8tOred＋matched）

O atomic stepS
baSb conflicts：0（re801ved）

StatB On memOry u8age（in MegabyteS）：

0・000

eqJlivalent memory u＄age for StateS（stored＊（State−VeCtOr＋overhead））

0・289

actllal memory uSage for8tateS（unSuCCeSSful compres8ion：601500・00笑）

State−VeCtOr aS StOred＝288712byte＋8byte overhead
2・097

memoryllSed for hasb table（−W19）0・320

memory uSed for DFS stack（一mlOOOO）

0・152

0ther（proc and cban StaCkB）

0・084

memoryloSt tO fragmentation

2・622

total actual memory u8age

u汀eaCbedin proctype Button
1ine32，日pan．●…

，

8tate4，■■D＿STEP■■

HD＿STEP‖

1ine35，■■pan．…ノ■，8tate

1ine42，−■pan．…ノ●，State15，

1ine42，■■pan．＿＿ノ●，

State15，

1ine42，日pan・＿＿＿日，

5tate15，

1ine50，日pan．＿‖■■，

8tate19，

lILcb！unlockll

1ine49，■■pan．…＿日，

8tate

23，

‖（（Ⅹ8＝＝Ⅹ））■■

1ine49，日pan．＿＿＿，

Btate

23，

1ine35，State30，
line

54，State36，

1ine

54，State36，

1ine

54，State36，

9，日D＿STEP日

日Bcb？D，d日
日Bcb？C，t日
日Bcb？し，tt●

1ine47，State38，‖（（i＝＝2））‖

1ine47，Statellelse日38，

1ine32，State44，

日D＿STEP‖−■Bcb？D，d‖−，Bcb？C，t−■‖Bch？し，t‖llelBell﹁
Ⅵ九14，No．8

WorkshopReport

1ine35，8tate48，
1ine65，Btate52，
1ine65，State53，
1ine64，8tate57，
11m864，8tate57，
1ine60，State61，
1ine60，8tate61，
1inQ60，8tate61，
1ine35，8tate70，
1ine32，8tate76，
11m072，8tate80，
1ine72，8tate80，
1ine72，8tate80，
1ine70，8tate82，
1ine70，8tate82，
1ine78，Btate84，

HD＿STEP‖llLcb！lockH
llXS

＝

Ⅹ11

−■くくi＝＝2））‖

lle18ell
HBcb？D，d日
日Bcb？し，tH■■Bcb？C，t■■‖D＿SⅥ；P●t
HD＿S●n…P日

日Bcb？D，d■■−，Bch？C，t日
日Bch？し，tH
Hくくi＝＝2））●−11018e日

日−QndJl

く260f848tateB）

以下省略

振り返って
伊藤，野中両大徳の誘いに乗って楽しい熱海を過ごせたわけですが，みなさまに大変ご迷惑をお掛けしてしまった．おかげで並行プロセスはいい加減には書けないことが身にぬみて解った・Vol．14，No．8

ⅥbrkshopReport

デザインワークショップ2005参加報告
三好健吾
九州大学大学院

システム情報科学府

情報工学専攻修士課程2年
TEL：092−642−3865
kengo＠ale．csce．kyushu−u．aC・jp

平成17年4月19日

1

ワークショップの要約
本資料は、2005年2月24日（木）〜26日（土）にウェルハートピア熱海において、ソフトウェア

技術者協会（SEA）が主催したデザインワークショップ2005の参加報告である。

1．1

ワークショップの日的

本ワークショップの目的は、モデル記述言語Promela（ProcessMetaLanguage）とその検証ツールであるSPINを実際に使用し、その有効性を検討することである。

1．2

ワークショップの課題

本ワークショップでは、課題として四桁の開錠鍵を持つ物置を題材とし、その物置のモデルを作成し性質を検証することを課題とした。

2

モデルの解説本ワークショップにおいて私が作成したモデルの解説を行う。なお、付録Aに作成したモデルを

掲載する。

2．1

モデル構築の方針課題となるモデルの作成にあたり、まず最初に山崎利治さんが考案されたステートチャート図を基に、物置を構成要素とその機能で区別した。今回は、物置がボタン入力部、施錠部、ドア部から成ると考え、この3つに区別した。その構成要素それぞれをButtonプロセス、Lockプロセス、D。。rプロセスとしてモデルを構成した。以上の3つのプロセスが完成した後に、物置のユーザの動作をプロセスとして定義した。最後に、モデルの初期状態をinitプロセスで定義した。

．35．

WorkshopReportⅥ）1．14，No．8

また、通信路として、ボタン入力に関するメッセージのための通信路Bcb、ドアの開閉に関するメッセージのための通信路Dch、施錠・開錠命令に関するメッセージのための通信路Lcbを定義
した。

2．2

各プロセスの説明

2．2．1

Buttonプロセス

Bnttonプロセスは、ボタンの入力部の動作を意味するプロセスである。このプロセスは、以下の四つの状態を取ると仮定する。
●

Sl

施錠され、ユーザが開錠鍵の入力を行う状態●

S2

施錠され、ユーザから開錠鍵の入力が完了した時に鍵の照合、開錠命令の送信を行う状態●

S3

開錠され、施錠命令を送信する状億●S4開錠され、ユーザからの入力を受けて開錠鍵の変更を行う状態
このプロセスでは、プロセス起動時に施錠された状態（lock＿1a叩＝ご1）であるなら、状態Slに遷移する。Slにおいては、入力した開錠鍵が四桁未満ならば鍵の入力の後再度入力の桁を調べ、四桁の入力が完了していれば状態S2に遷移する。
状態S2に遷移した場合、まず入力された開錠鍵の照合が行われる。入力が保存されている開錠鍵と一致した場合開錠命令を送信する。
開錠された状態（lock＿1anp三三三三0）であるなら、状態S3に遷移し、Lockボタンが押された場合に施錠命令を送信する。LocXボタンではなく数字のボタンが押された場合、状態S4に遷移し、開錠

鍵の変更を行う。
状態sl、S2においては、通信路LcbにメッセージLOCXが、状態S3、S4においては通信路LcbにメッセージUNLOCKが受信されず残っている状態である。これらのメッセージが受信されるのは、開錠命令および施錠命令送信の直前である。これにより、他のプロセスの動作に左右されることな
く開錠鍵の入力ができるようにしている。
Buttonプロセスにおける開錠鍵入力操作および入力消去操作は、inpllt止ey、Clearというinline

マクロとして定義されており、プロセス内で呼び出されている。このうちinlineマクロinput止Qy

については、数字ボタン以外の入力を受け付けず、Lockボタン、C18arボタンが押された場合にはinlinoマクロclearが実行され、入力を消去するようにしている。

2．2．2

Lockプロセス

Lockプロセスは、鍵の電子的な開錠および電子的な施錠を行うプロセスである。このプロセス
は、施錠時であるLSlと開錠時であるLS2という二つの状態を取る。

．36．

WorkShopReport

Ⅵ止14，No．8

開錠は、状態LSlにおいて通信路LchからメッセージⅧLOCKを受信することで行われ、施錠は、状態LS2においてLockボタンが押され、物置の表示窓に何も表示されていない場合に行われる。

2．2．3

Doorプロセス

D。。rプロセスは、ドアの開閉を行うプロセスである。このプロセスは、ドアが閉じた状態DSlと開いた状態DS2という二つの状態を取る。ドアの開閉はユーザによって行われ、開錠時にユーザを意味するプロセスからのメッセージを受信することで行われる。

2．2．4

tJSerプロセス

物置のユーザの動作をU80rプロセスとして定義する。今回定義したプロセスは以下の通りである。

初期状態の開錠鍵を使って物置の開閉を行うプロセスである。初期状態の鍵

1234

を入力後

ドアを開閉し、施錠を行うという動作を繰り返す。

開錠鍵の変更を行うプロセスである。まず初期状態の鍵
錠鍵を

5555

1234

を入力して開錠し、その後開に変更する。その後ドアの開閉を行い、施錠する。その後は変更後の鍵を用いて開錠と施錠を繰り返す。

鍵の変更を繰り替えすプロセスである。初期状態の鍵1234と変更後の鍵

5555

とを交互に

使用し、開閉を行う。

uS。rO3プロセスの動作に、鍵の入力間違いによるクリアと、鍵の入力途中に誤ってLockボ

タンを押すという動作を追加している。

3

SPINによる検証
SPINを用いて、このモデルの検証を行った。Simulationにおいては思惑通りの動作が行われていることを確認できた。しかし、Veriacationにおいては、検証オプションを変更した場合にデッドロックが発生した。これは、本来想定していない順序でメッセージの送受信が行われたことが原因である。

4

考察
今回のモデル構築の際には、山崎さんが考えられたステートチャートを参考にさせて頂いた。

そのため、構成要素の切り分けおよび状態の把握をスムーズに行うことができた。また今回は、atomic、d＿8tQp等の命令を極力使わず、メッセージの送受信のみで危険区域と非危険区域との区別

WorkshopReport

Ⅵ止14，No．8

をつけようと試みた。そう試みた理由は、atOmlc等の命令を用いた場合、モデルにおけるデッド
ロックの危険性を簡単に排除できる反面、SPINを用いることで検証可能な並行性の問題を発見できないと考えたからである。今回の課題では、3にも述べた通り、各プロセスを並行に走らせた時に予想外のメッセージの送受信が発生した。このことから、各プロセスにおいて他のプロセスの影

響を受けてはならない危険区域の切り分けが不十分だったと考えられる。

5

感想
今回の課題は、残念ながら期限内にnQVOr Claimによる検証を行うことができなかった。この点は非常に反省すべき点である。また、4でも述べた通り、危険区域と非危険区域の切り分けが不十分であった。今後モデル構築の際には危険区域についても十分な検討を行いたい。
今回DW2005に参加させて頂いて、PROMELAの基礎やモデル構築のノウハウを学ぶことができ、非常に有意義な時間を過ごすことができた。

A DW2005課題

物置のPROMELAモデル／＊ 定数定義＊／＃dQfineⅣ／＊施錠鍵は4桁＊／

40／＊ドア開いた状態＊／＃define CLS l／＊ドア閉じた状態＊／＃dofine HOR O／＊取っ手水平（開いた状態）＊／＃define OPⅣ＃define／＊取っ手垂直（閉じた状態）＊／

Ⅵ三Rl＃definQ BLAⅣK−1／＊表示窓空白 ＊／／＊大域変数定義＊／／＊データ型＊／

intindex；／＊値を表示する表示窓の番号＊／

int buff［Ⅳ］；／＊ユーザが指定した鍵を格納する領域＊／

int vin［Ⅳ］；／＊表示窓＊／

bitlock＿1amp；／＊施錠灯＊／

bit door；／＊ ドア ＊／

bit handle；／＊ 取っ手＊／mtype（D，C，L，LOCK，UNLOCK，OPEN，CLOSEI；／＊ メッセージタイプ

D：数字の入力

L：Lockボタン押下・38・

WorkshopReport

Vol．14，No．8

C：Clearボタン押下

LOCX：Lockプロセスへの施錠命令

ⅧLOCX：Lockプロセスへの開錠命令

OPEⅣ：Doorプロセスへの開扉命令

CLOSE：Doorプロセスへの閉扉命令＊／／＊通信路＊／
chむlBch…［1］0f fmtypo，Sbortl；／＊ボタン押下時の通信路＊／

Chan Dcb＝［1］0重くmtypoI；／＊ドア開閉時の通信路＊／

Chan Lcb＝［1］of t mtyp01；／＊ 開錠・施錠時の通信路＊／／＊inl土neマクロ＊／

inlineinplユー＿koy（）f／＊鍵入力＊／

if：：（！（Bch？lL（1）】）＆愈！（Bch？lC（1）】）＆＆nempty（Bch））−＞Bch？D（vin［index］）；
index＋＋：：Bcb？［しく1）】−＞Bcb？L（1）；Clear（）：：Bch？lC（1）】−＞Bch？C（1）；Clear（）fiIinline clear（）t／＊入力クリア＊／index＝0；do：：index！＝Ⅳ−＞vin［indQX］＝BLA∬K；
index＋＋：：indexココⅣ−＞index＝0；breakOd〉／＊ プロセス型定義＊／／＊ボタンの入力に関するプロセスButtonプロセス
PrOCtyPe BllttOn（）（

end：do：：if：：（Lch？lLOCK］＆＆（lock＿1amp＝＝1））−＞／＊鍵入力 ＊／
Sl：if：：index

三三Ⅳ−＞indQX＝

0：：01se−＞input」柑y（）；goto Sl−39−＊／

WorkshopReport

Vol．14，No．8

fi；／＊鍵の照合・開錠命令の送信＊／
S2：

if：：index！＝

Ⅳ

一＞if：：Win［indeⅩ】＝三三＝buff［indQX】；−＞index＋＋；
goto S2；：：els8−＞C18arO；gOtO Sl；

fi；：：index……Ⅳ−＞

Lcb？LOCK；

ClearO；
Lch！UNLOCK；

fi；：‥（Lcb？［ⅧLOCK］地（lock●1amp＝＝0））−＞／＊施錠命令の送信＊／
S3：

if：：Bch？［L（1）］−＞Lch？lLOCK］−＞Bch？L（1）：：emPty（Bch）−＞Skip：：（！（Bch？lL（1）］）＆＆！（Bch？［C（1）］）＆＆nempty（Bch））−＞／＊鍵の変更＊／S4：

if：：index＝＝

Ⅳ−＞index＝0：：index！＝Ⅳ−＞input＿key（）；goto S4fi；
Bcb？［しく1）］−＞Bcb？L（1）；ⅣEW KEY：

if：：index！＝Ⅳ−＞buff［index】＝Vin［index］；
indox＋＋；

gotoⅣEW＿KEY：：index＝＝Ⅳ−＞

clear（）

f土

fl
fi；

Od
〉

／＊鍵の開錠・施錠に関するプロセス

Lockプロセス

PrOCtyPe Lock（）（／＊電子的な開錠＊／
end：do：：Lcb？［ⅥqLOCX］−＞

・40−

＊／

WorkshopReport

LSl：

Ⅵ止14，No．8

lock●1a皿p＝0；／＊電子的な施錠＊／（Bch？［L（1）］＆＆（vin［0］＝＝（−1））＆＆（win［1］＝＝（一1））＆＆（vin［2】…＝（−1））＆＆（vin［3］＝＝（−1）））−＞LS2：

Lch？UⅣLOCK；
10Ck●1a皿p＝1；

Lcb！LOCX

Od
I／＊

ドアの開閉に関するプロセス

Doorプロセス

proctypo Door（）

t do
：：if

：：（（lock＿lamP＝＝0）抽Dch？lOPEN］）−＞／＊ドアを開く ＊／
DSl：

door＝

OPN；Dch？OPEN：：（（10Ck＿1amp；；二三0）＆＆Dch？lcLOSE］）−＞／＊ドアを閉じる ＊／DS2：

door＝CLS；Dch？CLDSE
fi；

Od
I

／＊

テストケース

Userプロセス＊／

proctype UserOl（）t
end：do：：Bcb！D（1）；
Bcb！D（2）；
Bcb！D（3）；Bch！D（4）；handle

亡HOR；

Dch！OPEN；
Bkip；

ha皿dle＝Vm；

Dch！CLOSE；
Bch！L（1）Od〉

PrOCtype UserO2（）t

Bch！D（1）；

．41．

＊／

Vol．14，No．8

Bcb！D（2）；

Bcb！D（3）；
Bcb！D（4）；
Bcb！D（5）；

Bcb！D（5）；
Bcb！D（5）；

Bcb！D（5）；
Bcb！L（1）；bandle＝HOR；

Dcb！OPEⅣ；
Bkip；

bandle＝Ⅵ≡R；

Dcb！CLOSE；

Bch！しく1）；
end：do：：Bcb！D（5）；Bcb！D（5）；Bch！D（5）；Bch！D（5）；bandle＝HOR；
Dcb！OPEN；
Bkip；

handlo＝Ⅵ：R；
Dch！CLOSE；
Bcb！L（1）Od〉proctype tJSerO3（）（ do：：Bch！D（1）；
Bcb！D（2）；
Bcb！D（3）；Bch！D（4）；
Bcb！D（5）；

Bcb！D（5）；
Bcb！D（5）；
Bcb！D（5）；
Bcb！L（1）；handle＝＝HOR；

Dcb！OPEⅣ；
Bkip；

Dch！CLOSE；

rj

WorkshopReportWorkshopReport

Vol．14，No．8

handle＝ⅤモR；
Bcb！L（1）；
Bcb！D（5）；
Bcb！D（5）；

Bcb！D（5）；
Bcb！D（5）；bandle＝HOR；
Dcb！OPEN；
Bkip；

Dcb！CLOSE；
bandlQ…Ⅵ：R；
Bch！D（1）；
Bch！D（2）；
Bch！D（3）；

Bcb！D（4）；
Bcb！L（1）；
Bcb！しく1）

Od〉

proctype UserO4（）

t do：：Bcb！D（1）；
Bcb！D（1）；
Bch！C（1）；
Bch！D（1）；
Bcb！しく1）；
Bcb！D（1）；
Bch！D（2）；

Bch！D（3）；
Bcb！D（4）；
Bcb！D（5）；
Bcb！D（5）；Bch！D（5）；Bch！D（5）；Bcb几（1）；
bandle＝HOR；
Dch！OPEN；
Skip；

bandle＝Vm；

Dch！CLOSE；
Bch！L（1）；
Bcb！D（5）；．43．

Ⅵ止14，No．8

ⅥbrkshopReport

Bch！D（5）；Bch！D（5）；
Bcb！D（5）；bandlo＝HOR；
Dcb！OPEN；
Bkip；
bandlQ＝Ⅵ：R；

Dch！CLOSE；

Bch！D（1）；
Bcb！D（2）；
Bcb！D（3）；Bch！D（4）；
Bcb！L（1）；
Bcb！L（1）

Od
〉

initt

／＊初期状態＊／
index＝0；
lock＿1amp＝1；
buff［0］＝1；
bllff［1］＝2；

bu董董［2】＝3；
bllff［3］＝4；

Vin［0】＝BLAⅣK；
vin［1］＝BLAⅣK；
Vin［2］＝BLAⅣⅩ；
win［3】＝BLAⅣK；
Lch！LOCX；

door＝CLS；
bandle＝Ⅵ：R；

nm BllttOn（）；

nm Lock（）；
nm Door（）；／＊nm USerOl（）；
nm USerO2（）；nm UserO3（）；＊／nm USerO40
1．44．

WorkshopReport

Ⅵ11．14，No．8

デザインワークショップDW2005課題の回答
野中哲（有）トゥルーロジック
2005年4月26日

1

はじめに
デザインワークショップ2005（以下DW2005）は、2005年2月24日（木）より2泊3日の日程で、ウエル

ハートピア熱海で開催された。日程の前半は、山崎さんによる、モデル検査およびPROMELAに関する講義で、後半は事前に示されていた課題［1】をPROMELAで記述して、SPINを使用して検証を行った。参加者は11名で、このうち学生が3名、教育機関から1名、その他が一般企業からの参加者であった。

2

モデル作成
課題についてPROMELAで作成したモデルのソースコードを付録Aに示す。モデルの簡単な説明は以下の通りである。
1．8afoがロッカーのプロセス。全体が1つのイベントループになっており、ke汀ad，bmdloからの入力を契機に処理を行う、イベントドリブン形式になっている。
2．グローバル変数lock＿StatuSが、鍵の状態を表す。施錠灯を兼ねている。
3．グローバル変数dooLBtatllSはドアが開いているかどうかの状態を示す。ロックされているが、ドアは閉まっているという状態がある。
4．8afeのローカル変数currentKoyが現在ロッカーに設定されている鍵。

5．8afoのローカル変数bufはユーザーのキー入力のバッファで、この値が前面に表示されているものとする。これは長さ4のキューで、キーが4つ以上入力されると古いものから消えていく。（シフトレジ

スタのような動作をする）
6．uSerとS誠8は2つのチャネルでロッカーと交信する。ke汀adが数字等のキーパッドで、bmdleが物理的にあけるハンドルである。
7．uSQr‥．がユーザーを模するプロセス

課題では言及されていないが、モデル作成に必要ないくつかの仕様を仮定した。それらを以下に列挙する。
1．ロックが解けたときは、現在のバッファをクリアする。
2．ドアが開いた状態ではキー入力は無視する。
3．新鍵設定時に4桁に数字が足りないときは、エラーにする。

4．新しい鍵を設定したときは、現在のバッファをクリアする。

・45・Ⅵ）1．14，No．8

ⅥbrkshopReport3

検証

3．1ロッカーが満たすべき仕様
まずロッカーが満たすべき仕様としては、以下のようなものが考えられた。
1．正しい鍵を入力すると開く
2．誤った鍵を入力すると開かない

3．新しい鍵を設定できる
4．新しい鍵を設定すると、新しい鍵で開く

5．新しい鍵を設定すると、古い鍵では開かない
SPINによる検証にはシミュレーションモードとべリフイケーションモードというものがある。前者では、並列プロセスをランダムにインターリーブさせながら実行を行い、後者では並列プロセスが取りうる全ての状態で問題が発生しないかどうか検証をする。

3．2 正しい鍵を入力するとドアをあけることができるか最初に正しい鍵を入力するユーザープロセスを定義し、ドアを開けられるかどうかの検証を行った。これはシミュレーションモードで検証を行ったが、ここで気が付いたのは、ドアを正しく開けるにはロッカープロセ

スとユーザープロセスの間で正しく同期をとらなければいけなという点である。
ロッカーの正しいあけ方
1．正しいキーを入力

2．ユーザーは施錠灯が消える事（解錠）を確認（ここで同期をとる）
3．レバーを回す

すなわち正しい鍵を入力しても、それを受け取ったロッカーの処理が完了し、解錠されなければ、レバーを回してもドアは開かないのである。これは、実際にシミュレーションを行った結果ドアが閲かないというケースがある事がわかり問題を発見した。ロッカーと人間の間では、現実的に実際にこのような問題が発生する事は少ないであろうが、一般的なソフトウエア設計のケースでは、このように並列プロセス間の同期は充分注意が必要なので、モデルチェッキングの有効性を感じた。

3．3 誤った鍵でドアが開く事はないか
次におこなったのは、誤った鍵を入力したにもかかわらずドアが開いてしまうことはないか、という点の検証である。これにはSPINのべリフイケーションモードを用いた。まず「ドアは永遠に開かない」という性質の記述は、TIJ式を用いて次のように記述した。
［】！p♯dofino p（lock＿BtatuBここX＿UⅣLOCKED）

次に誤った鍵しか入力できないユーザーとして、「ランダムに数字キーを押すが、4だけは絶対に押さない
ユーザープロセスを定義した。ロッカーの鍵の初期値は「1234」であるのでこのユーザープロセスは、どう頑ー46．

Ⅵbrb血opReport

Ⅵ11．14，No．8

張っても正しい鍵は入力出来ない。したがってドアは開かないはずである。
proctypQ uBer5（）tdo：：keypad！

m（0）；：：keypad！

m（1）；：：koypad！

mm（2）；：：koypad！

m（3）；：：keypad！

m（5）；：：keypad！

m（6）；：：keypad！

m（7）；：：koypad！

m（8）；：：keypad！

m（9）；：：keypad！

LOCX（0）Od）；

以上のように定義を行ったのち、SPINのべリフイケーションモードで検証を行った。実行結果は以下である。
Varning：for p・0・redllCtion to be valid the never clain mu8t be Stutter−invariant（never ciaims generated from LTL fomlae are Stutter−invariant）

Pan：Claim violated！（at depth375）
pan：VrOtQ pan＿in・trail（Spin VerBion4・2・1…80ctober2004）
Warning：Soardl nOt CO叩1eted＋

Partial Order RedllCtion

F1111BtateSpaCe8台arCb for：nQVOr Claim

a8Bertion violationS＋＋（if vithin BCOPe Of claim）

acceptance cycle8−（not8elected）

invalid end8tatQ8−（diBabled by never claim）

State−VeCtOr84byte，depth reached375，errOrB：1

くくく以下省略＞＞＞

最初のモデルでは検証は失敗した。すなわち「ドアは永遠に開かない」という表明は否定され、反例が発見されたのである。これは「正しくない鍵でもドアが開いてしまう」ということを意味する。SPINでは、この時見つかった反例の動作−シーケンスが出力され、この通りにシミュレーションを再実行することで判例を再現することが出来る。これによってわかった事は、仕様の理解に不十分な点があったという点である。すな
わち

．47−

WorkshopReportⅥ）1．14，No．8・●新しい鍵を設定できるという仕様は実は誤りで、正しくは●ロックされているときは、新しい鍵は設定できない●ロックされていないときは、新しい鍵を設定できるでなければいけない。そうでなければ、現在ロッカーが施錠中でその鍵の値を知らなくても、新しい鍵の設定方法さえ知っていれば、施錠中のロッカーに新しい鍵を設定（上書き）して、その鍵を使いドアを開けることが出来てしまう。これではロッカーの役目を果たさない。課題の文章の中には「施錠灯が消えているときに．
っぎのようにして好みの鍵にすることができます」と記述されているが、下線の条件部分に対する考慮がすっ

ぽりと抜け落ちていたわけある。
問題の原因がわかったので「新しい鍵を設定できるのは鍵が開いている場合のみ」という条件チェックをモデルへ追加した。これで再度検証を行い次の出力が得られた。
vming‥forp・0・reductionto be validthe never clainnuSt be Btutter−invariant（never clain8generated fromLTL formulae are stutter−invariant）（Spin VerSion4．2．1−−80ctober2004）＋

Partial Order Roduction

Ful18tateBpaCO8earCb for：nevQr Claim＋aSSertion violationS＋（if vithin8COPe Of claim）

acceptance cycleB＋（faimoB8diBabled）

hvalid Qnd Btate8−（dlBabled by never clain）

State−VeCtOr84byte，depth reached32817，errOrS：0

くくく以下省略＞＞＞

このように、表明が正しいことが確認され、不正な鍵ではドアは開かないことが確認された。今回の課題について行った検証は以上である。

4

演習を通じての感想

4．1仕様作成時における誤りについて
前セクションでとりあげた「新しい鍵を設定できるのは鍵が開いている場合のみ」という部分の仕様の誤りについて大変興味深い例だと思った。これはモデル作成時のコーディングエラーではなく、明らかに仕様作成時の誤りである。＊1そしてモデルはその誤った仕様どおり作成されている。このため、仕様の誤りがそのままモデルにも引き継がれたわけである。従って実際に製品の製造を行い、仕様書に沿ったテストのみしか行わな
ければ、この欠陥はテスト工程でも発見できない。市場に製品が出荷され実際にユーザーが使用してみて初め
・1今回の演習ではモデル作成時に物理的に仕様雷を実際に畜くという行為は行わなかったが当然意識の中では仕様雷は存在する。

＿48．

WorkshopReport

Vol．14，No．8て問題があきらかになるというわけだ。これはもちろん実際の製品ならば巨額の損失を引き起こす可能性をはらんでいる。このような仕様作成時のエラーがmL式を利用した仕様の検証で発見できたということは、モ
デルチェッキングの有効性を示す大きな例だと感じた。

4．2

形式手法に関する誤解

形式的手法、時間論理などといいう言葉からは、なにかしら作成したモデルや仕様が数学的で完全であるという印象を受ける。それらの手法を使うと、まるで魔法のように完壁なモデルや仕様書ができてしまうような錯覚にとらわれがちであるが、このような簡単な演習を通じてでも、それがまったくの幻想であることが良くわかる。

モデルをかいてみたものの、それらを検証する段階になると、これらをどうやって体系的、網羅的に検証していくかを考えることは、試行錯誤の連続で、手探りの作業であった。やはり、新たにものを作るという作業
は経験と知識とひらめきを用いて、迷い苦しまないと達成できない。製品開発のための汎用的解法やアルゴリ
ズムが存在するわけではないのである。以前SIGFMのフォーラムで九州大学の荒木先生が紹介されていた「形式的手法に関する7つの神話」【2】にも同様の指摘があったように記憶している。
形式的手法をつかうと対象を出来る限り厳密に記述しようという努力が要求されるが、この過程が非常に重要なのではないかと思う。出来上がった結果のモデルが完全無欠のものであるという保障はどこにもないが、形式的なモデルを作り上げていく過程では、多くの問題や考慮の抜けを発見できる。形式的モデルを作成する
ことは、いままで自然言語行や、その他の図法、記法などのツールを使用して行ってきた仕様作成とは、また別の角度から、開発の対象システムに光を当て眺める機会を得ることである。モデルチェッキングのみで全ての問題が解決されるというのは全くの幻想であるが、既存の手法やツールを補完し、それらでは発見が難しかった問題点の早期発見につながることも事実である。形式手法に対する過大な期待が払拭される一方、その有効性も実感できたのは大きな収穫であった。

4．3

プロセスの並列性について私の書いたロッカープロセスは、いわば一つの巨大なイベントループになっており、ロッカー内では並列性はない。私が問題を一見したときの印象では、これはごく自然な設計のアプローチであった。これは、私が長年Macintoshのユーザーアプリケーションを開発してきた経験と無関係ではないと思う。Windowシステム

上のアプリケーションでは、イベントループを中心に置いた、イベントドリブン形式のコーディングスタイルになるのはごく自然である。モデルを詳細化してゆく間に、このメインイベントループが、どんどん巨大化してしまい、読みにくい、扱いにくいという不満を感じてはいたが、これは主にPROMELAではサブルーチンが書けないためであると考えていた。＊2このため、ワークショップで、他の人たちが、ロッカーをもっと細かいプロセスに分解しているモデルにしているのを見たときは、新鮮な驚きを感じた。しかしながら、振り返ってみると、そもそもuSerと8afeの間の通信チャネルをbandloとko汀adの二つに分離したのは、キーパッ

ドとハンドルは独立しているので、並列に操作可能という事が念頭にあった。それにもかかわらず、ロッカー

を1つのプロセスにしてまってはなんのために、2つを別のチャネルにしたのかわからない。この部分に関しては、次の機会があれば、きちんと考慮するようにしたいと思う。

＊2これはモデルが詳細に過ぎる事が無いよう意図的にこのように設計されているということだ。

ⅥIl．14，No．8

ⅥbrkshopReport

4．4 抽象化ということ
ホルツマンの教科書［3】にも指摘されているが、初心者の犯しやすい誤りのうち最も多いものは「詳しすぎるモデルを書いてしまう」という事であるという0私の書いたモデルにも、これは当てはまる。数字キーが10個あるという事や、鍵長が4であるという事は、モデルについては本質的ではない0当然キーの種類が少なく、また長さも短い方が検証の際は、時間もメモリ使用量も節約できる。この点については改善の余地が大いにあると思う。＊3

4．5

その他

これはモデルチェッキングとは直接関係はないことであるが、シミュレーションをしている最中に、ロツヵーの仕様に関して次のようなことを考えた0ユーザーは、ロックが解けたのに気がつかず、ひたすらキーを押し続けるかもしれない。このような行為が続くと、気がつかないうちに新しい鍵でロックしてしまう可能性もある。そうすると、このユーザーは（おそらく）新しく鍵を設定したことを意識していないので、その鍵がゎからず、2度とロッカーを開けられなくなってします0これを防ぐためには「新しい鍵を設定するためには、ロックが解除され、ハンドルを回して一度ドアを開く必要がある」という仕様を追加するが良いのではないだ
ろうか。このような点に気がつくのは非決定的な実行が記述でき・それをランダム実行するシミュレーションが可能なSPIN／PROMELAの障れたど利益と言える0・3ただこの点に関しては何も考えずに作ったとき、どのあたりまで検証可能なのかツールの実力を試してみたい、という気持ちもぁった。当然なにも考えないと、すぐにメモリー不足で検証不能という結果にはなったが0．50・

WorkshopReport

付録AⅥ）1．14，No．8

ロッカーのモデルのPROMELAコード／＊aSSignment for DW2005＄Id：dv2005．pml，Vl．72005／02／0105：22：11nonaka Exp＄＊／＃define K＿OPEⅣ

0＃define K＿CLOSEDl＃define K＿UⅣLOCKED O＃define K＿LOCKEDl＃define KEYLEⅣGTH

4

mtype＝（NUM，CAⅣ，LOCKl；

Cban kQypad＝［0】of（mtype，int）；
chan handle＝［0】of t bitl

bitlock＿StatuS＝K＿LOCKED；／＊initial statelocked，meanSlocked＊／
bit door＿StatllS＝K＿CLOSED；／＊initial State door cIosed

inline Clear＿buf（）td＿StQp t

buf＿10m＝0；
bllf［0］＝−1；
bllf［1】ニー1；
bllf［2】＝−1；
bllf【3】＝−lII

inline open＿tbe＿doorOt
lock●BtatuS＝＝K●UNLOCKED；

assert（lock＿StatlユS＝＝K＿UNLOCKED）；

handle！Ⅹ＿OPEⅣ；
door＿Stat115＝＝K＿OPE∬；aSSQrt（dooLStatlユS＝岩K●OPEN）；
I

PrOCtyPe Safe（）（

．51．

＊／

WorkshopReportⅥ）1．14，No．8

int key；

int blユf［KEYLENGTH］；
int buf＿1en＝0；

int c−1rrentKey［KEYLEⅣGTH］；／＊initial key valueisl，1234日＊／
d＿8tep t

CurrentKey［0］＝1；
CurrentKey［1］＝2；

CurrentKey［2］＝3；
ClユrrentKey【3］＝4；
I

endO：

do

：：kQypad？m（key）−＞
d＿Step（Print・f（Nunberinput‥td．＼n■■，key）；

if：：door＿StatuS＝＝

K＿CLOSED−＞／＊the dooris close，aCCunulate keysinto buf＊／／＊display them on LED＊／buf［0］＝buf［1］；buf［1］＝buf［2］；buf［2］＝bllf［3］；bllf［3］＝key；if：：buL1en＜＝3−＞buL1en＋＋；：：else−＞skipfi；if：：lock＿StatuS＝＝

K＿LOCKED−＞／＊the dooris cllrrentlylockQd＊／

if：：（（buf［0］＝亡CllrrentKey［0］）＆＆（buf［1】＝＝CurrentKey［1〕）＆＆（buf［2］＝≡＝＝CurrQntI（ey［2］）＆＆（buf［3］亡＝ClユrrentKQy［3］））−＞lock．status＝K＿UNLOCKED；
printf（…Unlocked．＼n‖）；CleaLbuf（）／＊1igbtis off［open】＊／：：elsQ−＞Skipfi：：else−＞skip

fi

・52・

WorkshopReport：：door＿StatllSⅥ）1．14，No．8＝＝

K●OPEⅣ−＞／＊if the dooris opQn，ignore the keyinput＊／
printf（一一Door open and keyinputignored・＼n一．）；

Skip
fi
〉

／＊accumulate the datainto the buffer＊／：：keypad？CAN（＿）一＞／＊

cIQar tbe buffer＊／

CleaLbuf（）：：keypad？LOCKL）−＞
d＿Step t
printf（■■Lock Key pressed．＼n）；if：：lock＿StatuS＝＝

K．UNLOCKED−＞／＊Lock the door and set nev key＊／if：：buL1en＝ココ0−＞（／＊use current key andlock＊／lock＿StatuS＝K＿LOCKED；

Printf（HLocked vith the current Key・＼n．T）〉：：buLlen＝＝KEYLEⅣGTH／＊Set net key andlock＊／−＞ t

CurrQntKQy［0］＝bllf［0］；ClユrrentKey［1］＝blユf［1］；CurrentKey［2］＝buf［2］；Currentlくey［3］＝bllf［3］；lock＿StatlユS＝

K●LOCKED；

Clear＿blユf（）；printf（‖Locked vith the nev key・＼n−f）〉：：else −＞ t

Printf（．．Error：inslユfficient nev key・Try again！＼nCleaLbuf（）；）

fi：：else

−＞

skip

fi
）

．53．

）；

ⅥbrkhopReportⅥ）1．14，No．8：：handle？K＿CLOSED−＞／＊handle closed＊／
d＿8tep t

if：：dooLStatllS＝＝K＿OPEⅣ−＞t
door＿BtatllB＝K＿CLOSED；

printf（HDoor cloBed．＼n●り；
I：：8188−＞Bkipfi）：：bandle？Ⅹ＿OPEⅣ −＞／＊bandle＼opened
Checkif

un10Cked

if off，Open the door，Clear tbQ buffer＊／d＿Step t

if：：（10Ck＿StatuS＝＝K＿UⅣLOCKEI））−＞f
door＿StatllS＝K＿OPEN；
printf（一一Door opened．＼nH）；）：：elsQ−＞sk土p

fi
I

Od
I

init trun uBer5（）；
run Safe（）；〉

参考文献【1】山崎利治，DW2005のための問題，2005［2】J・A・Hall，SevenMythsofFbrmalMethods，IEEESoftware，Vol．7，No．5，pp．11−19，1990．

［3】GerardJ・HoIzmann，THESPINMODELCHECKERAddison−Wesley，2004−54．

Work5hopReportⅥ）1．14，No．8

デザインワークショップ2005参加報告
九州工業大学堂園隼人

2005年4月20日

ソフトウエア技術者協会（SEA）主催のデザインワークショップ2005（以下DW2005）の参加報告を行う。
1．DⅥ唱005の概要

開催日時：2005年2月24日（木）〜26日（土）場所：ウェルハートピア熱海
テーマ：ソフトウエア仕様検証技術の最新動向・・PROMEL〟SPINを用いて2．報告の概要

本ワークショップでは、実時間分散システムの設計および検証を行うことのできるモ
デルチェッカSPIN【1】を味見してみた。

ワークショップにあたり、山崎氏から事前に課題として、簡単な電子錠が付いた「物置」【2】が提示された。この物置は、電子錠、入力キー、取っ手、表示窓、施錠灯、ドアから構成されている。これらをプロセスに割り付け、PROMEIJA（PRocess MEta
LAnguage）によりモデルを記述し、SPINを用いて検証を行った。

ワークショップでは、山崎氏より講義を受けた後、グループで演習を行い、最終日に発表と意見交換を行った。
本報告では、ワークショップ後に改めて作成したモデルについて報告する。
3．作成したモデル
3．1．プロセス

検証モデルを作成する上で、物置の各部分をプロセスに割り付けた。物置自体をあらわすシステム内部のプロセスを表1に、環境（ユーザ）をあらわすシステム外部のプロセスを表2に示す。

．55．

WorkshopReportⅥ）1．14，No．＄

表1システム内部のプロセス
プロセス名

keypad役割

数字キーの入力をまとめた4桁の数字と、Lキーをe＿keyに送るプロセス

displaydoor

表示窓と施錠灯のプロセス
扉のプロセス

e＿key

電子錠のプロセス

表2

システム外部のプロセス

プロセス名

役割

key＿JuSher

keypadに入力を送る

door＿OPenerdoorにドアの操作を送る

3．2．チャネル

プロセス間の通信を行うために、表3のようにチャネルを設定した。なお、これらのチャネルはすべて同期チャネルとして設定した。
表3
チャネル名
n

key」】uSher

handledf

送信元

keypad，e＿鬼ey

keypad

送信先

keypaddooLOPener

送信内容

一一1桁の数字一一、日Cキー…、HLキー‖

door

display

e−key

チャネル

一一取っ手の開閉一一一一表示する数字日、‖施錠灯の点消灯■■

一一入力された4桁の数字■−

3．3．共有変数

メッセージ型や局所変数として設定せず、大域変数として設定したものは以下の2つである。これらは、チャネルによる通信で表現するとモデルの記述が冗長になるため、大域変数として設定した。
・扉の状態
・電子錠の状態

3．4．局所変数

局所変数については、付録の中で説明している。

．56＿

WorkshopReportⅥ）1．14，No．8

4．独自の仕様

今回、モデルを作成する上でいくつかの独自の仕様を導入した。
4．1．要求仕様であいまいだった点●

入力が1〜3桁のときLキーが押されたら、表示を消して終わる。

● 数字キーの入力は取っ手の操作により中断されない。
4．2．その他の点●シミュレーションで、電子錠の最初のキーワードがマッチしやすいように、1〜9、C、Lキー以外に■■1234−−を送るようにした。

● 簡単化のために、取っ手を回す動作と開閉の動作をまとめた。

5．キー入力に対するkeypadの動作

上記の仕様の追加により、キー入力に対するkeypadの動作は以下のようになる。
（ア）数字キーの入力①

数字が入力されるとkeypadは現在の入力値について覚えておく。

②

4桁目の数字が入力されたら、e＿keyに4桁の数字をまとめて送り、キーワードとの一致を調べる。

③ 4桁の数字の送信後、表示をクリアして、①に戻る。
（イ）C，Lキーの入力● Cキーが押されると、いつでも入力をクリアする。

●

Lキーが押されると、入力された数字が0，4桁のときはLキーが押されたことを
e＿keyに送る。1〜3桁のときには、e＿keyには何も送らず入力をクリアする。

5．調べた項目作成したモデルに対して以下の項目について検査を行い、妥当性を確認した。
● 「ロック状態で正しいキーワードが入力されたら、アンロック状態になる」● 「扉が開いている間は、物置はロックされない」● 「デッドロック状態には陥らない」●「アンロック状態のとき、1〜3桁の数字を入力してLボタンを押すと、数字が消えるだけである」．57＿

WorkShopReportⅥ）1．14，No．8

6．DW2005以前と以後のモデル
DW2005に参加するにあたり事前に作成したモデルでは、倉庫と環境をそれぞれ1
っのプロセスとして設定していた。それは、倉庫全体を1つの状態推移系として容易にイメージすることができたからである。

DW2005を終えて、本報告を作成するにあたりモデルを再構築した。その際、オブジェクト間の相互作用を見るために、倉庫をいくつかの子プロセスに分割したり、変数をできるだけ局所変数として設定したりするなどの変更を行った。
7．まとめ

ワークショップを通して、PROMELAによるモデルの構築と、その検証ツールであるSPINへの理解を深めることができた。

今回のワークショップのように、演習を行ったり、いろいろな方々の作成されたモデルを見比べ、意見を交わしたりする機会は大変有意義なものであった。

．58．

WorkshopReport

付録Ⅵ）1．14，No．8

作成したhomelaモデル＃defineDOOR＿OPENl＃defineDOOR＿CLOSEO＃de丘neEKEY＿UNLOCKl＃defineEKEY」．OCKO＃defineIJAMP＿ONl＃defineLAMP＿OFFO

mtype＝iinputNum，C，1〉；／☆キー入力★／mtype＝〈rediSPlay；lampi；／☆表示★／

mtype＝〈sOpen，SClose〉；／★ドアの開閉☆／mtype＝〈num4〉；／★4桁の数字☆／／☆共有変数☆／
Showintdoor＿State＝DOOR＿CLOSE；／☆ドアの状態☆／

Showinte＿key＿State＝EKEYJJOCX；／☆電子錠の状態☆／／☆チャネル☆／chand＝［0】ofimtype，int）；／★表示・ランプ用☆／

chann＝［0】ofimtype，int）；／☆キー入力用賀／

chanhandle＝［0］ofimtype）；／★取っ手用☆／chanf＝［0］oflmtype，int〉；／★入力数字4個組み，Lボタン☆／／☆キー入力を受け取るプロセス☆／
activeproctypekeypadOi
inti；／☆入力★／

intalLnumS；／＊全入力☆／
intnum＿JOint；／☆入力総数☆／

ZerO・

Skip；
d＿Step〈i＝・1；

dLnumS＝−1；
num＿JOint＝0；）・59・

Ⅵ）1．14，No．8

ⅥbrkshopReport

d！redisplay（alLnum8）；

if：：n？inputNum（i）・＞alLnumS＝i；num」）0int＋＋；
d！redisplay（alLnums）；gotoone；：：n？cO・＞gotozero；：：n？10ウm（・1）；gotozero；

丘；

One：
if

：：n？inputNumG）・＞alLnumS＝alLnumS★10＋i；
d！rediSplay（alLnums）；num＿JOint＋＋；gototwo；：：n？cUゥgotozero；：：n？1（」ゥgotozero；

丘；

two：

if
：：n？inputNum（i）・＞alLnums＝all」lumS☆10＋i；
d！redisplay（alLnumS）；num」）Oint＋＋；gotothree；：：n？C（」・＞gotozero；：：n？10ウgotozero；

丘；

three：

if：：n？inputNum（i）−＞alLnums＝alLnumS＊10＋i；
d！redisplay（alLnums）；num＿JOint＋＋；

nnum4（alLnumS）；gotozero；：：n？C（」−＞gotozero；：：n？lO，＞Ⅷ1（・1）；gotozero；

丘；
）

・60・

WorkshopReportⅥ）1．14，No．8／☆表示窓・施錠灯のプロセス☆／
activeproctypedisplayOi
intd＿num＝・1；
boollockJamp＝1；／☆表示窓の数字★／／☆施錠灯★／

end：

do：：d？redisplay（d＿num）・＞

げ：：（d＿num＜0）−＞printql￥n）；：：（d＿num＞＝0）・＞printf（一．％d￥n，d＿num）；

丘；：：d？lamp（IJAMP＿ON）−＞lockJamp＝IJAMP＿ON；：：d？lamp（IJAMP＿OFF）・＞locILlamp＝LAMP＿OFF；od；〉／☆電子鍵のプロセス★／
activeproctypee」【eyOiintkeyword＝1234；

intinput＝−1；／☆現在のキーワード☆／／☆keypadから送られた4桁の数字☆／

cloSe：

e＿key＿State＝EKEY＿LOCK；
if：：f？num4（input）・＞if：：（input＝＝keyword）−＞d！lamp（LAMPj）FF）；gotoopen；：：（input！＝keyword）・＞gotoclose；

丘；：：PIU−＞gotoclose；

丘；

Open：

e＿key＿State＝EKEY＿UmOCK；
input＝・1；

・61・

Ⅵ）1．14，No．8

ⅥbrkshopReport

Open2：
if：：f？num4（input）−＞gotoopen2；：：PIUウif：：（door＿State＝＝DOOR＿OPEN）−＞gotoopen；：：（door＿State＝DOORLCLOSE）・＞d！lamp（LAMP＿ON）；if：：（input＞＝0）−＞keyword＝input；gotoclose；：：（input＜0）・＞gotoclose；丘；丘；／★ドアのプロセス★／
activeproctypedoorO〈close：

dooLState＝DOOR＿CLOSE；
if：：handle？sOpen・＞if：：（e＿key＿State＝EKEYJJNLOCK）−＞gotoopen；：：（eJkey＿State＝EIEY＿LOCK）・＞gotoclose；丘；：：handle？sCloSe・＞gotoclose；

丘；

Open：

dooLState＝DOOR＿OPEN；
if：：handle？80pen−＞gotoopen；：：handle？sClose−＞gotoclose；

丘；
）

．62．

WorkshopReportⅥ）1．14，No．8／☆キーを入力するプロセス☆／
activeproctypekey＿JuSherOido：：atomic（／☆最初のキーワード1234がシミュレーションで早くおこるようにするため☆／n！inputNum（1）；n！inputNum（2）；n！inputNum（3）；n！inputNum（4）；〉：：n！inputNum（1）；：：n！inputNun（2）；：：n！inputNum（3）；：：n！inputNum（4）；：：n！inputNum（5）；：：n！inputNum（6）；：：n！inputNum（7）；：：n！inputNum（8）；：：n！inputNum（9）；：：n！inputNun（0）；：：n！C（・1）；：：n！1（・1）；od；）／★ドアを開閉するプロセス丈／
activeproctypedool・＿OPenerOido：：（dooLState＝DOOR＿CLOSE）・＞handle！sOpen；：：（door＿State＝DOOR＿OPEN）−＞handle！sCloSe；
od；
）

・63．

WorkshopReport

Vol．14，No．8

参考文献［11GerardJ．HoIzmann．TheSpinModelChecker：PrimerandReferenceManual・【2】山崎利治

DW2005のための問題【3】山崎利治

ソフトウエア仕様検証技術の最新動向．64．

PROMEIA／SPINを用いてWorkshopReport

Vol．14，No．8

デザインワークショップ2005参加報告
張暁晶

九州大学大学院システム情報科学府情報工学専攻

修士課程1年
TEL：092−642−3869
Zhang＠ale．csce．kyushu−u．aC．jp

2005年4月4日−、ワークショップの要約
ソフトウェア技術者協会（SEA）主催のデザインワークショップ2005の参加報告である。
ワークショップでは、金庫を模型検査言語PROMELAにより模型化し、SPINというツールで模型検査する演習を行った。演習では、参加者が3チームに分かれてそれぞれ模型を構築した。張は、同チームの（株）ニルソフトの伊藤さんと（株）デンソーの中里さんとともに金庫の模型化に挑戦した。

伊藤チームでは、模型化する対象の本質を見出し、まずそこだけを模型として構築した。
金庫の場合においてはドアの開閉と鍵の開閉が一番肝要だと考え、最初の模型をドアと鍵の二つのプロセスにより構成した。演習後に張がチームメンバの指導の下、この模型にパスワードの照合や、ボタン入力などの機能を付け加え、問題文に近い金庫の模型を作り上げた。以下に作成した金庫模型を説明する。なお、PROMELA模型は付録に添付する。
二、模型の解説

張が作成した模型では、金庫の要素を大きく鍵、ドア、液晶表示窓の三つに分けた。それぞれを独立したプロセスとして作成した。
まず液晶表示窓プロセス1cdはユーザのボタン入力を受け付ける。つまり液晶表示窓を表す変数W土ndowを入力バッファとして使っている。このプロセスはボタン入力の通信路
Chanbuttonからメッセージを受信し、そのメッセージが数字ボタンが押されたことによるものであれば、バッファにためていき、CLEARボタンによるものであればバッファをクリアする。LOCKボタンによるもので、バッファが4桁とも空であれば「施錠しろ」イベントを起こし、4桁とも埋まっていれば「パスワードを変更しろ」のイベントを起こす。ただし入力を受け付けるのはドアが閉まっている時のみである。
次にドアプロセスd00rはドアの状態を変更する。ユーザからドアの状態を変更するイベントが発生した時イベントの種類、すなわち開けるか閉めるかによってドアの状態を変化させる。通信路chand00rから、「ドアを開けろ」イベントを受信すると、ドアが閉まっている状態でかつ鍵が開いていることを確認して、ドアの状態を開いている状態に変更する。
「ドアを閉めろ」イベントが来た時も同様であるが鍵の確認はしない。

．65．

WorkshopReportⅥ〉1．14，No．8

次に鍵プロセスkeyは鍵の状態を変更する。通信路chanlockからIcdプロセスが起こした3種類のイベントを受信する。まず「開錠しろ」イベントが来るとドアが閉まっていて鍵が閉まっていることを確認して、次に入力バッファとパスワードを照合して一致すれば鍵の状態を開いている状態に変更する。一敦しなかったり入力桁数が足りない場合は何もしない。次に「施錠しろ」イベントが来た場合ドアが閉まっていて鍵が開いていることを確認して、LOCKボタンが押されたら鍵の状態を閉まっている状態に変更する。最後に「パスワードを変更しろ」イベントが来た場合、ドアが閉まっていて鍵が開いていることを確認して、パスワードを入力されたものに変更して鍵の状態を閉まっている状態にする。

以上が金庫の構成要素のプロセスで、外界から金庫に命令する、つまり通信路を通じて信号を送る実体として、ユーザプロセスを設けた。ユーザは、「ドアを開けろ」、「ドアを閉めろ」のイベント、数字ボタンとCLEARボタンとLOCKボタンを押す動作を、ランダムにいずれかを起こすことができる。イベントというものをユーザの意思として捕らえており、
いずれもinline関数として定義した。

上記のモデルをSPINを使ってシミュレーションした結果、期待した動作が行われた。

「ドアが開いている状態と鍵がかかっている状態は同時に成立できない」という性質を検証しようとNeverClaimを記述したが、SPINによるVerificationでは開始直後にシミュレーションが停止し、モデルにまだバグが残っていることが確認できた。今後の作業としては、Never Claimに抵触しないようモデルを修正する必要があると思われる。

三、模型検査の結果

今回‡SPINというGUIのSPINを用いて作成した金庫模型の模型検査を行った。SPINではシミュレーションとVerificationができ、シミュレーションでは模型の一通りの動作（確率的なだが）を見ることができる。また、Verificationでは模型がある性質を満たしているかどうかを検証できる。
今回の模型をシミュレーションにかけた結果、ほぼ要求を満たす動作をしていたと確認できた。ユーザプロセスの最初で1234と登録させているパスワードを入力させている。その結果金庫が開錠されたことが確認できた。また、開錠された状態でLOCKボタンを押した

場合金庫が再び施錠されることも確認できた。鍵がかかっていない状態でユーザがドアを開けるとドアが開いたことも確認できた。
Verificationのほうでは、模型の満たすべき性質として、「ドアが開いている状態と、鍵がかかっている状態は同時に起こりえない」という性質をSPINで検証しようとしたが、返された結果として、今回作成した模型ではそのようなことは起こりうるとあった。これは模型に欠陥が存在することを意味している。張の経験不足により現在のところはまだこの欠陥を修正するに至っていない。

．66．

WorkshopReportⅥ〉1．14，No．8

四、感想
今回のワークショップで初めてPROMELA言語とSPINを使って模型検査を体験した。また、今回の演習で模型検査のための模型の作り方を主に考えてきた。模型のモジュール化にプ
ロセスという概念を用いているところに馴染みがなかったので、モジュールの切り分け方が難しいと感じた。そのため、模型化の対象の本質を明確にするため、シンプルな模型を作成し後に詳細化する手法を取り入れた。
付録：張が作成した金庫模型＃define KEY＿LOCKEDl／★鍵が閉まっている★／＃define KEY＿UNLOCKED O／＊鍵が開いている★／＃define D00R＿CLOSEl／★ドアが閉まっている★／＃define D00R＿OPEN O／★ドアが開いている★／＃define KEY＿LENGTH4／★パスワードの桁数★／／＊

以下never claim用★／＃define open（d00r＿StatuS＝＝DOOR＿OPEN）／＊ドアが開いている状態＊／＃definelocked（key＿StatuS＝＝KEY＿LOCKED）／★鍵が閉まっている状態★／

mtype＝†NUM，C．Ll；／★信号の型は数字ボタン、C工JEARボタン、10CKボタン★／

chan chand00r＝［10］of（intH／★ドア状態を流す通信路★／

chan chanlock＝【10］of tint）；／＊鍵状態を流す通信路＊／

Chan chanbutton＝［200】ofimtype，intl；／＊ボタン入力を流す通信路★／

Show bit door status＝

D00R CLOSE；／★ドアの状態（初期値は閉まっている）★／

Showint E changed00r＝

0；／★ドア状態変更に関するイベント ★／／★

0：イベントなしり／★1：「ドアを閉めろ」イベント発生り／★ 2：「ドアを開けろ」イベント発生★／Show bit key＿StatuS＝KEY LOCKED；

・67．

WorkshopReport

ⅥIl．14，No．8／★鍵の状態（初期値は閉まっている）★／

Showint E changelock＝0；／★鍵状態変更に関するイベント ★／／★ 0：イベントなし★／／★1：「施錠しろ」イベント発生り／★ 2：「開錠しろ」イベント発生り／★ 3：「パスワード変更しろ」イベント発生★／

Showint window【KEY＿LENGTH］；／★液晶表示窓（ユーザ入力バッファ）り／★各桁には−1（無表示）もしくは0−9が入る

りShowint password【KEY■LENGTH】；／★金庫に設定されているパスワードり

inline opend00r（）（／★ドアを開ける＊／d step t
E changedoor＝

2；

Chand00r！E changed00r；／★「ドアを開けろ」イベントの発生を通信路chand00rに通知＊／
E changedoor

＝

0；

1；

）；

inline closedoor（）（／★ドアを閉める★／

d step t
E changed00r＝1；

Chand00r！E changed00r；／★「ドアを閉めろ」イベントの発生を通信路chand00rに通知りE changedoor

＝

0；

H
I；

inline sejy〇日（／★施錠する★／
d step（．68一

WorkshopReportⅥ）1．14，No．8

E changelock＝1；

Chanlock！E changelock；／＊「施錠しろ」イベントの発生を通信路chan10Ckに通知＊／
E changelock

＝

0；

）；

）；

inline kaijyo（）（／★開錠する
E changelock

＝

＊／

2；

Chanlock！E change10Ck；／＊「開錠しろ」イベントの発生を通信路chanlockに通知★／
E changel0Ck

＝

0；

）；

inline henko（日／★パスワードを変更して施錠する
E changelock

＝

★／

3；

Chanlock！E changelock；／★「パスワード変更しろ」イベントの発生を★／／★通信路chanlockに通知★／
E changelock

＝

0；

）；

inline clear（）（／＊液晶表示窓をクリアする★／

d＿Step（Wlndow【0】＝−1J

Wlndow【1】＝−H

Wlndow【2】ニーいWindow［3】＝

−H

I；

）；

active proctypelcd（）priority1001／★液晶表示窓のプロセス★／
int but；do：：1f：：Chanbutton？NUM（but）T＞／★数字ボタンが押されていたら

・6，・

★／

WorkshopReportⅥ）1．14，No．8

d step（if：：d00r StatuS＝＝

D00R CLOSE−＞

Window［0】＝W土ndow［1】；Window【1】＝Window【2】；Window【21＝Window【3］；Window［3］＝

but；

⊥f

：：（window【0】！＝−1＆＆Window【1］！＝−1＆＆Window【2日＝−1＆＆window【3］！＝−1）−＞kai〕yo日；：：else一＞skip；

fl：：d00r StatuS＝＝

DOOR OPEN

−＞

skip；

／★ドアが開いている時は入力を無視★／
fi；
1；：：Chanbutton？C（0）−＞／★

CLEARボタンが押されていたら／★

LOCKボタンが押されていたら★／Clear（）；：：Chanbutton？L（0）−＞★／if：：（Window［0］！＝−1i＆window【1］！ニー1＆＆Window【2］！ニー1＆＆Window【3】！＝−1）−＞henko（）；：：（Window【0］＝＝−1＆＆window［1］＝＝−1＆＆windowl2］＝＝−1＆＆Windowl3］＝＝−1）−＞sejy〇日；：：else−＞ciear日；
f土；
fl；

Od；
）

active proctype d00r（）prioritylOOt／★ドアのプロセス★／
int x；

OPEN：／★ドアが開いている状態★／
do：：Chand00r？X −＞if：：（X＝＝1＆＆d00r＿StatuS＝＝D00R＿OPEN）−＞

d00r＿StatuS＝D00R CLOSE；gOtO CLOSE；．70・

WorkshopReportⅥ）1．14，No．8／★「ドアを閉めろ」イベントが発生したら開いているドアを閉める ★／：：else

−＞

skip；

fl；

OdJ

CLOSE：／★ドアが閉まっている状態★／
do：：Chand00r？X −＞if：：（X＝＝2＆＆

key＿StatuS＝＝KEY＿UNLOCKED＆＆

d00r＿StatuS＝＝D00R＿CLOSE）−＞

d00r＿StatuS＝D00R OPEN；gOt0

0PEN；／★「ドアを開けろ」イベントが発生したら ★／／★鍵が開いていれば、閉まっているドアを開ける ★／：：else

−＞

sk⊥p；

fl；
Od；
）；

active proctype key（）prioritylOO（／★鍵のプロセス★／

int x；

int but；

d＿Stepり★初期パスワードは1234★／

password【01＝：＝
password【1］＝2；password【2］＝3；password［3］＝4；）；LOCK：／★鍵が閉まっている状態★／
do：：Chanlock？Ⅹ一＞

if：：（Ⅹ＝＝2＆＆d00r＿StatuS＝＝D00R＿CLOSE＆＆

key＿StatuS＝＝KEY＿LOCKED）−＞／★「開錠しろ」イベントが発生したら ★／／★ドアが閉まっていて鍵も閉まっていればパスワード照合に進む★／
if：：（Window［0］＝＝PaSSWOrd［0】＆＆．71．

WorkshopReport

Wl．14，No．8

Window【1】＝＝paSSWOrd【1】ふ＆Window【2］＝＝PaSSWOrdl2］＆＆

Windowl3］＝＝

PaSSWOrd【3日−＞／★入力がパスワードと一致したら開錠する ★／key＿StatuS：：else−＞＝KEY＿UNLOCKED；Clear（）；gOtO UNLOCK；

sklp

fi；
：：else

一＞

sklp；

fl；
Od；

UNI」OCK：／★鍵が開いている状態★／
do：：Chanlock？Ⅹ −＞if：：（X＝＝1＆＆d00r＿StatuS＝＝DOOR＿CLOSE＆＆

key−StatuS＝＝KEY＿UNLOCKED）−＞／★「施錠しろ」イベントが発生したら ★／／★ドアが閉まっていて鍵が開いていれば次に進む★／
key status：：（Ⅹ＝＝3＆＆

keyTStatuS＝

KEY LOCKEDJgOtO LOCK；

d00r＿StatuS＝＝D00R＿CLOSE＆＆＝＝KEY＿UNLOCKED）一＞／★「パスワード変更しろ」イベントが発生したら ★／／★ドアが閉まっていて鍵が開いていれば次に進む★／
PaSSWOrdl0］＝

Window【0］；PaSSWOrd［1］＝Window【1】；password【2】＝Wlndow【2】；PaSSWOrd【3］＝Window【3］；key status

KEY LOCKED；＝

clear（）；／★パスワードを変更して施錠する
gotoI」OCK；
fi；

Od；
）；

active proctype user（）（／★ユーザのプロセス
ChanbuttonlNUM（1）；Chanbutton！NUM（2）；

．72．

★／

★／

WorkshopReport

ⅥIl．14，No．8

Chanbutton！NUM（3）；Chanbutton！NUM（4）；／★ユーザはランダムに以下の換作を行う ★／do：：Opend00r日；：：Closed00r（）；：：Chanbutton！NUM（0）；：：Chanbutton！NUM（1）；：：Chanbutton！NUM（2）；：：Chanbutton！NUM（3）；：：Chanbutton！NUM（4）；：：Chanbutton！NUM（5）；：：Chanbutton！NUM（6）；：：Chanbutton！NUM（7）；：：Chanbutton！NUM（8）；：：Chanbutton！NUM（9）；：：Chanbutton！C（0）；：：Chanbutton！L（0）；Od；）；

never（／★！＜＞（OPen＆＆locked）＊／／★鍵が掛かってるときにドアは開かない★／
TO in土t：if
日locked）＆＆（OPen日：：（1）−＞−＞

goto TOinit

goto accept＿all

fl；accept ali：

Sklp；
）；

＿73．

ⅥbrkshopReport

ⅥIl．14，No．8

Promela及びSpinについてのノート
伊藤 昌夫（nil）

2005年1月5日

そして，本来的時間性にあっては，＜将来＞と＜既在＞とく瞬間的現在＞が緊密に結びつき，しかも＜将来＞が圧倒的な優位に立つ．
「ハイデガー拾い読み」 木田元

1概要
反応系（基本的にシステムは停止せず，イベント駆動するシステム）を考える上で，イベントの順序列や並行プロセスを記述することは必須である・PROMELA（PROcessMEtaLAnguage）はCSP（Communicating

SequentialProcesses）に基づいている．最初に時間論理とCSPについて概観し，次にPromelaと実行系であるSPIN（SimplePromelaINterpreter）について見る＋l spINは，線形時間論理（IRL：LinearTbmporalbgic）を扱うことができる．なお，この短い文でそれぞれの手法についての全体を知ることはできない．あくまで，ホンの糸口を与えるだけである．詳細は，参考文献を当たること．

2

時間論理とCSP

2．1時間論理
時間論理（temporallogiC）は，様相論理（modallogiC）の特殊な型であり【7］，Kripke構造■2の性質を記述するのに用いることができる．即ち，どのような実行順でふるまうべきか，或いはどういうふるまいが不正であるかを示す時に使用する・Kripke構造は，K：＝〈P，，S，Sb，T，L）で示される．ここで，P，は，原子命題の組みであり，方は，状態の組み，鋸は初期状態である・r⊆ぶ×βは，全ての遷移を示し，J：∫→ア（Pr）
は与えられた状態βにおいて，原子命題が正当であることを示す状態ラベル化関数である．

時間論理として特殊なものに線形時間論理（LTL）がある，線形時間論理とは，離散的で，任意の点は，必ず一つの可能な未来を持っている．また，それ以前の時がない開始時刻がある．今，p∈Prならば，線形時間論理式￠は次のように再帰的に定義することができる．

車：＝p HmelかbeIr射￠∧射￠∨￠l弟日印日揮卜匪甘方，ダ，G，打は時間演算子と呼ばれ，経路町の性質を示す．
■1promelaもSpinも共に略語であるが，以後はそれぞれPromela，Spinと記述する）．

■2有限状態機械の一種であり，グラフで表現される．グラフ上でノードは，系の到達可能な状態を表し．エッジは状態遷移を表す＿74．

WorkshopReport

Ⅵ軋14，No．8

・ズ：現時点の直後の状態において某である（○とも書かれる）．
・ダ：何れかの将来において真になる．（◇とも記述される）．

・G：現時点以降，全てにおいて真である（□）とも記述される）．
●打：￠lF￠2としたとき，経路上のある点であが真になるならば，それ以前の状態￠1も真であるなら
ば，真である■3．

g，汀巨タは， 構造∬において，論理式タは時系列汀において正しい ということを表す．これを用いて，次のような定義をすることができる．
・方，訂巨れe・方，汀巨p好p∈i（句），ここで，p∈Prであり，恥は汀の最初の状態である．

・方，訂巨「￠貯mOfg，汀巨￠

・方，汀巨￠1∧￠2

好∬，汀巨￠1dndg，汀巨由・方，汀巨￠1Vあ相方，汀巨￠10rg，汀巨あ・∬，訂巨ズ￠げ∬，汀1巨￠・方，訂巨ダ￠好例えば，∬，訂1巨￠を満足するi≧0が存在する・方，汀巨G￠

好全ての壷≧0に対して，方，訂i巨￠が成り立つ

・方，汀巨￠1こJ毎

げ盲≧0を満足する古に対して，∬，汀；巨あであり，かつ，ブ∈0，…，i−1である全てのjに対して，方，汀メ巨￠1が成り立つ

システムには幾つかの性質（p叩e嘲）がある．システムの性質を知ることができるというのが，時間論理に従って記述することの利点である．性質には幾つかの区分がある．例えば，熟、ことは決して起こらないという安全性（叫存毎）及び，何時かは良いことが起こるという活性（肋emegβ）である．例えば，障害物があるときにロボットアームを伸ばしてはいけないという不変条件が維持されることは仕様上の安全性であり，デッドロックを起こさないことというのは設計上の安全性に関わる性質である．また，意図しない終了をしない，あるイベントが生起したときには，対応するアクションを実行しなくてはいけないというのは仕様上或いは設計上の活性に関わるシステムの性質である．ここでは，【1］に従って時間論理の構造化から分類した例を挙げる．
・安全性（β（ホ旬）‥□p・保証性（タMm雨ee）：◇p・拘束性（08和也如れ）＝

ロpV◇曾・応答性（代印0耶e）：口◇porロ（p→◇曾）

・永続性（perβ豆β如ce）：◇□p・反応性（r班C抽e）：□◇pv◇口曾

一般に，LTLを用いて，実務者が仕様を記述するには訓練を必要とする．そのためにデザインパターンに類似したパターンも提案されている【81．証明すべきシステムの性質とは，逆にいえば，（それが適切に分類されていれば）容易に仕様として記述できたところで，後は証明器に委譲することができることになる．その観点からの分類が以下のものである．

■3上記の肌用演算子は，強いM痛打と呼ばれるときもある・弱いunは（通常Wと示される）では，￠1【J（毎日叫1）と等価になる・即ち，￠1が貢であれば，￠2の値には関係しない．

．75．

Ⅵ）1．14，No．8

ⅥbrkshopReport

生起（occurence）

不在（absence）
普遍（universality）
存在（existence）

時間境界付存在（boundedexistence）
順序（order）

先行（precedence）
反応（responSe）

複合（compound）

先行連鎖（precedencechains）
反応連鎖（responsechains）

ブーリアン（boolean）

例えば，「プロセスAが値を更新してから（updateA）でないと，プロセスBは読ん（readB）ではいけない」，という仕様は，反応パターンを使って次のように書ける．
□（叩血feA＜◇柁αdβ）．76．

WorbhopReport

2．2Ⅵ）1．14，No．8

CSP

CSPで扱うプロセスは，データ構造とサービスをカプセル化したコンポーネントである．但し，概念的なオブジェクト指向とは異なり，データ構造ばかりか，サービスも隠蔽されている．他に対して開かれているのはチャネルを介して行う通信のみである．
CSP＊4は，広い意味でプロセス代数の一つと呼ばれる．基本プロセスを表す定数記号及びプロセスを合成するための演算記号の集合を定め，それらからなる代数項としてプロセスを定義する【3】国．CSPでは，観測可能なイベントを用いて，複数のプロセスからなるシステムを記述する．プロセス間のやりとりはアクションとして記述する．なお，プロセスのふるまいに影響を与えるイベントの集合をアルファベットと呼ぶ．この時，プロセスが起動したイベントと，他から受け付けるイベントは区別しない．
次のプロセスPHONEにおいて，
躇0〃茸＝摘ngJα耶Wer→grOf）．

プロセスPHONEは次のような有限個の軌跡を持つ．
くく），〈血タ），恒九g，α耶Wer〉）

一方で次のように再帰表現されるとき，その軌跡は無限である．
CエOC打＝加Cた→CエOC打

今，アルファベット（瓜，む，C）を持つプロセスPを考える．また同様に，アルファベットくわ，C，d）を持つプ
ロセスQを考えると次図のように表現することができる（【3】pp．54−55）．
￣⊥￣てこ

図1独立した2つのプロセス

これら2つが並行して協調動作する場合，同じイベント同士をつなぐことによって，次のような接続線図を書くことができる．ここで，図1のあはメッセージの通信路と考えることもできる．従って，通信は次のように対として考えることができる．今，チャネルの名前をCとし，メッセージをUとし：タがチャネルCを通して通信できる全てのメッセージの集合，通信から要素チャネル及びメッセージを取り出す関数はそれぞれ次のようになる．

αC（P）＝（可C・V∈ranαP），C克也mmeg（C・可＝C，meββαge（C・可＝γ．77．

WorkshopReportⅥ）1．14，No．8

（Ⅱ）

図2

並行して動作するプロセス

次に，α点＝tc，e）となるプロセスRが追加された場合，次図となる．

（Ⅲ）

図3

並行して動作する3つのプロセス

しかし，これを詳細を隠蔽した次図のように単一プロセスとして記述することもできる．

（Ⅳ）

a（PuqせR）

図4

単一プロセスとしての表現■4communica．tingSequentialProces8eSの略．78．

WorkshopReport3Ⅵ）1．14，No．8

PromeJaとSpin

3．1

Promela下記に例を示す．文法とについては，【51を参照のこと．
1

mtype＝（msgtype）／＊メッセージ型の宣言り

2

Chan name＝［0】of fmtype，byte）；／＊ランデブーポートの宣言＊／

3

aCtive proctype A（）／＊プロセスの宣言Aり4f name！msgtype（124）；＄

name！msgtype（121）；

6 ）7

aCtive proctype B（）

8

（

O

name？msgtype（state）；／＊プロセスの宣言B＊／

byte state；

10 ）

11

／＊プロセスの生成＊／

init

12

I atomic（run A（）；run B（））

13 ）この例では，プロセスAは最初のメッセージをバッファサイズがゼロであるランデブーポートに送信したところで（stateが124を持つ），実行不能になる．バッファサイズが2以上の場合，プロセスAはプロセスBの終了を待たずに停止することができる．バッファサイズが1の時は，最初のメッセージを送信後，Bがポートから値を取得したところで，Aは再度送信する．そこで，両方とも停止状態となる．

3．2

Spin

Spinは，並行システムの論理的な一貫性（特に，データ通信プロトコル）を分析するためのツールである
【2】・

図5

Spin全体図

先に述べた時間論理に関して，Promelaは直接的には関与しない．図1に示すように，SpinはIRLを理解

・79．

WorkShopReport

Vol．14，No．8

するパーザを持つ（【2】，pp・141）沌・1＄

spin−f

2neVer t

さ

／＊

＜＞H p
＜＞【1p

＊／

TO＿init：4if5：：（（p））−＞goto accept−S46：：（1）−＞goto

7

8

TO＿initri；

aCCept＿S4：

p

if

lO

：：（（p））−＞goto accept−S4

11

ri；

12）

ここでは，永続性を展開している．pが真であるならば，自動的に生成されたラベルaccept＿S4に飛び無限ループする．そうでないならば，評価を繰り返すPromelaの式を生成している．

★5until演算子については，強いもののみをサポートする．80−

WorkshopReport

4

ⅥIl．14，No．8

まとめ
CSPにおける概念的な枠組みは，自己充足したコンポーネントである【6】．また，時間論理は，（反応系の）システムの性質について，妥当性確認する機会を与える．また，検証することも可能であり，より信頼性の高いプログラムを作る上で有益である・また，有限状態検証の一つであるSpinツールは，いわゆる「状態空間爆発（statespaceexplosion）問題」に対して，有効に機能する．実世界において，WEBや組込み系といった反応系の高い信頼性を保持するシステムを，多数のコンポーネントから構成しようとするとき，これらアプ
ローチは工学としての基盤をなすと考えられる．

参考文献［11ZoharManna，AmirPnueli，THETEMPORALLOGICOFREACTIVEANDCONCURRENTSYSTEMS，Springer−Verlag，1991・［2】http‥／／spinroot・COm／spin／Man／Manual．htmll3】C・A・R・Hoare，COMMUNICATINGSEQUENTIALPROCESS，http：／／www．usingcsp．com／，2004（邦訳は・吉田訳「ホーアCSPモデルの理論」，丸善，1992）．
【4】堀田英一，プロセス代数の意味論，情報処理学会誌，Ⅶ1．37，No．4，1996．
［5】GerardJ・Holmann，THESPINMODELCHECKER，AddisonWesley，2003．古いがPr。mela及びSpinを扱っているHoIzmann氏の別の著書にDESIGNANDVALIDATIONOFCOMPUTER

PROTOCOLS＊6（邦訳：コンピュータプロトコルの設計法）がある．
［6］SteveSchneider，CONCURRENTANDREAL−TIMESYSTEMS−THECSPAPPROACH−，Wiley，［7】AllenEmerson，TbmoralandModalLogiC，（inHandbookofTheoreticalComputerscience），EIT

SeVeirScience，1990．

［8JMatthewB・Dwyer，etal，PropertySpecificationPatternsforFiniteTStateVerification

ターン集については，http：／／patterns・prOjects．cis．ksu．edu／にある．

6，原書の電子版はhttp：／／spinroot．com／spin／Doc／popd．html，実際のパWorkshopReportⅥ）1．14，No．8

Promegα簡介
伊藤 昌夫（nil＠nil・CO・jp）

2005年2月23日

1概要
これは，Promeraについてのごく簡単な解説である．基本的には，【1】のページの構文に関する部分の拙い訳になっている．記述が古い部分に関しては，4．2．4の仕様に合わせた．なお，参照個所が本資に含まれていない場合がある．

2f）7℃megαPmomeJαプログラムはプロセス，メッセージチャンネル，および変数から構成される．プロセスは大域的なオブジェクトである．メッセージチャンネルと変数は大域的ないしは局所的に宣言できる．プロセスには，振る舞い，チャネル，大域変数を記述し，プロセスを実行する環境を規定する．

2．1語彙に関する仕様
5つの字句クラスがある：識別子，キーワード，定数，演算子，および文分離子．空白，タブ，ニューライ
ン，改行，およびコメントは字句を分離するために用いる．1つ以上の解釈が可能であるなら，字句を構成可
能な最も長い文字列として解釈する．
2．2

コメント

コメントは，／＊から始まって，＊／で終わる．コメントは入れ子にしても良い・

2．3

識別子

識別子は，一文字／ピリオド／アンダースコアで始まり，ゼロ個以上の文字，数字，ピリオド，アンダース

コアの何れかがにより連接されたものである．
2．4

キーワード

以下の識別子は，キーワードとして予約されている．
whileはキーワードではないことに注意．

●82．

WorkshopReportⅥ）1．14，No．8

Listl Pmmekのキーワード
activebool

atomicassert

break

byte

d＿SteP

D＿prOCtyPe

do

empty

enabled

fi

full

goto

hidden

ir

init

int

len

mtype

nempty

never

nfu11

od

or

elBe

pc＿Value

printfPriority

provided

run

Short

timeotlt traCe
Xr

2．5

bit

chan

proctype
8how

typedef

unlessskip

unslgned

XS

ラベル

ラベルは識別子であり，最後にコロン（：）を付加する．全ての文はラベル化できる．印d，pr関門ββないしはdCαpfで始まるラベルは特別な意味を持っている．

2．6

定数

定数は10進整数を表す数字列である．浮動小数点はサポートしていない．2つの方法で定数のための英字名を定義できる．最初の方法はC言語風のマクロ定義である．
List2＃define NAME

定数5

もう一つは，キーワードm如〉eを利用する．シンボル定数参照．

2．7式（expression）

式を作成するために以下の演算子と関数を使用できる：
List3
＋

＞＝

＆
くく

len（）

＊

く

／

演算子と関数

％

く＝

日

＆＆

＞

！＝

I

＞＞

l

＋＋

empty（）nempty（）

mrull（）full（）run eval（）enabled（）

pc＿Value（）

ほとんどの演算子は2進数演算用である・文脈によって，論理的な否定（！）とマイナス（−）演算子は単項と2進演算の両方であることができる．＋＋と一一演算子は，C言語と同様に単項接尾演算子である．排他的論理和はである．最下段の一つ前の行にある関数は，単項であり，メッセージチャンネルだけに適用される（メッセージチャネル参照）．gem（）は，チャンネルが保持するメッセージの数を返す．他のチャンネル演算・83・WorkshopReportⅥ）1．14，No．8

子は，既定義の意味があり半順序簡約をより有効に機能するために導入されている．半順序簡約を参照のこと．これらの関数を他と組み合わせ，新たな式として用いるべきではない．例えば，！e叩P旬（q）は構文誤りとなる．ne7叩fy（曾）を用いるべきである．

最終行の単項関数は特別なものである．最初の演算子は，プロセスのインスタンス化のために用いる（プロセスの項参照）．実行後，幾つかのインスタンスを生成する．2番目（emnについては，チャネル演算子の項で議論する．また，他の2つについては，neVer要求の項で説明する．

最初の4行は，C言語と同様に定義されている．即ち，ブーリアンのわbeは，0の値であり，その他は非ゼロとなり，truthを表す．

2．7．1条件式
List4（exprl−＞expr2‥

条件式

eXpr3）

e呼rlが0であれば上の式はe鱒r3の値をとり，そうでなければ，e巧r2の値をとる．−＞は必要であり，，；，で置き換えることはできない（文（statement）の項参照）

2・8

宣言（declaration）

プロセス，チャンネル，変数などは使用する前に宣言しなければならない．変数とチャネルはプロセス内部

で局所的に宣言することもできるし，大域的に宣言することもできる．プロセスは，prCC脚e宣言中でのみ大域的に宣言することができる．局所的な宣言はプロセスの本体中のどこにでも記述することができる．
2．8．1変数

変数宣言は，基本データ型であるは，あ00J，如e，β如け如意に引き続いて一つ以上の識別子が記述される．

初期子を続いて記述することもできる．
List5

変数宣言

byte namel，name2＝4，name3

初期子が記述されている場合，定数でなくてはならない．デフォルトでは，変数は0に初期化される．これ
らの基本データ型のビット幅は，それぞれ1，1，8，16，32である．最後の2つは符号付であるが，前の3つは，符号なしである．ユーザ定義型の変数も同様である（構造を参照のこと）．

2．8．2

配列

変数配列は例えば次のように宣言する．
List6

配列の宣言

int name【4】配列は，初期子として単一の定数を持つ．それにより全ての配列要素を初期化する．配列は，C言語と同様に0から始まる．従って，上記の場合の最大のインデックスは，3である．固定長のみ宣言できる．

●84＿

ⅥbrkshopReport

ⅥIl．14，No．8

2．8．3 シンボリック定数

シンボリック定数は，以下のように宣言できる．
List7

シンボリック定数の宣言

mtype＝tOK，READY，ACK）

一般に，メッセージタイプの定義に用いられる．そして，この型の変数は，次のように宣言できる．
Li5t8
mtype

シンボリック定数の宣言

St．atlユS＝OK；

mf汐eの定義は一つだけが許される．それは大域的であり，最大255個のシンボリック定数を持つことができる．
＃defineマクロに対するmtypeの優位性は，次の点である．SPLWは，シンボリック定数の型を理解し，シミュレーションの間，値ではなく，シンボル名を使用する．
2．8．4 メッセージチャンネル

メッセージチャンネルは例えば次のように宣言される．
LiSt9
Clmn Transfer

メッセージチャネルの宣言＝［2l of（mtype，bit，Short，Chan）；

Chan Device【3】＝【0】of tbyte）；

Chan Channel；

ここで，Ttansfbrはチャネルであり，最大2つのメッセージをチャネルに保存できる．メッセージの型は，中括弧内に示される．Deviceは，チャネルの配列であり，各チャネルは同期用になる．即ち，メッセージをチャ

ネルは保管できないので，送受信は同期しなくてはならない．最後のChannelは初期化されていないチャネ

ルであり，別の初期化済みチャネルを割り当てるという使い方のみである．

チャネルはメッセージの一部にもなり得るということに注意せよ．チャネル上での排他的受信（∬）や排他的送信（∬）は以下のように記述する．
ListlO

排他的なチャネルへのアクセス

Xr Transfer；

XS Channel；

動作している様々なプロセス中で，肝を宣言しているプロセスのみが，llans鎚rからメッセージを受け取ることができ，同様にxsを宣言しているプロセスのみが，Channelにメッセージを送信することができる．
もし，分析中に他のプロセスがltansferからメッセージを受け取ったり，Channelにメッセージを送信した場合は，実行中エラーである．詳細については，半順序簡約の項参照．
2．8．5

構造

typedef定義によって，ユーザ定義のデータ型を用いることができる．

ユーザ定義型は，変数宣言中でもちいることもできるし，型の定義が必要な場所で用いることができる：

WorkshopReportⅥ）1．14，No．8

Listllユーザ定義のデータ型

typeder Msg t
byte al3】，b；
CIlⅢ1p）List12

ユーザ定義型の利用

Msg roo；
Chan stream＝【0】of tmtype，Msg）

構造要素は，C言語と似た方法でアクセスできる．
List13構造要素へのアクセス

foo・a【112．8．61隠蔽変数
List14

隠蔽変数

hiddenint foo

隠蔽変数は，システム状態の一部ではない（実行をみよ），そして，借を割り当て可能であるが，その値は常に未定義でである．有効な変数の無効化が必要な時にこれは有益である．例えば，チャネルバッファの中の値を消し去り（且u血）たい時である．分析中に状態ベクトルのサイズを増加させないので，分析におけるメモリ

要求を下げる効果がある（メモリと時間要求を見よ）．
大域的な宣言のみが有効である．大域的であっても，構造要素は局所的とみなされる．古記，800g，C加nneJ変

数を隠蔽変数にすることはできない．
，＿，は事前定義された隠蔽変数であり，それは全ての文脈中で割り当て可能である．その（暗黙的な）型はinfであり，古記，あ00g，如e，mf肝e，βゐ0再，血の値を割り当て可能である．

2．9

プロセス

次の形式で基本的なプロセスの宣言をすることができる．
List15プロセスの宣言

proctype pname（chanIn，Ollt；byteid）（statements）

プロセスは，r触れ操作によって，インスタンス化できる．
List16プロセスのインスタンス化

run Pname（Transfer，Devicel0】，0）

最初に実引数を仮引数に割り当て，次にプロセスのボディ部を実行する．各プロセスインスタンスは，ユニークで，整数のインスタンス番号を持っている．これはm朋演算子（それとpid）によって生成されたも＿86．

ⅥbrkshopReport

Vol．14，No．8のである（特殊な変数を見よ）．インスタンス化されたプロセスは，プロセスのボディ部が終了するまで，活性状態にある．
プロセスは配列を引数の型としてとることはできない．しかし，構造（型）は許される．
プロセス宣言の最も一般的なフォームは以下のものである．
List17

一般的なプロセスの宣言

active【N］proctype pname（‥．）provided（E）priority M

αC如e修飾子は，システムの初期状態において，N個のproc脚eのインスタンスを活性状態にする．もし，【N】が記述されない場合，一つのインスタンスだけが活性状態になる．dC如e修飾子によって活性化されたイ
ンスタンスの引数は0に初期化される．即ち，実引数は，run一文によってのみ渡される．

実行可能条件を式Eに記述することができる．この式に記述できるのは，一般的な副作用なしの表現であり，定数／大域変数／事前定義された変数であるタイムアウト／pidを含むことができ，局所変数／引数／遠隔参照は記述できない．実行可能条件は初期状態において一度だけ評価される．
ランダム模擬の間（意味があるのは，この模擬のときのみである），プロセスインスタンスは優先度Mで実行される．優先度は，1以上の定数である．このプロセスを優先度1のものと比べ，M倍多くスケジューリングされることを意味する．実行優先度は，rum一文においても同様に用いることができる．
LiSt18

優先度付きのプロセスの実行

run pname（・・・）priority M

run文によってインスタンス化されたプロセスは，明示的にないしは暗示的に（デフォルトは1）示された優先度を常に持つ．

分析中では，優先度は意味がないことに注意せよ．
2．9．1決定的プロセス
List19

決定的プロセスの宣言

D＿PrOCtyPe Pname（chanIn，Out；byteid）（statements）

上記のpnameの全てのインスタンスは決定的である．それ以外の他の影響はない．もしインスタンスが実行中に決定的でないならば，検証時に誤りとなる．
決定性といのは，動的な性質であることに注意せよ．もし，pnameが次の文をそのボディ部に持つとする：
Li5t20チャネルへの讃き出しと読み出し

ir：：In？Ⅴ −＞：：011t！e −＞fi

このときにチャネルへの書き込みが同時である必要があるインスタンスが存在する場合，非決定的となる．
2．9．2 初期プロセス

・87．

WorkshopReport

Ⅵ止14，No．8

List21初期プロセス
init（Statements）

このプロセスは，一一度だけインスタンス化される．変数や適切なプロセスをインスタンス化することによって，システムの初期状態を生成するためにしばしば用いる．

2．9．3

never要求
LiSt22never要求

mever（statements）

これは，一度だけインスタンス化される特別なタイプのプロセスである．これについては，時間要求で述べる．never要求は，望ましくない或いは不正と考えられる振る舞いを検出するために用いる．

個々の文は，条件として解釈される（実行可能性，式を参照）．従って，副作用を持つべきではない（副作用については，構文誤りというより警告を出すことになる）．
副作用を持つ文には，割り当て，自動増加（alltO−increment）／自動減少（auto−decrement）演算，通信，実行，表明がある．
れeUer要求とともに関数ないしは変数を用いることができる．
・enα鋸ed（p摘）：pidによって示されるインスタンス番号を持っているプロセスが操作を実行可能であれ

ば，このブーリアン関数は，trueを返す．この関数は，同期型通信を持たないシステムでのみ用いることができる．
・pC＿〃αhe（pid）：この関数は，pidによって示されるインスタンス番号を持ったプロセスが実行中の状態の数を返す（−d実行時オプションによって状態数が与えられる）．
・＿叩：システム状態において，少なくとも一つの実行プロセスが，進行（progress）ラベルによって印付けられている制御フロー上にある時，hlseを返す．metJer要求と

2．9．4

mCe表明で用いられる．

trace表明
List23

traL：e表明

trace t statementsI

meVer要求と同様に，かⅥCe表明は新たな振る舞いを規定するわけではない．加α表明は，メッセージチャ

ネルの性質を表す．特に，プロセスがメッセージチャネルに働きかける操作列が妥当か否かについての形式的な文である．
2．9．5 特別な変数
List24

特別な変数

一，np＿，＿pid，−last●−は書き込みのみの変数で，メッセージフィールドのうち気にする必要のない場所を表すのに用いる．
・rp豆dは，事前定義された局所変数である．プロセスインスタンスのインスタンス番号を保持している．

・88・

WorkshopReport

Vol．14，No．8●＿払β舌は事前定義された大域変数である．現時点の実行列のなかで最後のステップを実行するプロセス
インスタンスのインスタンス番号を保持している．初期値は0である．meVer要求とfmce表明で用
いられる．

2且6

遠隔参照
LiSt25

遠隔参照

procnamelpidユ◎label

この式は，インスタンス番号pidを持つプロセスprocnameが，la，bel文の直前にいるときに，trueを返す．

2．10

文（statement）

文として次を使用することができる．
List26
a朋ert

aSSlgnment

declaratiom

goto

文を構成するもの

d＿8teprecelVe

repetition

atOmlC
elSe

Selection

send

break

eXpreSSion

timeout

Skip
unleSS式（expression）は文と同様に使用できるということにも注意せよ．

文はセミコロン（；）或いは，矢印（−＞）によって分離する．これらは同じ意味であるが，矢印は，後続の文との因果関係を示すのに時に用いられる．また，選択や繰返しにおいて，ガード条件とガードされる文を分離するのに用いられる．選択と繰返しを見よ．
構成要素として，文より小さなものはない場合，基本（basic）と呼ばれる．例えば，代入は基本文であるが，選択はそうではない．
2．10．1実行可能性
文の実行は，その実行可能性に依存している．文は，実行可能（enable）かブロックされている（blocked）
かの何れかである．先の文のリストのうち，代入文（BLSSignment），宣言文（declaration），表明文（a5Sert），ス

キップ（skip），gOtO文，break文は常に実行可能である．もし，ある文がブロックされたならば，実行可能になるまでその点で停止する．

2・10・2表明（asse托）

Lkt27

表明文

a朋ert（expression）

この式expresSionがfalse（ないしは0）を返す場合，プログラムをabortする．そうでない場合は，単に通過する．
2・10・3核化（atomic）

WorkshopReport

Ⅵ止14，No．8

List28核化文

atomic t statementS）

StatementSの個々の文においてそれぞれを実行しようと試みる．即ち，核化プロセスを実行中に分岐して他のプロセスを実行しないということである．核化文は，最初の文が実行可能であったときのみ実行可能になる．
局所的な計算を核的にすることは，検証システムの複雑性を減らすために重要である．核化文とd＿β甲を見よ．
実行中，明示的なタ0わや，核化のスコープ内で文がブロックされた点でのみ，そのスコープの外に制御が移る．このとき，もし，続きの文が再び実行可能になるならば，その点から，再度実行する．
スコープ内で何が起きるかについての制約はない．但し，ネスト化された核化やd＿虜甲は許可されない．

核化のスコープ内で，（ラベル化された）位置にジャンプすることは可能である．

run文によってインスタンス化されたプロセスインスタンスのボディ部は，（活動中の）核化文のスコープの外側にあると考える．

2．10．4break

繰返しを参照のこと．

2．10．5

goto

LiSt29

goto文

gotolabelgotoと同じ手続き中にあるラベルlabelに制御を移す文である．
2．10．6 決定的ステップ
List30

決定的ステップ

d−Step（statements）

これは，核化と同様な効果を持つが，別の効果も持つ（核化文とd＿β卸を見よ）．決定的ステップのスコー
プ中の文は完全に決定的である．しかし，d＿β亡甲のスコープ外のラベルに制御は移動しない．また，外部からスコープ内へのジャンプも存在しない．遠隔参照（remotereference）は許可されない．最初の文が実行可能な場合のみ，d＿β吟は実行可能である．d＿成甲は，d＿β物の直前はスコープ内とみなし，最終行の直後はスコープ外とみなす．従って，下記のコード（List．31）で1abelの効果を出そうとする場合：

List．32にあるコードに変更しなくてはならない．

2．10．7else

選択を参照のこと．

2．10．8式（expression）

自動増加／自動減少（＋＋／一一）を使用しないどんな式も文として使用可能である．この場合，もし評価結果が非ゼロ値ならば，厳密な意味で実行可能である．実行可能な式は，状態に変更を与えることなく実行さ．，0．

WorkshopReportⅥ）1．14，No．8

Li5t31効果のないラベル
gotolabel；label：

d−Step（do

break

List32効果のあるラベルgotolabel；label：Skip；

d−Step（do

break

Od；Skip）れる．
例えば，busywaitループを書く代わりに，次を使用することができる・
List33wbile（a！＝bllSyWaitループb）skip以下も同等である．
List34より簡単なblユSyWaitループの記述（a＝b）

2．10．9 チャネル操作

これらは（List．35），標準的なチャネルの操作である．

最初は，送信文である．二番目は受信文である．ここで，官はチャネルであり，Vdn，0m洩りα巧‥・は，チャネルのメッセージ型と合致しなくてはならない．送信，受信が可能となるためには，可は初期化されなけ
ればならない．更に，チャネルがバッファを持つならば，送信はバッファが一杯でないときのみ可能になる．
受信はバッファが空でないときのみ可能になる．バッファを持たないチャネルにおいて，送受信は，共に受送Ⅵbrb血opReport

Ⅵ止14，No．＄

List35q！varl，COnSt，Var2，…

チャネル操作或いはq？varl，COnSt，Var2，‥．或いはq！varl（const，Var2，…）
q？varl（const，Var2，．‥）

信が可能なとき（即ち同期している）時のみ可能である．受信文は，チャネルから最も古いメッセージを読む．送信文は，メッセージを（バッファを持っている限りにおいて）そこに置く．バッファを持たないチャネ
ルへの操作は，同期を取ってのみ実行可能である．
受信リスト中の定数は，実行可能性に制約を与える．すなわち，最も古いメッセージ中の対応する値が同じである場合に可能であり，そうでない場合はブロックされる．
同様の制約をチャネル操作の実行可能性に加えるために，局所ないしは大域変数を用いることもできる．
LiSt36

チャネルからの値の取得

q？varl，eVal（var2），Var3

2番目のメッセージがひα巧の値に等しくない場合，この受信はブロックされる．りα巧の億は変化しないことに注意せよ．

バッファリングされたチャンネルのための以下の操作がある．
・ボtV叫，CO乃紙UO巧】：受信操作が可能である時に，trueを返す（即ち非ゼロ値）．一問い合わせ●97＜udn，COI博士，化巧＞：メッセージがバッファから取り除かれないということを除けば，通常の受信操作と同様である．
●曾！！むαrl，COWf，VQr：ソート化送信：数字順，辞書順で直ちにメッセージを送信する．

・977肌町hα肌虎，…r：ランダム受信：同一のメッセージが存在したら，最も古いメッセージを受信する．
・97申叫，CO舶亡，Vd巧】‥先の問い合わせ操作と同様．

●曾？？くりαrl，CO那亡，Uα巧＞：メッセージがバッファから取り除かれないということを取り除けば，標準的なランダム受信と同様である．
バッファ付きチャネルは，Spinのコマンドラインスイッチ

一m

によって異なる振る舞いをする．スイッ

チが指定された場合，バッファが一杯であっても，送信アクションはブロックされない．その代わり，バッ
ファが一杯の状態で送信されたメッセージは失われる．

2．10．10

選択
List37

選択文

ir：：

StatementS：：

StatementS

fi

オプション（：：から始まる）の中の1つを選択して，実行する．もし，最初の文（ガード）が可能ならば，そのオプションが選択される．少なくとも，選択可能な分岐が一つもないとき，選択はブロックされる．一つ以上のオプションが選択可能ならば，ランダムにそのうちの一つが選択される．特別なカードであるebeが選

．92＿

﹁⁝︒

Ⅵ）1．14，No．8

WorkshopReport

択と繰返し文で一度だけ用いられる．もし，他のガードがブロックされている時のみ，実行可能となる・送信や受信文がガードとして用いられているときは利用されない・

2．10．11繰返し（repetition）

List38

繰返し文

do
：：

StatementS：：

StatementS

od

選択と同様であるが，gObや古代αたによって，制御が明示的に外側に移らない限り・繰り返して実行されるという点が異なる．古代α七は，実行中の最も内側の繰返し文を終了させる・繰返し以外では古代αたは用いられない．

2．10．12skip

影響を与えない．構文上の要求を満足するために主として用いられる・

2．10．13

timeout

舘me㈹f文は，システム中の全ての他の文がブロックされているときにのみ実行可能になる・実行されても，影響を与えない．

2．10．14

U山ess
List39tnnle岱文statements−1）unleSS（statements72）

staもements＿1の文を実行し，各文が実行終了する前に，StatementS−2の文の実行可能性が検査される・もし，実行可能であれば，StatementS−1はabortL，制御は，StatementS−2に移る・そうでなければ・StatementS−1に制御が残る．もし，StatementS−1が終了すれば，StatementS−2は無視される・

肌geββにおいて，αbm豆Cとは対照的にd＿β物は分割不能と考えられる・即ち・もしd一g坤のスコープ
中にstatements−1の制御があるならば，StatementS−2の実行可能性は，検査されない・

参考文献［1】Gerth，R．，ConcisePromelaReference，http：／／spinroot・COm／spin／Man／Quick・html，1997

Anmouncememt

Ⅵ）1．14，No．8

今後のSEAForumの予定
ここ何年かSEAForum開催の間隔がまちまちになっていましたが，先ごろの幹事会で話し合った結果，この春以降は少なくとも毎月1回は開催しようということに決まりました．主な会場としては，東京・東銀座のJJK会館（全国情報サービス産業厚生年金会館）を考えています．また，それぞれの地方支部の企画にもとづいて，大阪・名古屋・福岡その他の都市でも順次開催します．
とりあえず現在予定されている東京でのForumの一覧を以下にまとめておきます．

期日

テーマ

4月3日（月）ウオータフオール再考（再考？）−

5月17日（水）アスペクト指向は実用的か？

すでに案内済み

5月31日（水） システム危機と仕様検証（東証のトラブルは防げたか？）
6月16日（水）7月上旬

8月21日（月）オブジェクト指向の理想と現実
GPL Version

一

当日夜はSEA総会

3

要求工学（Ss2006での討論を受けて）これらのForumの記録（簡単なまとめと発表に用いられたスライドその他の資料）は，
順次SEAMAILに収録して会員に配布するつもりです（これでSEAMAILも船便状態から脱出できるか？：−）秋以降の東京Forumおよび地方開催Forumの企画は，これから幹事会で検討します．
会員各位からのご希望や提案をsea＠sea．or．jpまでお寄せください．

・，4．

AnnouncementⅥ）1．14，No．8

SS2006in熊本での新しい試み

すでにみなさんのお手元に届いたCallforPapersSEAForumでアナウンスされている

ように，今年のソフトウェア・シンポジウム（7／19−21）では，3日間の会期のうちの第2日目をいくつかのテーマによるワークショップ形式の討論にあてるという新しい試みを行

います．これまでのように講演や論文発表を聴くだけのシンポジウムではなく，参加者全員が討論に参加するという形のイベントにしようという狙いです．
4月17日に予定されている応募論文の審査が終わり，プログラムが決まったあと，参加者募集が始まりますが，参加申し込みにさいしては，希望するワークショップへのエントリーを，簡単なポジション・ステートメントつきで指定することが求められることにな
ると思います．

発表論文は応募しなかったがシンポジウムには参加したいと考えておられる方々は，どのテーマのワークショップに参加されるか，あらかじめ考えておいてください．

CallforPapersにリストアップされていたワークショップのテーマは次の通りでした：

A．プロセス，メトリクス，マネジメント

B．要求，テスティング，メインテナンス
C．仕様記述技法
D．教育
E．FLOSS，セキュリティ，ネットワーク

F．モデリング
G．組込み

この他に8番目のテーマとして「要求工学」も考えられており，このワークショップの討論結果は8月21日のForumで公開される予定です．

それぞれのワークショップの具体的な討論の企画は参加者募集のさいに明らかになります．期待してお待ちください．

MesSagefhImEditor

SeamailⅥ）1．14，No．8

編集後記

☆

昨年の2月に開催されたデザインワークショップの報告をお届けします．

☆☆
このレポートは，ワークショップの世話人だった野中さんから，去年の夏にはいただいてあって，
SS2005特集のVbl．14，N0．7のあとすぐに発行する予定だったのですが，IWFST2005その他の雑用に追われているうちに，いつのまにか冬も終わる季節になってしまいました．

☆☆☆
巻末（94ページ）の「今後のSEAForumの予定」に書いたように，これからは毎月定期的にForumを開催

し，その記録をSEAMAILに載せて行くということが先日の幹事会で決まったので，これからはいままでのような船便状態からは脱出できるのではないかと考えています（甘いか？）．

☆☆☆☆

．，6．

名

ソフトウ土7技術者協会〒160−0004東京都新層区四谷3−12丸正ビル5F
Tel：03−3356−1077

Fax：03−3356・1072

E−mail：Sea＠sea．or．JP

URL：http：／／www．sea．jp／