• 検索結果がありません。

Seminar2 Aoki 20160123 最近の更新履歴 exektlab

N/A
N/A
Protected

Academic year: 2018

シェア "Seminar2 Aoki 20160123 最近の更新履歴 exektlab"

Copied!
19
0
0

読み込み中.... (全文を見る)

全文

(1)

形式手法

方定

青木利

(2)

本日

内容定

!

形式手法

!

検査を体感

(3)

信頼性定

!

社会

様々

場所

!

航空管制

電話

自動車

etc.

!

を含

!

社会

混乱

莫大

損害

人的損害を引

!

正しいソ

を作

!

現在

手法中心

開発

!

必要

!

形式手法

/

検証定

(4)

社会背景定

!

形式手法

/

検証

期待

!

信頼性

危機感

!

信頼性保証

増大

!

経済産業省

情報

信頼性向

!

国際標準

!

機能安全

: IEC61508, ISO26262

!

: ISO/IEC15408

!

後を絶

いソ

損失

(5)

形式手法

検証

特徴定

!

形式手法

検証

(Formal Methods/Verification)

!

/73.

4.年代

を中心

研究

実践

.定

! 

手法を指

く,色々

手法,技術,理論

.定

! 

形式手法

,検証

を,形式検証

場合

多い.定

!

数学や論理学

開発

検証を行う

! 

科学的

根拠

開発

検証

!

多く

整備さ

.定

!

難しそう

...定

!

/76.年代

多く

実践

報告さ

.定

!

比較的容易

使う

難しい

(6)

形式手法

ン定

!

対象を厳密

記述

.定

!

対象を解析

検証

!

何を解析

良い

&手法'?

! 

表明

成立

?競合状態

発生し

!

解析

! 

数学的

論理的問題を取

扱う理論

応用.定

仕様定

設計定

形式仕様記述言語8

VDM,Z,B

形式仕様記述言語 言語

(ex.SDL,Promela)

記述言語定

(7)

形式手法

ン定

数学的

論理的問題

扱い&解析

理論'定

検査

(Model Checking)

理証明

(Theorem Proving)

充足可能性解決

(SAT solving, SAT/SMT)

代数

(Process Algebra)

形式仕様記述言語

/

VDM/VDMTool,

Z/ZEVES,

B/Aterlier,

Event-B/RODIN,

CafeOBJ,

Alloy/Alloy Analyzer,

etc.

検査

Spin, NuSMV, LTSA,

UPPAAL, PAT, CBMC,

JPF, etc.

理証明

Coq, Isabelle/HOL,

HOL, ACL2, Vampire,

E, etc.

充足可能性問題解決器

:

MiniSAT, zChaff,

Yices, CVC3, Z3,

etc.

手法

(8)

代表的

適用事例定

! 

論文

!  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車載 ン 検証.

(9)

検査定

!

検査

(Model Checking)

!

1980

年代

発案.

!

効率的

全探索

!

多く

存在

!

いわ

ュボ

技術.

!

膳立

をし

を実行

,自

動的

結果

!

並行性

検証

得意.

(10)

検査定

!

擬似コ

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);

}

(11)

検査定

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)→

(12)

検査定

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)

(13)

検査定

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); }

}

(14)

検査概説定

! 

検査手法8考え

状態を

自動的

探索

!  有限状態 特徴 セ 並行動作 わ 性質 定

!  代表的 8NuSMV, Spin, LTSA, UPPAAL, etc.

! 

検査

UML

!  論理学 え 性質をp 対象 振 舞いをM M 対し p 成

立 を M p あ 呼 定

!  検査8振 舞い 記述し 性質 あ を検査 定

性質

記述定

相論理(CTL, LTL), 表明,

到 性& 検出 ', 進行性&飢餓状態検出 ', ...

舞い

記述定

状態遷移 , 並行 セ , ...

(req⇒◊ack),

¬(critical1∧ critical2), ...定

検査

自動 定

反例定

検出定

OK

相論理(Temporal Logic): 間 関 性質を取 扱う 論理

(15)

開発

!

形式手法

開発

! 

形式仕様記述8仕様策

工程

用い

! 

検査8設計工程や実装工程

用い

!

を形式手法

行う必要

無い.

! 

理論的

,望

しい

,コ

高い.

! 

品質

要.

!

使う

! 

形式仕様記述8

使う

向い

い.

! 

検査8

使う

向い

!

8電卓代わ

検査

! 

算,掛

算,割

算,複雑...

電卓.

(16)

開発

! 

手順書&

.定

!  既存 手順を破壊的 変更 い.定

!  形式手法をや い い , く い.定

!  実行 くし ,出荷 あ え い.定

!  ,既存 手順 適 埋 込 &補強' 要.定

!  を減 第一目標.定

! 

方法

考え

.定

!  ,軽い方法 試し 良い 思わ .定

!  し 提供さ い をas is 使う.定

現在

手順書定

電卓代わ 形式手法定

蓄積定 一般 手順 定

(17)

俊敏さ

形式手法定

!

開発

形式手法&特

手軽

手法'

相補的.

!

開発

を&そ

'制約

い.

!

仕様記述,

質を向

!

例え

!

! 

効果/'仕様

実装前

! 

効果0'

自動

品質保証.

!

検査を電卓代わ

使う

...

! 

仕様

設計を適

抽象度

記述し

動作さ

(18)

俊敏さ

形式手法定

!

形式手法

!

開発

初期段階&実装前'

を発見

!

品質保証

確認

を高く

!

俊敏さ

相性

良い&

?'.

!

やく動作を確認

! 

し,

!

を仕様&

! 

あわ

技.

!

検査

を電卓代わ

使う

!

大丈夫

,気

使う.

!

実際

使

実践例を聞く

使い方

多い.

(19)

! 

形式手法

整備さ

使いや

! 

様々

形式手法

様々

使い方.

! 

手軽

難しい

色々あ

! 

軽く使う

使い

色々考え

! 

使い

,大学

共同研究.

! 

手法

,使わ

いう考

え方

! 

を形式的

い.

! 

手軽

手法

開発

を制約し

い.

! 

,素早く使う,電卓的

使い方

! 

開発

使え

参照

関連したドキュメント

In this study, X-ray stress measurement of aluminum alloy A2017 using the Fourier analysis proposed by Miyazaki et al.. was carried

reduction.. Change in Vickers hardness as a function of annealing temperature for cold-rolled pure iron, Fe-0.3mass%Si alloy and Fe-0.3mass%Al alloy with 99.8%. reduction

[r]

日臨技認定センターの認定は 5 年毎に登録更新が必要で、更新手続きは有効期間の最終

新製品「G-SCAN Z」、 「G-SCAN Z Tab」を追加して新たにスタート 新製品「G-SCAN Z」、 「G-SCAN Z

We study the classical invariant theory of the B´ ezoutiant R(A, B) of a pair of binary forms A, B.. We also describe a ‘generic reduc- tion formula’ which recovers B from R(A, B)

タッチON/OFF判定 CinX Data Registerの更新 Result Data 1/2 Registerの更新 Error Status Registerの更新 Error Status Channel 1/2 Registerの更新 (X=0,1,…,15).

エリアP 雑固体廃棄物 焼却設備 処理設備     瓦礫保管エリア     伐採木保管エリア