ソフトウェア開発の形式学的手法 - CIS授業wiki

ソフトウェア開発の形式工学手法･･･3年/CS,DM/選択

lecture01 - 08/04/14

ソフトウェア開発の形式工学手法

第一回　2008/04/14

形式工学手法とは何か？を学ぶ

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

＜システムとは？＞
相互関係を持ついくつかの部品から
構成された一定の機能を提供するものである。

システム
⇒ハードウェア、ソフトウェア、ハードウェア＋ソフトウェア

システムの事例･･･人工衛星の発射、新幹線の運行、銀行システム

＜システムエンジニアとは？＞
システムを開発する人である。
ソフトウェア、またはソフトウェアとハードウェアの開発

＜システムの開発は？＞
システムの構築に関する
理論、方法論、言語、ツールなどの技術を応用しながら
開発するプロセスである。

【ソフトウェア開発はシステム開発の焦点である】

• ソフトウェアはハードウェアよりシステム制御、

　情報処理能力が高い、また更新の作業がより簡単。
しかし

• ソフトウェア間の依存関係が複雑(誤差を許さない)
• 開発、管理、保守が難しく、コストも高い。
• 開発を厳密に行えないため正確性を保証できない。

◎本講義で学ぶ内容
1)形式工学手法の背景
2)ソフトウェア形式要求仕様と形式仕様記述技術
3)形式仕様にもとづくプログラムテスト技術

◎成績の評価
出席20％、期末試験80％(参照不可)

１．形式工学手法の紹介

• ソフトウェア開発の問題点
• 問題点の解決における形式手法
• 形式手法への挑戦
• 改善策とした形式工学手法
• SOFLとはなにか？具体的な形式工学手法

1.1 ソフトウェア開発の問題点

ソフトウェア開発の主な仕事
理解⇒創造⇒検証
★失敗の70％は「理解」の部分にある
「創造」に必要なのは"プログラム設計"

【ソフトウェア開発の抽象プロセス】
何をする(S･機能仕様)→→→どのようにする(P･プログラム)
その後、検証しなければならない
Sをどのように書くと

• その意味を明確に伝え正確に理解することができるか
• Pの検査、またはテストに役に立つのか
• ツールによりSの分析、変換、検証などを効率的に行えるか

仕様Sは自然言語で書くと･･･問題アリ

• 親しみがあるがはっきりわからない⇒個人の常識に頼ってしまう

《構造＋意味》が問題!!!
⇒構造の部分は改善可能･･･箇条書きにする、など

【非形式仕様の問題点】

• 曖昧性がある
• プログラムの表現との差が大きく、プログラムの検証とテストに利用しにくい
• 整合性と正当性の分析が難しい
• 分析、変換、発展などを支援するツールがつくりにくい

そこで！
★【形式手法(Formal Methods)】を使う！

• 検証した設計手法

形式仕様記述技術(Formal Specification)
　　　　　＋
仕様を詳細化する技術(Refinement)
　　　　　＋
形式的検証(Formal Verification)

離散数学(集合、論理等)を使う。

lecture02 - 08/04/21

2008/04/21　形式手法(Formal Method)

【形式手法によるソフトウェア開発プロセス】
要求分析⇒形式手法⇒設計⇒実装⇒テスト
テスト以外は１つ前のフェーズに戻れる(検証)
テストで全てのフェーズのフィードバック？

形式仕様をどのようにかけるのか？
⇒代表的なのは VDM、Z、and　B

【形式手法に使われる言語】

〔VDM(Vienna Development Method)〕

操作仕様：
　操作名(入力変数の宣言)出力変数の宣言
　ext状態変数(外部変数とも言う)
　pre事前条件　←入力変数と状態変数が満たさなければならない条件
　post事後条件　←出力変数はかならず事後条件を満たす

例）
　Divide(x:int) result: real
　ext wr register: real
　pre x<>0（xは0ではない）
　post register = register～/x　←代入演算子ではない、比較のみ
　　　　and
　　　　result = register

〔Z〕や〔B〕もある。
Bはいくつかの抽象マシンから構成された文書

【形式手法の応用状況】

• FeliCa社の栗田グループは携帯電話用のICチップ開発にVDM++を利用
• CSKの佐原グループはVDMを用いて事務システムを開発
• イギリスIBMのhurslayはOxford大学と協力しCICSシステムを開発

【形式手法への挑戦】

• 教育が足りない。
• 形式手法の利用によって、伝統的なソフトウェア開発プロセスに変化が起こる。要求分析と設計段階にもっと時間がかかるが、実装とテストにかかる時間が減る。その変化を管理者が懸念。
• 大規模ソフトウェアの形式仕様は複雑で理解しにくく、変更に時間がかかる。
• 形式検証手法の制限があるため、検証を有効に行うのが難しい。
• 支援ツールが少ない。

【改善策とした形式工学手法】
形式手法を既存のソフトウェア開発に統合して得た開発手法である。
＜目的＞伝統的なソフトウェア開発プロセスの厳密性、文章の理解しやすさ、およびツール支援能力を向上させる。

形式手法⇒形式工学手法(橋のような役割)⇒ソフトウェア開発の形式手法の応用

【形式手法と形式工学手法の違い】
形式手法･･･ソフトウェア開発には「何をすべきか、なぜ？」
形式工学手法･･･ソフトウェア開発には「何ができるのか、どうやって？」

【SOFL：具体的な形式工学手法】
SOFL=Structured Object-Oriented Formal Language
2000年に大学でSOFL形式工学手法が完成
SOFL=言語+手法+プロセスモデル
<言語>データフロー図とVDMの結合を基板としている。
<手法>SOFLで形式仕様の作成をしシステムモデリングし、仕様に基づく厳密な検査とテスト技術でシステム検証を行う。構造化設計とオブジェクト指向の実装も支える。
<開発プロセスモデル>SOFLが仕様の進化と詳細化技術とともに利用する。設計仕様をまず完成させておいて、少しずつ実装する形をとる。

条件データフロー図⇒モジュール仕様⇒クラス仕様　の構造

lecture03 - 08/04/28

2008/04/28 第３講
The Basic Components of the SOFL Specification Language

【SOFL論理】
SOFL論理･･･命題論理と述語論理の拡張で、「未定義」という特別な値
を表すことが出来る論理

【命題(proposition)】
真または偽と判断できる事柄
真理値＝truth value
boolean型はboolと書く。
分解できない命題は「原子命題」という。

～ここからスリーピング（笑）～

【論理演算の優先順位】
あいまい性の解消のためにつけられる。

これ以降、2年後期「人工知能(講義)」を参照?

【正規形】
和正規形･･･論理積から構成された論理和
積正規形･･･論理和から構成された論理積
(1年前期「論理回路」参照？)

【述語論理】
命題論理では一部または全てのオブジェクトについての性質を表現できない。

• 私のクラスの1人が受賞した。
• 私のクラスには数学が嫌いな人がいる。

★述語Pは、trueまたはfalseを得る特別な関数である。
P:X->bool

x>10･･･述語であるが命題ではない。
5>10･･･命題である(真偽が判断可)が、述語でもある。
→命題は特別な述語

is_big(x:int):bool
==x>10

この述語から命題が形成
is_big(2008) true
is_big(5) false
is_big(1992) true

lecture04 - 08/05/13

lecture05 - 08/05/13

担当：mica@管理人
Last Update: 2008年04月28日13時16分57秒

---

コメントどうぞ♪

---