« 2016年4月 | トップページ | 2016年7月 »

2016年6月

2016年6月29日 (水)

SysML/UMLの状態図の制約や並行性の性質記述

要件仕様の内容,あるいはSysML/UMLの状態図に正確に制約や性質を記載することが大切であるが,SysML/UMLだけでは不可能であるし,また検証もレビューやテストで行うことは極めて非効率なので
Promelaでクラスの状態図の振る舞いを実装し,その後SpinにLTLを指定し,NeverClamを自動生成して用いるのが効率が良い。
 
公平性条件(無・弱・強)や並行性の条件(状態図のアクティビティへの割り込み,並行動作)など大抵のことは指定できる。
 
巷で良く見かけるSysML/UMLの状態図は公平性条件(無・弱・強)や並行性の条件(状態図のアクティビティへの割り込み,並行動作)などは無視あるいは考慮していないので,タスク間通信や排他制御の問題を表現できていないものが多い様だ。
 
今日はサンプル作りのために,良く例にある交差点の信号機の,NeverClamを自動生成し,promelaで書いた振る舞いに追加。その後C言語に変換し動作させる。

Spin

Spin2


|

2016年6月21日 (火)

Spinのツールを複数使い分け~xSpinとiSpin

線形時相の命題の充足や反例チェックのやり易さやGUIの使い勝手を考慮してxSpinとiSpinなど幾つかのSpinのツールを複数使い分けることにした。

Xspin


|

2016年6月17日 (金)

並行性を持つコンポーネントの安全な再利用

コンポーネントをブラックBOXとして扱い再利用や機能拡張を実現するにはコンポ―ネント間のインタフェースの事前条件と事後条件の推論規則は[satisfies]が、やや厳しい制約であるがやはり安全だろう。
 
これがクラスであれば、やはり[plug-in]が良く柔軟性も高い。
 
コンポ―エントが並列性を持つ ≪active≫コンポーネント なら、タスクやプロセスの線形時相理論的な不変条件の推論規則を追加した上で、推論規則で自動判定をツールで行う。
 
コンポーネントを分析・設計の狙い通りに開発・拡張するなら、メトリクスで[抽象度]と[不安定度]などの値を予め計画しておき,モデリングを作成中に自動計測してマッチングを判定する必要がある。

Compo1


|

プロセス代数による動的モデリングとispin

クラスやコンポーネントの拡張や再利用の数理論理的な「タイプ置換原理」による形式化と推論エンジンによるモデル(クラス,サブシステム,コンポーネント)の整合性&置換性の自動判定&コード生成のモデリングツールの開発はある程度はかたがついた。

モデル(クラス,サブシステム,コンポーネント)の整合性&拡張性や再利用性には、セマンティックな見地からのモデリングが不可欠だからDbCやリスコフ置換原理などを使うために数理論理による記述は不可欠。

それから、並行して作業していた状態図や並列処理などのプロセス代数による作業にしばらく集中する。こちらも線形時相理論による数理論理的なアプローチを取らないといけない。
最近はispinで作業がほとんどだけれど。

Hope1

Spin1

Spin2





|

2016年6月 1日 (水)

並列処理のモジュール技法とコンポーネント化および再利用のツールによる自動化

ここしばらく並列処理のアプリケーションモジュール技法とコンポーネント化および再利用を開発ツールで自動化するために検討をおこなってきた(大体目途が付く)
 
リアルタイム&組込みシステムでは、オブジェクト指向技法とパフォーマンスの点で対極にあるが避けては通れない
 
特に、信頼性とリアルタイム性が重要な要件(リアルタイム&組込みシステムではこれらは非機能要件では無い)なので
・例外と割り込みハンドラー
・RTOSを使うことを前提としてハードタイマー、ソフトタイマー
・ISRからの呼び出しのメカニズム
・各種I/Oからのイベントに対応するために処理分割とコンポ―ネントへの割り付けおよび優先度付与
・リアルタイムスケジューリング
・コンポーネント間の同期と通信
・オブジェクト指向としてのどのタイプの並列モデルのモデルを採用するか

以上は再利用があるリアルタイム・組込み・コンポーネントには特に重要な課題であり、再利用性のめにモデリング&設計で科学的に対応する必要がある
 
リアルタイム&組込みシステムに付いて回る
・優先度逆転
・デッドロック(シングル・インスタンス・デッドロック/マルチ・インスタン・スデッドロック)
を確実に避けることが重要で,RTOSの回避アルゴリズムは使わないようにしたい

並列処理と優先度逆転とデッドロックと言うとCSPを想起するが、CSPだけでも現場で実務を行う上で色々な利用上の制約がある

|

« 2016年4月 | トップページ | 2016年7月 »