形式手法
役
立
方定
青木利
本日
内容定
!
形式手法
紹
!
検査を体感
ソ
信頼性定
!
社会
様々
場所
ソ
組
込
い
定
!
ン
ン
航空管制
携
電話
自動車
etc.
!
誤
を含
少
く
い
定
!
社会
混乱
莫大
損害
人的損害を引
起
定
!
正しいソ
を作
要
定
定
!
現在
手法中心
開発
定
!
そ
誤
取
除
い
必要
定
!
形式手法
/
検証定
社会背景定
!
形式手法
/
検証
期待
!
信頼性
関
危機感
!
信頼性保証
コ
増大
!
経済産業省
情報
信頼性向
関
ン
!
国際標準
.
!
機能安全
: IEC61508, ISO26262
!
セ
ュ
: ISO/IEC15408
!
後を絶
いソ
損失
形式手法
検証
特徴定
!
形式手法
検証
(Formal Methods/Verification)
!
/73.
4.年代
を中心
研究
実践
行
わ
い
.定
!
特
手法を指
く,色々
手法,技術,理論
含
う
.定
!
形式手法
う
,検証
特
し
を,形式検証
呼
場合
多い.定
!
数学や論理学
基
い
開発
検証を行う
定
!
科学的
根拠
基
い
開発
検証
定
!
多く
整備さ
あ
.定
!
難しそう
聞
え
...定
!
/76.年代
多く
実践
報告さ
い
.定
!
比較的容易
使う
難しい
存
形式手法
ン定
!
対象を厳密
記述
.定
!
対象を解析
検証
.
!
何を解析
良い
&手法'?
!
表明
成立
?競合状態
発生し
い
?
!
う
解析
?
!
数学的
論理的問題を取
扱う理論
応用.定
仕様定
設計定
定
形式仕様記述言語8
VDM,Z,B
形式仕様記述言語 言語
(ex.SDL,Promela)
記述言語定
形式手法
ン定
数学的
論理的問題
取
扱い&解析
理論'定
検査
(Model Checking)
理証明
(Theorem Proving)
充足可能性解決
(SAT solving, SAT/SMT)
セ
代数
(Process Algebra)
形式仕様記述言語
/
8
VDM/VDMTool,
Z/ZEVES,
B/Aterlier,
Event-B/RODIN,
CafeOBJ,
Alloy/Alloy Analyzer,
etc.
検査
8
Spin, NuSMV, LTSA,
UPPAAL, PAT, CBMC,
JPF, etc.
理証明
8
Coq, Isabelle/HOL,
HOL, ACL2, Vampire,
E, etc.
充足可能性問題解決器
:
MiniSAT, zChaff,
Yices, CVC3, Z3,
etc.
手法
定
代表的
適用事例定
!
サ
論文
! Edmund M.Clarke and Jeannette M.Wing8Formal Methods: State of the Art
and Future Directions, ACM Computing Surveys, 1996.
! 回路設計 コ 標準 航空宇 企業 ン
相当数
! Jim WOODCOCK, et.al: Formal Methods: Practice and Experience, ACM
Computing Survey, 2009.
! 最近 要 事例
!
報告書
! IPA/SEC:厳密 仕様記述 形式手法成 事例調査報告書
! IPA/SEC: 形式手法適用調査報告書
!
代表的
適用事例
!
CICS, TCAS, ISDN,
鉄
,防潮可動橋,航空管制,
,
etc.
!
共同研究&論文
発表し
い
'.
! ンソ , サ 8車載 ン 検証.
検査定
!
検査
(Model Checking)
!
1980
年代
発案.
!
効率的
全探索
.
!
多く
存在
.
!
いわ
ュボ
ン
技術.
!
膳立
をし
,
を実行
,自
動的
結果
返
く
.
!
並行性
検証
得意.
検査定
!
擬似コ
定
void processA(){
while(1){
lock(mutex1);
lock(mutex2);
/* Critical Section */
unlock(mutex1);
unlock(mutex2);
}
}
void processB(){
while(1){
lock(mutex2);
lock(mutex1);
/* Critical Section */
unlock(mutex2);
unlock(mutex1);
}
検査定
void processA(){ while(1){
lock(mutex1); lock(mutex2);
/* Critical Section */ unlock(mutex1); unlock(mutex2); }
}
void processB(){ while(1){
lock(mutex2); lock(mutex1);
/* Critical Section */ unlock(mutex2); unlock(mutex1); }
}
数え 定
A: lock(mutex1)→A:lock(mutex2)→
A:unlock(mutex1)→A:unlock(mutex2)
B: lock(mutex2)→B:lock(mutex1)→
B:unlock(mutex2)→B:unlock(mutex1)
A: lock(mutex1)→B:lock(mutex2)→
検査定
void processA(){ while(1){
lock(mutex1); lock(mutex2);
/* Critical Section */ unlock(mutex1); unlock(mutex2); } } void processB(){ while(1){ lock(mutex1); lock(mutex2);
/* Critical Section */ unlock(mutex1); unlock(mutex2); }
}
数え 定
A: lock(mutex1)→A:lock(mutex2)→
A:unlock(mutex1)→A:unlock(mutex2)
B: lock(mutex1)→B:lock(mutex2)→
B:unlock(mutex1)→B:unlock(mutex2)
A: lock(mutex1)→A:lock(mutex2)→
A:unlock(mutex1)→B:lock(mutex1)→
A:unlock(mutex2)→B:lock(mutex2)
B: lock(mutex1)→B:lock(mutex2)→
B:unlock(mutex1)→A:lock(mutex1)→
検査定
void processA(){ while(1){
lock(mutex1); lock(mutex2);
/* Critical Section */ unlock(mutex1); unlock(mutex2); } } void processB(){ while(1){ lock(mutex2); lock(mutex3);
/* Critical Section */ unlock(mutex2); unlock(mutex3); } } void processC(){ while(1){] lock(mutex3); lock(mutex4);
/* Critical Section */ unlock(mutex3); unlock(mutex4); } } void processD(){ while(1){ lock(mutex4); lock(mutex5);
/* Critical Section */ unlock(mutex4); unlock(mutex5); } } void processE(){ while(1){] lock(mutex5); lock(mutex6);
/* Critical Section */ unlock(mutex5); unlock(mutex6); } } void processF(){ while(1){ lock(mutex6); lock(mutex1);
/* Critical Section */ unlock(mutex6); unlock(mutex1); }
}
検査概説定
!
検査手法8考え
状態を
自動的
探索
定
! 有限状態 特徴 セ 並行動作 わ 性質 定
! 代表的 8NuSMV, Spin, LTSA, UPPAAL, etc.
!
検査
≠
UML
定
! 論理学 え 性質をp 対象 振 舞いをM M 対し p 成
立 を M p あ 呼 定
! 検査8振 舞い 記述し 性質 あ を検査 定
性質
記述定
相論理(CTL, LTL), 表明,
到 性& 検出 ', 進行性&飢餓状態検出 ', ...
振
舞い
記述定
状態遷移 , 並行 セ , ...
(req⇒◊ack),
¬(critical1∧ critical2), ...定
検査
定
自動 定
反例定
検出定
OK
相論理(Temporal Logic): 間 関 性質を取 扱う 論理
開発
セ
定
!
形式手法
開発
セ
置
.
!
形式仕様記述8仕様策
工程
用い
.
!
検査8設計工程や実装工程
用い
.
!
を形式手法
行う必要
無い.
!
理論的
,望
しい
,コ
高い.
!
品質
コ
ン
要.
!
う
使う
?
!
形式仕様記述8
使う
向い
い
い.
!
検査8
使う
向い
い
.
!
8電卓代わ
検査
.
!
算,掛
算,割
算,複雑...
→
電卓.
開発
セ
定
!
手順書&
セ
'
埋
込
.定
! 既存 手順を破壊的 変更 い.定
! 形式手法をや い い , く い.定
! 実行 くし ,出荷 あ え い.定
! ,既存 手順 適 埋 込 &補強' 要.定
! を減 第一目標.定
!
埋
込
方
い
い
方法
考え
.定
! ,軽い方法 試し 良い 思わ .定
! し 提供さ い をas is 使う.定
現在
手順書定
電卓代わ 形式手法定
蓄積定 一般 手順 定
俊敏さ
形式手法定
!
開発
セ
形式手法&特
,
手軽
手法'
,
相補的.
!
開発
セ
を&そ
ほ
'制約
い.
!
仕様記述,
ュ
,
質を向
さ
.
!
例え
,
.
!
!
効果/'仕様
明
点
実装前
明
.
!効果0'
自動
品質保証.
!
検査を電卓代わ
使う
...
!
仕様
設計を適
抽象度
記述し
動作さ
.
俊敏さ
形式手法定
!
形式手法
.
!
開発
初期段階&実装前'
誤
を発見
.
!
品質保証
確認
質
を高く
.
!
俊敏さ
相性
良い&
い
?'.
!
やく動作を確認
.
!
し,
ン
.
!
を仕様&
'
.
!
あわ
技.
!
検査
を電卓代わ
使う
勧
.
!
大丈夫
う
,気
使う.
!
実際
使
い
実践例を聞く
,
使い方
多い.
わ
定
!
形式手法
,
や
ュ
ン
整備さ
使いや
く
.
!
様々
形式手法
様々
使い方.
!
手軽
難しい
色々あ
.
!
軽く使う
,
使い
色々考え
.
!
使い
あ
,大学
共同研究.
!
,
手法
あ
,使わ
い
損
,
いう考
え方
勧
.
!
を形式的
!
,
わ
い.
!
手軽
手法
開発
セ
を制約し
い.
!
追
的
,素早く使う,電卓的
使い方
.
!