Formal Engineering Methods for Software Development --An Introduction to SOFL--

Transcription

1 ソフトウェア開発の形式工学手法 --SOFL の紹介 -- 劉少英 (Shaoying Liu) URL:

2 講義の目標 システムエンジニアは持つべき最先端の技術を紹介する

3 本課程の内容 ソフトウェア開発の形式工学手法 (1) 形式工学手法の背景 (2) ソフトウェアの形式要求仕様と設計仕様記述技術 (3) 形式仕様に基づくプログラムテスト技術 現代社会のシステムエンジニアになるためには この授業の内容を良く勉強するのは間違いない

4 教科書 The textbook: Formal Engineering for Industrial Software Development Using the SOFL Method, by Shaoying Liu, Springer-Verlag, 2004, ISBN

5 成績の評価方法 1. 出席 : 20% 2. 期末試験 : 80% ( 何も参考できない ) クラスでの練習およびクラス後の宿題は 授業内容を理解するために全力でやって欲しい

6 1. 形式工学手法の紹介 ソフトウェア開発の問題点 問題点の解決における形式手法 形式手法への挑戦 改善策とした形式工学手法 SOFL: 具体的な形式工学手法

7 1.1 ソフトウェア開発の問題点 入力 プログラム (Java, C 等 ) 出力 コスト 時間 どのように開発するプログラムの信頼性を保証できるのか プログラムの信頼性は 何? 開発者

8 信頼的なシステムとは どういう意味? ソーセージ装置 input output 要求 : 小さい豚を入力すると ソーセージ装置は ソーセージを自動的に作る

9 信頼できないシステム : 牛肉 ソーセージ装置 input output 要求 : 小さい豚を入力すると ソーセージ装置は ソーセージを自動的に作る

10 ソフトウェア開発の抽象プロセス 機能仕様 プログラム S 作成する P 何をする 検証 どのようにする 仕様 S をどのように書くと その意味を明確に伝え 精確に理解することができるのか 仕様 S をどのように書くと プログラム P の検査 (inspection) 又はテストに役に立つのか 仕様 S をどのように書くと ソフトウェアツールにより S の分析 変換 検証などを効率に行うことができるのか

11 日本語で書いた仕様 : `` 各種の銀行口座に対し 次のサービスを提供する ATM ソフトウェアシステムを開発する 第一 current 口座および savings 口座に対して様々な操作を行う 第二 銀行口座の間の振り込み 第三 外国貨幣口座の管理 第四 各口座のパスワードの変更 また current 或いは savings 口座の操作は 預金 引き出し 残高の表示 手帳の印刷などを含む 問題点 : 構造 + 意味

12 より良い構造を持つ仕様 : 各種の銀行口座に対し 次のサービスを提供する ATM ソフトウェアシステムを開発する サービス : 1 current 口座の操作 2 savings 口座の操作 3 銀行口座の間の振り込み 4 外国貨幣口座の管理 5 各口座のパスワードの変更 Current または savings 口座のサービス : 1 預金 2 引き出し 3 残高の表示 4 手帳の印刷

13 非形式仕様の主な問題点 : 非形式仕様の表現は 曖昧性があり 誤解される可能性が高い ( 例えば 手紙 ) 非形式仕様の表現は プログラムの表現との間の差が大きいので プログラムの検証とテストには利用し難い ( 人間に任せるしかない ) 非形式仕様の整合性と正当性の分析は難しい 非形式仕様の分析 プログラムへの変換 発展など活動を支援するツールの構築は 難しい

14 2006 年 4 月 9 日の朝日新聞

15 ソフトウェアエラーを直すに必要なコストの状況 According to the paper ``What Is the Cost of a Requirement Error? By Tom King/Joe Marasco

16 可能な解決方法 形式手法!!! 形式手法は 今までソフトウェア開発手法のなかで 最も科学的な開発手法である

17 1.2 問題点の解決における形式手法 形式手法 (FM) とは 検証した設計手法である 形式手法 (Formal Methods) = 形式仕様記述技術 (Formal Specification) + 仕様を詳細化する技術 (Refinement) + 形式的検証 (Formal Verification) 集合論, 論理, 代数等.

18 形式手法を用いた現実なソフトウェア開発プロセス 要求分析 Validation 形式仕様の作成 Verification Verification 設計実装 テスト

19 重要な質問 : 形式仕様をどのように書けるか? 沢山の形式仕様記述言語と技術は開発された その中で代表的なものは VDM, Z, and B. である

20 よく使われた形式手法 (1) VDM (Vienna Development Method), IBM Research Laboratory in Vienna 参考書 : (1) Systematic Software Development Using VDM, by Cliff B. Jones, 2nd edition, Prentice Hall,1990. (2) Modelling Systems, by John Fitzgerald and Peter Gorm Larsen, Cambridge University Press,1998.

21 操作仕様 : 操作名 ( 入力変数の宣言 ) 出力変数の宣言 ext 状態変数 ( 外部変数とも言う ) pre 事前条件 post 事後条件 Example: Divide(x: int) result: real ext wr register: real pre x <> 0 post register = register~ / x and result = register

22 何故事前条件と事後条件が必要? 簡単な計算機を考えましょう register Divide Multiply Subtract Add

23 VDM 操作 (operation) 仕様と プログラムの関係 ( 同異点 ) 簡単な計算機を考えましょう 5 register register Divide Multiply Subtract Add

24 VDM 操作 (operation) 仕様と プログラムの関係 ( 同異点 ) 簡単な計算機を考えましょう register 1 register / Divide Multiply Subtract Add

25 VDM 操作 (operation) 仕様と プログラムの関係 ( 同異点 ) 次のプログラム ( クラスとメソッド ) を検討しましょう import ; class Calculator { int register := 0; int Add(int x) { register := register + x; return register; } double Divide(int x) { register := register / x; return register; } } main(string arg[]) { int input; double divisionresult; Calculator mycal := new Calculator(); read(input); //input に入力を読み込む divisionresult := mycal.divide(input); System.out.println( 除算の結果 : + divisionresult); } //main メソッドの終了

26 VDM 操作 (operation) 仕様と プログラムの関係 ( 同異点 ) 仕様は入力と出力の関係を重視するが プログラムは入力によってどのように出力を作るプロセスを重視する import ; class Calculator { int register := 0; double Divide(int x) pre x!= 0 { register := register / x; return register; } post register = register~ / x and result = register } main(string arg[]) { int input; double divisionresult; Calculator mycal := new Calculator(); read(input); //input に入力を読み込む divisionresult := mycal.divide(input); System.out.println( 除算の結果 : + divisionresult); } //main メソッドの終了

27 VDM 操作 (operation) 仕様と プログラムの関係 ( 同異点 ) 仕様は入力と出力の関係を重視するが プログラムは入力によってどのように出力を作るプロセスを重視する import ; class Calculator { int register := 0; double Divide(int x) pre x!= 0 { register := register / x; return register; } post register~ / x = register and register = result } main(string arg[]) { int input; double divisionresult; Calculator mycal := new Calculator(); read(input); //input に入力を読み込む divisionresult := mycal.divide(input); System.out.println( 除算の結果 : + divisionresult); } //main メソッドの終了

28 VDM 操作 (operation) 仕様と プログラムの関係 ( 同異点 ) プログラムを抜き出しても 仕様だけで操作の機能を定義できる import ; class Calculator { int register := 0; double Divide(int x) pre x!= 0 post register~ / x = register and register = result } main(string arg[]) { int input; double divisionresult; Calculator mycal := new Calculator(); read(input); //input に入力を読み込む if (input!= 0) { divisionresult := mycal.divide(input); System.out.println( 除算の結果 : + divisionresult);} else System.out.println( 入力された分母は 0 ですから 除算ができない ); } //main メソッドの終了

29 VDM 操作 (operation) 仕様とプログラムの関係 ( 同異点 ) 完全にVDM 仕様になる main(string arg[]) { int input; module Calculator Divide(x: int) result: real ext wr register: real pre x <> 0 post register = register~ / x and result = register double divisionresult; Calculator mycal := new Calculator(); read(input); //input に入力を読み込む if (input!= 0) { divisionresult := mycal.divide(input); System.out.println( 除算の結果 : + divisionresult);} else System.out.println( 入力された分母は 0 ですから 除算ができない ); } //main メソッドの終了

30 操作はモジュールにまとめる : module A 状態変数の宣言状態の不変数 操作仕様 1; 操作仕様 2; 操作仕様 n; end

31 (2) Z, PRG (Programming Research Group), Oxford 大学 UK 参考書 : (1) The Z Notation, by J.M. Spivey, Prentice Hall, (2) Using Z: Specification, Refinement, and Proof, by Jim Woodcock and Jim Davies, Prentice Hall, 1996.

32 (3) B-Method, Jean-Raymond Abrial, フランス 参考書 : (1) The B-Book: Assigning Programs to Meanings, by J-R Abrial, Cambridge University Press,1996, B 仕様は 幾つかの抽象マシンから構成された文書である 抽象マシンは 幾つかの操作を含むモジュールである 操作は 事前条件と事後条件で定義される

33 形式手法の応用情況 1. イギリスの Praxis 社は 形式手法 VDM,CSP,Z を用いて SSADM Toolset を開発した 2. イギリスの IBM Hursley は Oxford 大学と協力して Z を用いて Customer Information Control System (CICS) システムを開発した 3. カナダの Darlington Nuclear Generator System (Ontario Hydro) は Parnas の SCR (Software Cost Reduction) を用いて Shutdown System のソフトウェアを検証した 4.CSK の佐原グループは VDM を用いて 事務システムを開発した 5.FeliCa 社の栗田グループは 携帯電話組み込み用 モバイル FeliCa IC チップ 開発に VDM++ を利用した

34 政府又は標準機関の勧め 1.International Electrotechnical Commission (IEC) の European Standard IEC イギリスの Ministry of Defense のガイドライ ン MoD 経済産業省の情報システムの信頼性向上に 関するガイドライン

35 1.3 形式手法への挑戦問題 教育が足りない 形式手法の利用によって 伝統的なソフトウェア開発プロセスに変化が起こる 要求分析と設計段階にもっと時間がかかるが 実装とテストに時間が減らす その変化に対し 管理者が心配している

36 ソフトウェア企業の現状 幸せな世界 形式手法 開発者 ソフトウェア開発現場

37 1.4 改善策とした形式工学手法 形式工学手法 (Formal Engineering Methods) とは 形式手法を既存のソフトウェア開発技術に統合して得た実用性と厳密性と共に高い開発手法である その統合の目的としては 伝統的なソフトウェア開発プロセスの厳密性 文章の理解しやすさ およびツール支援能力を向上させることである

38 形式手法 形式工学手法 および伝統的なソフトウェア工学との関係 : 形式手法 伝統的なソフトウェア工学 ユーロッパ 形式工学手法 アメリカ アジア

39 形式手法と形式工学手法の違い 形式手法は 次の質問に答える ソフトウェア開発には 何をすべきか 何故? 形式工学手法は 次の質問に答える ソフトウェア開発には 何ができるのか どうやって?

40 1.5 SOFL: 具体的な形式工学手法 SOFL = Structured Object-Oriented Formal Language SOFL の研究開発は 1989 年イギリスの Manchester 大学から初め 1998 年で広島市立大学で基本完成 2000 年に法政大学で SOFL 形式工学手法を最終的に完成した

41 SOFL = 言語 + 手法 + プロセスモデル 言語としては SOFL がデータフロー図と形式仕様記述言語 VDM の結合を基盤として 構造化分析かつ設計を支えるだけでなく オブジェクト指向の設計と実装も表現できる その結合によって SOFL 仕様は 作成しやすく 理解しやすく そして保守しやすくなる 開発手法としては SOFL が形式仕様の作成によってシステムモデリングし 仕様に基づく厳密な検査 (inspection) とテスト技術でシステムの検証を行う また 構造化設計とオブジェクト指向の実装も支える 開発プロセスモデルとしては, SOFL が仕様の進化と詳細化技術と共に利用する また 設計仕様はまず完成し その後少しずつ増加する ( incremental) 形で実装を行うという方法を強調する

42 SOFL 仕様の一般構造 class S1; const; type; var; inv; method Init; module SYSTEM; const; type; var; inv; process Init; A1 A2 method P1; method P2; method P3; end_class; process A1; process A2; end_module; B2 B1 class S2; const; type; var; inv; method Init; method Q1; method Q2; method Q3; end_class; module A2_Decom; const; type; var; inv; process Init; process B1; process B2; process B3; end_module; B3 クラス仕様 モジュール仕様 条件データフロー図

43 部品 アーキテクチャ

44 練習 1 以下の質問に答えしなさい 1. ソフトウェア開発には 主な問題点が何ですか 2. 形式手法とは 何ですか 3. 形式工学手法とは 何ですか 4.SOFLとは 何ですか