管理メニュー
  • atwiki
  • Model Base
  • 「状態遷移システムの構成概念を理解する」のPFD

Model Base

「状態遷移システムの構成概念を理解する」のPFD

最終更新：

modelbase

- view
管理者のみ編集可

更新日2013-01-31
[ 形式手法の独学 ] / [ 「形式手法の独学」のPFD ]

「状態遷移システムの構成概念を理解する」のPFD

各プロセスの説明

P101_FSMの数学モデルを学ぶ

  • 【なぜやるか】
    • 考察対象のシステムを有限状態機械(FSM Finite State Machine)として形式化したいため。
    • ステートマシン図が表す設計情報を数訳するため(やや言い過ぎかも)。
  • 【どのようにやるか】
    • FSMを構成する情報の要素を把握する
    • 構成要素の表現記号は参照情報によって異なることもあるが気にしない。
    • UMLのステートマシン図を構成する図式要素とFSMを構成する情報要素との間に、どのように対応があるのか考察してみる。

P102_状態遷移に関わる用語の意味を考える

  • 【なぜやるか】
    • システムの"遷移"を適切に規定できるようになるため
  • 【どのようにやるか】
    • 事前条件、事後条件、不変条件、ガード条件などの用語は、FSMの数学モデルでは何を意味するのか研究してみる。
    • 条件は部分集合として考える。

P103_UMLでの"状態"という用語の運用について考える

  • 【なぜやるか】
    • FSMの数学モデルとUMLステートマシン図の図式の対応関係を把握するため。
  • 【どのようにやるか】
    • UMLステートマシン図のコンポジット状態をFSMの数学モデルではどのような解釈を与えるべきか考察してみる。

P104_状態遷移の合成ついて考える

  • 【なぜやるか】
    • FSMの数学モデルとUMLステートマシン図の図式の対応関係を把握するため。
  • 【どのようにやるか】
    • 積オートマトン(product automaton)の定義を把握する。
    • 積オートマトンの定義とUMLステートマシン図の直交状態の図式の関連を考察する。
    • 単純な二つのサンプルFSMからその積オートマトンの作り、直交状態の記法で表してみる。

P105_状態遷移時のアクションについて考える

  • 【なぜやるか】
    • ステートマシン図の図式制約を理解するため。
    • アクションと状態のかかわりを理解するため。
  • 【どのようにやるか】
    • run to completion step というUMLの用語を調べる。
    • FSMの数学モデルの見地から"アクション"をどういう解釈にするか考察してみる。

P106_ProtocolStateMachine図とBehavioralStateMachine図の作図目的の違いを考える

  • 【なぜやるか】
    • 目的に応じて図式が違うことを意識するため。
  • 【どのようにやるか】
    • BehavioralStateMachineとProtocolStateMachineの構文の違いを調べる。
    • 事前条件とガード条件の違いを考える。

P107_ステートマシンの作図を練習する

  • 【なぜやるか】
    • ステートマシン図自体は目新しくない図式であり、今まで鵜呑みにしていた何かがあるはずなので、それを取り除くため。
    • 実際に手を動かすことで図式の意味を実感し知識を定着させるため。
  • 【どのようにやるか】
    • システム動作概要を描く程度のラフスケッチではなく、設計情報の形式的な図式として詳細にステートマシン図を書いてみる。
    • 状態変数を常に意識して対象システムの状態空間を明確にする。
    • 図式内の事前条件やガード条件を示す論理式は適当な述語で代替表記するが、別途それらの述語を状態変数を項に取る論理式で定義する。
    • サーバー／クライアントの通信プロトコルをProtocolStateMachineで表現してみる。

各成果物の説明

I101_FSMの数学モデルの定義

  • 【教本】
    オートマトンの教本ならどれでも数学モデルの定義が載っている。定義を知るだけが目的ならネット検索でも何とかなるかもしれないが、オートマトンの基礎を学んでいるほうが学習の糧になるので教本を紹介する。

I102_UMLのチュートリアル

I103_状態ベース仕様に関する参考書

  • 【教本】
    形式手法で標準的な考え方ある、事前条件、事後条件、不変条件といった用語の意味を読者が理解している前提で、教本が書かれることが一般的で、用語を丹念に解説している教本を自分は知らない。参考にならないかもしれないが、手元にある本から参考箇所を探してみた。

D101_FSMの数学モデルの理解

  • 【何を得るか、どんな状況になるか】
    • FSMの数学モデルで記された情報を状態遷移図で表すことができる。
    • 決定性有限オートマトンの遷移関数を他の人に説明できる。

D102_遷移_事前条件_事後条件_不変条件_ガード条件の理解

  • 【何を得るか、どんな状況になるか】
    • 事前条件をFSMの数学モデルで説明できる。
    • 事後条件をFSMの数学モデルで説明できる。
    • 不変条件をFSMの数学モデルで説明できる。
    • ガード条件をFSMの数学モデルで説明できる。
    • 決定性有限オートマトンと非決定性有限オートマトンの遷移関数の違いが説明できる。
    • "デッドロック"とはFSMのどのような性質を指す用語なのかを説明できる。

D103_UMLステートマシン図_コンポジット状態の意味の理解

  • 【何を得るか、どんな状況になるか】
    • FSMの数学モデルでいう"状態"は集合の要素を指し、 UMLのステートマシン図でいう"状態"はFSMの数学モデルの状態の集合を指していることを理解する。

D104_UMLステートマシン図_直交状態の意味の理解

  • 【何を得るか、どんな状況になるか】
    • 直交状態の各リージョンの積オートマトンが直交状態の振る舞いであることを理解する。
    • 設計者が意味付けできるのは、システムの振る舞いを直交する射影軸で分解(自分は因数分解と呼んでいる)した様子であることを理解する。
    • システムの振る舞いの因数分解は困難な作業であり、システムを検証するためには予め因数(直交状態の各リージョン)が定義してあることが重要だと理解する。

D105_run_to_completionの理解

  • 【何を得るか、どんな状況になるか】
    • UMLのステートマシンのアクション実行中のイベント処理に関する方針を、run to completion という用語を手がかりに理解できている。
    • 関数呼び出しをイベント入力と見なしてコンポーネントの振る舞いをステートマシン図で定義したとき、そのコンポーネントのアクション中に実行する他コンポーネントの関数呼び出しが同コンテキストの中で自身の関数の再入呼び出しとなる場合、そういった状況をどのように取り扱うべきかについて自分なりの見解を持つ。

D106_ProtocolStateMachineによる仕様記述の理解

  • 【何を得るか、どんな状況になるか】
    • 作図するステートマシン図がBehavioralStateMachineなのかProtocolStateMachineなのか、両者のどちらであるべきか目的意識を持てている。
    • 事前条件とガード条件の運用について自分なりの見解を得ている。
    • ライブラリモジュールのProtocolStateMacineを作図するために、そのAPI仕様にどのような情報を記すべきか、自分なりの見解を得ている。
「「状態遷移システムの構成概念を理解する」のPFD」をウィキ内検索
記事メニュー
人気記事ランキング
  1. 抽象によるソフトウェア設計／付録 A 練習問題 解答例
  2. Alloy Analyzer
  3. A.4.1 状態機械の定義
  4. A.3.1 驚くような三段論法
もっと見る
最近更新されたページ
もっと見る
目安箱バナー