技術セミナー・研修・出版・書籍・通信教育・eラーニング・講師派遣の テックセミナー ジェーピー
技術セミナー・研修・出版・書籍・通信教育・eラーニング・講師派遣の テックセミナー ジェーピー
大規模高度システムのための組み込みソフトウェア開発では、安全性と信頼性が大きな問題となっています。とりわけ、自動車、エレベータ、ロボット、鉄道、医療、宇宙機器などの産業機器、或いは民生機器では高信頼化が要求されています。組み込みシステムでの機能安全規格として、IEC61508、ISO26262 などの上位レベルでは形式手法(CCS,CSP,HOL,LOTOS,OBJ,VDM,Z, 時相論理, 他) を使う事を高く推奨(HR) されています。従って証明されたシステム設計方法は特別なものではなく、ヨーロッパでは当然のように実施されています。
自動車、列車の制御、通信、制御、ロボットなどの様に高機能で高性能な領域に入りますと、リアルタイム処理、高度で複雑な並行処理プログラミング技法が要求されます。一般に使われていますZ/B/Event-B/Alloy/ VDM などの形式手法ツールでは要求仕様の検証が主であり、リアルタイム処理、並行処理、通信、割り込み等の振る舞いの検証は十分でないだけでなくアーキテクチャーの検証は非常に難しいです。そこで注目されるのがCSP モデルです。
CSP は、元Oxford 大学のTony Hoare が1978 年 に考案し英国を中心に欧州で研究実用化が進められ、その結果としてInmos 社から並列処理言語occam と並列プロセッサTransputerが生み出されました。90 年代後半にTransputer が消えてからも、2000 年以降CSP モデルを採用したハードウェア、ソフトウェアは数多く見られる様になりました。この背景には、アプリケーションが複雑化するにつれて、CSP モデルの有効性が再注目されている様に思います。
CSP はプロセス代数の一つでありプロセスの振る舞いを数学的に記述できする事ができます。その後にモデル検証ツールを用いてモデルが正しいかどうかの検証をします。CSP モデルの検証ツールには、LTSA/SPIN/FDR2 /PAT3/Verum/Moby/ProB/CONPASU/CSP-Prover などがあります。特にPAT3 はReal-Time CSP などサポートされていますので、組み込み系のアプリケーションのモデル検証として使えます。
PAT3 には多くの機能が用意されていますが、とりわけCSP モデルが中心となってますので、ある程度 CSP の理解が必要とされます。従ってこのテキストでは、第1章でCSP プロセス概論、第2章でトレースとその意味、第3章で拒否、失敗、失敗発散、第4章でPAT3 の構文と使い方、第5章でCSP モデルのデザインパターンとPAT3 の基本的な使用方法、第6章でTimed-CSP 概要、第7章でTimed-CSP によるPAT3 の事例、第8章でUML 図へのPAT3 の事例、第9章でStateflow 図へのPAT3 の事例について説明します。
テキストの構成は、英国Surrey 大学のSteve Schneider 教授のテキスト「Concurrent and Real-timeSystems – The CSP Approach」を主として使い、CSP のデザインパターンを用意し、それらをPAT3 のコードに書き直す事から入ります。
このデザインパターンはプログラミングの構造と同じなのでoccam-π/JCSP/XC などのプログラミング技法へと展開する事ができます。基礎的なデザインパターンの構造が理解できますと、更に複雑なプロセスモデルを考える事ができます。この操作はLEGO マシンの仕組みと同じです。プロセスの遷移法則と代数的法則はプログラム言語の意味を理解するのに役立ちますので添付いたしました。
CSP コンストラクタの法則性に関してTony Hoare、Bill Roscoe、Steve Schneiderのテキストには書かれていますが、もう少し基本的で有益な内容がTony Hoare、Jim Woodcock、Xinbei Tangらの資料の中にありますので、その中から抽出し追加致しました。
| 開始日時 | 会場 | 開催方法 | |
|---|---|---|---|
| 2024/5/15 | ソフトウェア開発への生成AI・ChatGPT導入と活用 | オンライン | |
| 2024/5/21 | 永久磁石同期モータの制御系設計の基礎 | オンライン | |
| 2024/6/18 | Pythonではじめる機械学習入門講座 | オンライン |
| 発行年月 | |
|---|---|
| 2003/12/10 | 入門 MATLAB/SimuLinkによる制御系設計手法 |
| 2003/5/22 | ソフトウェア品質保証の考え方と技術の実際 |
| 2002/10/25 | Windowsプログラミングのソフトウェア解析とデバッグ手法 |
| 1993/10/29 | FPGA設計技術の基礎と応用 |
| 1987/11/1 | デジタルシグナルプロセッサの基礎と応用 |