背景 並行システム : 協調する複数の処理 ( プロセス ) から構成されるシステム 並行システムの例 ( 昇降舵のフライバイワイヤ ) 操縦桿 x2 角度 x3x2 ジャイロ x3 重量計 x4 フラップ LVDT IRU WOW FSACE PB 優先ボタン x2 MON モニタ COM コマン

Size: px
Start display at page:

Download "背景 並行システム : 協調する複数の処理 ( プロセス ) から構成されるシステム 並行システムの例 ( 昇降舵のフライバイワイヤ ) 操縦桿 x2 角度 x3x2 ジャイロ x3 重量計 x4 フラップ LVDT IRU WOW FSACE PB 優先ボタン x2 MON モニタ COM コマン"

Transcription

1 並行システム解析支援ツール ~ 協調動作の可視化 ~ 磯部祥尚 * 1, 大岩寛 * 1, 高橋孝一 * 1, 田中純 * 2 産業技術総合研究所 * 1 セキュアシステム研究部門, * 2 イノベーション推進本部 第 10 回クリティカルソフトウェアワークショップ 10 th WOCS 年 9 月 28 日 この資料の一部またはすべての内容について 作成者の許可なき使用 複製 配布を固くお断りします 1

2 背景 並行システム : 協調する複数の処理 ( プロセス ) から構成されるシステム 並行システムの例 ( 昇降舵のフライバイワイヤ ) 操縦桿 x2 角度 x3x2 ジャイロ x3 重量計 x4 フラップ LVDT IRU WOW FSACE PB 優先ボタン x2 MON モニタ COM コマンド 協調 フライト制御 x4 アクチュエータ x4 ACE, PCU センサプロセッサアクチュエータ ( エンブラエル社レガシー ) なぜ並行システム? センサに対する応答性 故障時に対する冗長性 制御情報の通信 ( 共有 ) 背景 : ネットワークやマルチコアの普及によって 並行処理が身近になっている 課題 : 全体で正しく並行処理するように 個々のプロセスを設計するのは難しい 2

3 目標 目標 : 設計モデルの協調動作を理論的に解析するツール CONPASU の開発 効果 : 信頼性の向上 手戻りコストの削減 解析結果 設計レビュー支援 解析 フィードバック 並行システムのモデル 要求分析 設計 手戻りコスト削減 受入テスト 結合テスト CONPASU-tool SQ REM SUM 実装 単体テスト 3

4 発表概要 はじめに ( 済 ) 背景 目標 CONPASUツールの特徴 並行システムの解析例 協調動作の可視化 モデル検査との違い CONPASUの適用 既存ツールとの連携 CSPモデルベース設計工程 CONPASUの機能 記号処理 状態数削減 おわりに まとめ 今後の課題 pp.5-11 pp pp

5 CONPASU ツールの特徴 並行システムの解析例 協調動作の可視化 モデル検査との違い 5

6 並行システムの解析例 並行システム全体の動作を把握するのは難しいので? upload cancel complete UI input ok ng quit0 succ Sender start net term quit1 ack Receiver output 構造 UI Sender 振舞い Receiver 通信 通信 6

7 並行システムの解析例 並行システム全体の動作の可視化するツール CONPASU [1] を開発中! CONPASU-tool upload cancel complete 入力 : 並行システムの構造 各プロセスの振舞い UI UI input ok ng quit0 succ Sender Sender start net term quit1 Receiver τ[#ds0>0] /ds0:=tail(ds0), ack Receiver output 構造 振舞い 出力 : 全体の振舞い 処理 : 並行合成 状態数削減 CONPASU( 産総研知財管理番号 :H24PRO-1409) 並行システム通信全体の振舞い 通信デッドロック 7

8 協調動作の可視化 既存のツール ( 例 :PAT [10], LTSA [11] ) でも状態遷移図を表示できる 入力値は具体化されるため状態数が多くなる CONPASU パイプライン並列計算の例 in.1 in.0 PAT in?x1 SQ REM SUM LTSA 状態数 : 8 遷移数 : 12 状態数 : 105 遷移数 : 160 入力値 : 無制限入力回数 : 任意 状態数 : 42 遷移数 : 67 入力値 :{0,1} 入力回数 :3 8

9 状態遷移図の抽象化 CONPASU では興味のあるイベントに着目した状態数の削減が可能 状態数 : 3 遷移数 : 3 CONPASU CONPASU-tool 途中結果の表示を隠蔽 状態数 : 8 遷移数 : 12 in?x1 [n>0] / y:=y+(x1 * ((11)1) SQ REM SUM ( 計算式が見える!) 9

10 計算過程の可視化 CONPASU では任意の入力値に対する計算過程 ( 計算式 ) を確認できる in?x1 状態数 : 3 遷移数 : 3 状態数 : 105 遷移数 : 160 in.1 in.0 比較 in.1 式 CONAPSU 入力値 : 無制限入力回数 : 任意 入力値 :{0,1} 入力回数 :3 prts.2 10 PAT 値

11 モデル検査との違い CONPASU では検証用の性質 ( 時相論理式など ) を記述する必要がない 性質 ( 逐次動作 ) は CONPASU が抽出する 両ツールを併用すると効果的 in の後にいつか ack が起きる? この性質を記述 in ack 並行システムの設計モデル Snd c1 Rcv out Ack c2 性質 ( 時相論理 ) (in ack) 逐次動作 in in in in c1 c2 ack c1 out ack ack ack c2 in と ack の関係は? in と ack を選択 11

12 CONPASU の適用 既存ツールとの連携 CSP モデルベース設計工程 12

13 既存のモデル / ツールとの連携 CONPASU は形式手法 CSP* 1[2,3] に基づく解析ツール CONPASU の入力言語には形式言語 CSP M * 2 を採用 ( 例 : モデル検査器 FDR と連携して UML モデルを解析可能 ) FDR モデル検査器 [8] ( オクスフォード大学 ) UML Activity UML State M. 変換器 UML CSP M ( サリー大学 [7] ) 変換器 SimuLink CSP M 状態遷移図 意味論 Snd = in -> c1 -> Snd Rcs = c1 -> out -> c2 -> Rcv Ack = Sys = ((Snd Ack) [ ]Rcv) \{ } ProB モデル検査器 [9] デュッセルドルフ大学 サウサンプトン大学 MATLAB/Simulink ペルナンブコ連邦大学 エンブラエル社 [6] CSP M 言語 CONPASU * 1 CSP : 並行システムを記述し 解析するための理論 ( プロセス代数 ) * 2 CSP M : CSP の代表的なモデル検査器 FDR の入力言語 ( 関連研究が多い ) モデル解析器 [1] ( 産総研 ) 13

14 形式手法 CSP CSP モデルはメッセージパッシング通信を採用 協調部 ( 並行処理 ) とデータ部を分割して設計しやすい プロセス チャネル in?x f x, y, z = x + y z C UI in x CNTL out y back?z out!y y:=f(x,y,z) データ部 ( 関数 ) z 協調部 ( 構造 ) back 協調部 ( 振舞い ) 設計手順 役割分担の明確化 比較 : 共有メモリではプロセス間の結合強度が高い ( 分割しにくい ) x:=f(y,z) y:=g(x,z) x z y 共有メモリ z:=h(x,y) 14

15 CSP モデルベースの設計工程 CSP では協調部 ( 並行処理 ) とデータ部を分割して設計 解析しやすい 概念モデル 間違えやすい協調部は網羅的解析 (CONPASU に実装中 ) 設計工程 網羅的解析 解析工程 協調部 データ部 構造図 ( コンポーネント図 ) 振舞い図 ( ステートマシン図 ) 協調部 データ部 ( 関数定義等 ) int fact(n){... } 解析済の CSP モデル シミュレーション 状態数の多いデータ部はシミュレーション解析 (CONAPSU に実装予定 ) 15

16 CONPASU の機能 記号処理 状態数削減 16

17 CONPASU の機能 CONPASU は並行処理の全体像を解析して可視化するツール 逐次化機能 : 並行処理を記号的意味論によって逐次処理に展開する機能 状態数削減機能 : 振舞いの等しさを保ったまま状態数を減らす機能 状態数 : 8 状態数削減 (CONPASU) CONPASU 並行システムの設計モデル 状態数 : 4 in c1 c2 out B0 B1 B2 in c1 c1 c2 c2 out 逐次化 (CONPASU) 容量 3 のバッファ 17

18 記号的意味論 プロセス代数の記号的意味論 [4,5] は 1995 年頃から研究が行われている CSP モデル Proc = in?x out!(x 2) ack Proc ( 普通の ) 意味論記号的意味論 入力値 x {0,, 9} 値 変数 in.0 in.1 in.2 in.9 out.0 out.2 out.4 out.19 ack in?x out!(x 2) ack 状態数の増加を抑えられる 解析 ( 等価性判定など ) は難しい 18

19 状態数削減 状態遷移図 ( 変数含 ) の振舞いを変えずに状態数を削減する方法を考案 振舞いを変えないように内部動作をバイパスする ( 注 : 振舞いに影響する すなわちバイパスできない内部動作もある ) 振舞いの等しさにはCSPの失敗等価性 = F を採用 観測されない内部動作 / n:=1,m:=0 τ/ m:=m+2 S1(n, m) S2(n, m) print!n bak/n:=n+1 print!n bak/n:=n+1 τ/ m:=m+2 S3(n, m) S4(n, m) print!m STOP 状態数削減 = F / n:=1, m:=0+2 S2(n, m) print!n bak/n:=n+1 print!m S4(n, m) STOP 並行処理では このような順番が可換な振舞いはよく現れる ( インターリービング ) 19

20 並行システムの解析例 並行システム全体の動作の可視化するツール CONPASU を開発中! upload cancel 普通の意味論で状態遷移図 UI を作成した場合 complete (FDR 使用 ) 状態数 : 約 12 万 CONPASU-tool UI データ種類 :4 種類入力 : 転送回数 :4 回 並行システムの構造 各プロセスの振舞い input ok ng quit0 succ Sender Sender start net term 状態数 Receiver : 8 quit1 ack Receiver output 構造 振舞い 出力 : 全体の振舞い 処理 : 並行合成 状態数削減 通信 通信 20

21 おわりに まとめ 今後の課題 21

22 まとめ CONPASU 研究のポイント ネットワークやマルチコアの普及によって 並行処理が身近になっている 複雑な並行処理の全体像を解析して 簡潔に可視化するツールを開発 UMLなどの並行処理も解析可能で 既存の開発工程への導入が容易 信頼性の向上 手戻りコストの削減 UML モデルベース開発工程への導入 CSP モデルベース開発工程の採用 解析 UML 要求分析 設計 UML 手戻りコスト削減 受入テスト 結合テスト 解析 CSP/UML 要求分析 設計 CSP/UML 解析 CSP (CONPASU) 実装 単体テスト (CONPASU) 並行処理の明確化 検証効率の向上 実装 22

23 今後の課題 解析結果のフィードバック方法 見やすい解析結果の表示方法 解析結果ともとのモデルとの対応表示方法 他 設計モデル 解析結果 解析 フィードバック モデルの表現力の拡張 実数など CSP M では未対応のデータ型も扱えるようにする 23

24 参考文献 1. (CONPASU)Y. Isobe, CONPASU-tool: A Concurrent Process Analysis Support Tool based on Symbolic Computation, CPA2011, WoTUG-33, IOS Press, pp , (CSP)C. A. R. Hoare, Communicating Sequential Processes, Prentice Hall, (CSP)A. W. Roscoe, The Theory and Practice of Concurrency, Prentice Hall, ( 記号的意味論 )Z. Li and H. Chen, Computing strong/weak bisimulation equivalences and observation congruence for value-passing processes, TACAS '99, LNCS 1579, Springer, pages , ( 記号的意味論 )M. Hennessy and H. Lin, Symbolic bisimulations, Theoretical Computer Science, Volume 138, Issue 2, pp , (Simulink-CSP)J. Jesus, A. Mota, A. Sampaio, and L. Grijo, Architectural Verification of Control Systems Using CSP, ICFEM 2011, LNCS 6991, Springer, pp , (UML-CSP)I. Abdelhalim, S. Schneider, and H. Treharnea, Towards a Practical Approach to Check UML/fUML Models Consistency Using CSP, ICFEM 2011, LNCS 6991, Springer, pp.33-48, (FDR)Formal Systems (Europe) Limited, Failures-divergence refinement: FDR2, 9. (ProB)Universität Düsseldorf and University of Southampton, The ProB Animator and Model Checker National University of Singapore, PAT: Process analysis toolkit Imperial College London, LTSA - labelled transition system analyser. 24

形式手法に基づく CONPASU 並行処理可視化ツールの紹介 ~CSP モデルベース開発のすすめ ~ 磯部祥尚 * 1, 大岩寛 * 1, 高橋孝一 * 1, 田中純 * 2 産業技術総合研究所 * 1 セキュアシステム研究部門, * 2 イノベーション推進本部 ET2012 展示会場内 IPA 出

形式手法に基づく CONPASU 並行処理可視化ツールの紹介 ~CSP モデルベース開発のすすめ ~ 磯部祥尚 * 1, 大岩寛 * 1, 高橋孝一 * 1, 田中純 * 2 産業技術総合研究所 * 1 セキュアシステム研究部門, * 2 イノベーション推進本部 ET2012 展示会場内 IPA 出 形式手法に基づく CONPASU 並行処理可視化ツールの紹介 ~CSP モデルベース開発のすすめ ~ 磯部祥尚 * 1, 大岩寛 * 1, 高橋孝一 * 1, 田中純 * 2 産業技術総合研究所 * 1 セキュアシステム研究部門, * 2 イノベーション推進本部 ET2012 展示会場内 IPA 出展ブースプレゼンテーション 2012 年 11 月 15 日 この資料の一部またはすべての内容について

More information

TopSE並行システム はじめに

TopSE並行システム はじめに はじめに 平成 23 年 9 月 1 日 トップエスイープロジェクト 磯部祥尚 ( 産業技術総合研究所 ) 2 本講座の背景と目標 背景 : マルチコア CPU やクラウドコンピューティング等 並列 / 分散処理環境が身近なものになっている 複数のプロセス ( プログラム ) を同時に実行可能 通信等により複数のプロセスが協調可能 並行システムの構築 並行システム 通信 Proc2 プロセス ( プログラム

More information

CSPの紹介

CSPの紹介 CSP モデルの優位性 産業技術総合研究所情報技術研究部門磯部祥尚 0:40 第 9 回 CSP 研究会 (2012 年 3 月 17 日 ) 1 講演内容 1. CSPモデルの特徴 CSPモデルとは? 同期型メッセージパッシング通信 イベント駆動 通信相手 ( チャネル ) の自動選択 3. CSPモデルの検証 CSPモデルの記述例 検証ツール 振舞いの等しさ 2. CSPモデルの実装 ライブラリ

More information

CONPASU-tool

CONPASU-tool CONPASU-tool (CONcurrent Process Analysis SUpport tool): 記号処理に基づく並行プロセス解析支援ツールの試作 情報技術研究部門 ミドルウェア基礎研究グループ 磯部祥尚 0:50 FOSE2010 2010/11/19 1 発表内容 背景と動機 並行プロセス設計の難しさ 本研究の目的 プロセス代数記術 CONAPSU の機能 既存ツールとの違い 解析ツール

More information

Vol. 32 No. 1 Feb Processes) [6] [13] CSP CSP [7] CSP CSP PAT [14] FDR2 [4] [7] SD2CSP SD2CSP SDVerifier SDVerifier SD2CSP : 3. 1 : create (

Vol. 32 No. 1 Feb Processes) [6] [13] CSP CSP [7] CSP CSP PAT [14] FDR2 [4] [7] SD2CSP SD2CSP SDVerifier SDVerifier SD2CSP : 3. 1 : create ( 234 SDVerifier: CSP SDVerifier SDVerifier CSP SDVerifier Sequence diagrams are often used in the modular design of softwares. However, it is difficult to verify UML diagrams automatically. In this work,

More information

7 ソフトウェア工学 Software Engineering モデル検査 MODEL CHECKING 1 モデル検査の概要 並行システム : 相互排他, デッドロック, スタベーションなどの現象 入出力関係に着目した 停止性 + 部分正当性 のみでは正当性を言えない 振る舞い ( 途中の状態遷移

7 ソフトウェア工学 Software Engineering モデル検査 MODEL CHECKING 1 モデル検査の概要 並行システム : 相互排他, デッドロック, スタベーションなどの現象 入出力関係に着目した 停止性 + 部分正当性 のみでは正当性を言えない 振る舞い ( 途中の状態遷移 7 ソフトウェア工学 Software Engineering モデル検査 MODEL CHECKING 1 モデル検査の概要 並行システム : 相互排他, デッドロック, スタベーションなどの現象 入出力関係に着目した 停止性 + 部分正当性 のみでは正当性を言えない 振る舞い ( 途中の状態遷移 ) の考慮の必要性 behaviors モデル検査 : 有限状態遷移系の振る舞いの検証を自動で行う技術

More information

CSP研究会 プロセス代数の基本と関連ツールの紹介

CSP研究会 プロセス代数の基本と関連ツールの紹介 プロセス代数の基本と関連ツールの紹介 産業技術総合研究所情報技術研究部門磯部祥尚 第 5 回 CSP 研究会資料 2010.07.10 1 講演内容 1. プロセス代数 プロセス代数とは? プロセス代数による記述例 プロセス代数による解析例 解析ツールの紹介 2. 等価性 強双模倣等価弱双模倣等価分岐双模倣等価失敗発散等価 3. 例題 :AB プロトコル ABプロトコルの概要各プロセスの動作 4.

More information

Microsoft PowerPoint - 【最終提出版】 MATLAB_EXPO2014講演資料_ルネサス菅原.pptx

Microsoft PowerPoint - 【最終提出版】 MATLAB_EXPO2014講演資料_ルネサス菅原.pptx MATLAB/Simulink を使用したモータ制御アプリのモデルベース開発事例 ルネサスエレクトロニクス株式会社 第二ソリューション事業本部産業第一事業部家電ソリューション部 Rev. 1.00 2014 Renesas Electronics Corporation. All rights reserved. IAAS-AA-14-0202-1 目次 1. はじめに 1.1 モデルベース開発とは?

More information

はじめに : ご提案のポイント

はじめに : ご提案のポイント 8. モデリングプロセスの構成と手順 モデル検査を用いた設計モデリングのプロセスを分類し それぞれのプロセスの流れと手順を示す 本章の概要は以下の通りである 対象読者目的想定知識得られる知見等 (1) 開発技術者 (2) 開発プロジェクト管理者モデル検査における設計モデリングにおいて 最初に利用できる情報に応じて モデリングプロセスが分類されることを示し その中で典型的なアーキテクチャ情報に基づくモデリングプロセスについて具体的に示す

More information

Microsoft PowerPoint - Wmodel( ) - 配布用.pptx

Microsoft PowerPoint - Wmodel( ) - 配布用.pptx SEA SPIN Meeting May 2012 配布用 W モデル 2012/06/08 1 2 はじめに 3 目次 4 メモ 5 W モデルって 何ですか? 6 現在の状況 7 現在の状況 8 現在の状況 9 W モデルの定義 10 Andreas Spillner の W モデル Requirements Executing Accept. Tests Specification Executing

More information

目次 ペトリネットの概要 適用事例

目次 ペトリネットの概要 適用事例 ペトリネットを利用した状態遷移テスト 和田浩一 東京エレクトロン SDC FA グループ 目次 ペトリネットの概要 適用事例 ペトリネットの概要 - ペトリネットとは ペトリネット (Petri Net) とは カール アダム ペトリが 1962 年に発表した離散分散システムを数学的に表現する手法である 視覚的で 数学的な離散事象システムをモデル化するツールの一つである ペトリネットの概要 - ペトリネットの表記と挙動

More information

Microsoft PowerPoint - sakurada3.pptx

Microsoft PowerPoint - sakurada3.pptx チュートリアル :ProVerif による結合可能安全性の形式検証 櫻田英樹日本電信電話株式会社 NTT コミュニケーション科学基礎研究所 アウトライン 前半 :ProVerif の紹介 後半 :ProVerifを用いた結合可能安全性証明 [Dahl Damgård, EuroCrypt2014, eprint2013/296] の記号検証パート 2 ProVerif フランス国立情報学自動制御研究所

More information

PowerPoint プレゼンテーション

PowerPoint プレゼンテーション GSN を応用したナレッジマネジメントシステムの提案 2017 年 10 月 27 日 D-Case 研究会 国立研究開発法人宇宙航空研究開発機構 研究開発部門第三研究ユニット 梅田浩貴 2017/3/27 C Copyright 2017 JAXA All rights reserved 1 目次 1 課題説明 SECI モデル 2 GSN を応用したナレッジマネジメントシステム概要 3 ツリー型チェックリスト分析

More information

CANapeを用いたラピッドコントロールプロトタイピングのバイパス手法による制御モデル開発

CANapeを用いたラピッドコントロールプロトタイピングのバイパス手法による制御モデル開発 ape を用いたラピッドコントロールプロトタイピングのバイパス手法による制御モデル開発 近年 自動車のソフトウェア開発において 開発期間の短縮やコスト削減の面からモデルベース開発が注目されています アイシン エィ ダブリュ株式会社は ラピッドコントロールプロトタイピングのバイパス手法による制御モデル開発にベクターの測定 / キャリブレーションツール ape ( キャナピー ) を導入しました 本稿では

More information

IPSJ SIG Technical Report Vol.2015-SE-189 No /7/23 iarch-u 1,a) 1,b) 1,c) 1,d) Archface-U iarch-u Partial Model !" %&)*+,-./ :;<

IPSJ SIG Technical Report Vol.2015-SE-189 No /7/23 iarch-u 1,a) 1,b) 1,c) 1,d) Archface-U iarch-u Partial Model ! %&)*+,-./ :;< iarch-u 1,a) 1,b) 1,c) 1,d) Archface-U iarch-u Partial Model 1. 123+!" %&)*+,-./0 46789 :; ( 1) Archface-U [7] Archface-U Archface-U iarch-u 2 Archface-U 3 1 Kyushu University a) fukamachi@posl.ait.kyushu-u.ac.jp

More information

2013 年年度度ソフトウェア 工学分野の先導的研究 支援事業 抽象化に基づいた UML 設計の検証 支援ツールの開発 公 立立 大学法 人岡 山県 立立 大学情報 工学部情報システム 工学科 横川智教 Circuit Design Engineering Lab. - Okayama Prefec

2013 年年度度ソフトウェア 工学分野の先導的研究 支援事業 抽象化に基づいた UML 設計の検証 支援ツールの開発 公 立立 大学法 人岡 山県 立立 大学情報 工学部情報システム 工学科 横川智教 Circuit Design Engineering Lab. - Okayama Prefec 2013 年年度度ソフトウェア 工学分野の先導的研究 支援事業 抽象化に基づいた UML 設計の検証 支援ツールの開発 公 立立 大学法 人岡 山県 立立 大学情報 工学部情報システム 工学科 横川智教 背景 - 組込みソフトウェア開発の課題 組込みソフトウェアの開発プロセス 要求分析 設計 実装 テスト 手戻り 下流流 工程での不不具合の検出 上流流 工程への 手戻りの発 生 手戻りによる開発コスト増

More information

040402.ユニットテスト

040402.ユニットテスト 2. ユニットテスト ユニットテスト ( 単体テスト ) ユニットテストとはユニットテストはプログラムの最小単位であるモジュールの品質をテストすることであり その目的は結合テスト前にモジュール内のエラーを発見することである テストは機能テストと構造テストの2つの観点から行う モジュールはプログラムを構成する要素であるから 単体では動作しない ドライバとスタブというテスト支援ツールを使用してテストを行う

More information

個人依存開発から組織的開発への移行事例 ~ 要求モデル定義と開発プロセスの形式化 による高生産性 / 高信頼性化 ~ 三菱電機メカトロニクスソフトウエア ( 株 ) 和歌山支所岩橋正実 1

個人依存開発から組織的開発への移行事例 ~ 要求モデル定義と開発プロセスの形式化 による高生産性 / 高信頼性化 ~ 三菱電機メカトロニクスソフトウエア ( 株 ) 和歌山支所岩橋正実  1 個人依存開発から組織的開発への移行事例 ~ 要求モデル定義と開発プロセスの形式化 による高生産性 / 高信頼性化 ~ 三菱電機メカトロニクスソフトウエア ( 株 ) 和歌山支所岩橋正実 iwahashi@est.hi-ho.ne.jp Iwahashi.Masami@wak.msw.co.jp 1 改善効果 品質 : フロントローディングが進み流出不具合 0 継続生産性 : 平均 130% 改善 工数割合分析

More information

f2-system-requirement-system-composer-mw

f2-system-requirement-system-composer-mw Simulink Requirements と新製品 System Composer によるシステムズエンジニアリング MathWorks Japan アプリケーションエンジニアリング部大越亮二 2015 The MathWorks, Inc. 1 エンジニアリングの活動 要求レベル システムレベル 要求分析 システム記述 表現 高 システム分析 システム結合 抽象度 サブシステム コンポーネントレベル

More information

オートマトン 形式言語及び演習 3. 正規表現 酒井正彦 正規表現とは 正規表現 ( 正則表現, Regular Expression) オートマトン : 言語を定義する機械正規表現 : 言語

オートマトン 形式言語及び演習 3. 正規表現 酒井正彦   正規表現とは 正規表現 ( 正則表現, Regular Expression) オートマトン : 言語を定義する機械正規表現 : 言語 オートマトン 形式言語及び演習 3. 酒井正彦 www.trs.css.i.nagoya-u.ac.jp/~sakai/lecture/automata/ とは ( 正則表現, Regular Expression) オートマトン : 言語を定義する機械 : 言語を記号列で定義 - 記述しやすい ( ユーザフレンドリ ) 例 :01 + 10 - UNIX の grep コマンド - UNIX の

More information

2 1,384,000 2,000,000 1,296,211 1,793,925 38,000 54,500 27,804 43,187 41,000 60,000 31,776 49,017 8,781 18,663 25,000 35,300 3 4 5 6 1,296,211 1,793,925 27,804 43,187 1,275,648 1,753,306 29,387 43,025

More information

ホンダにおける RT ミドルウェア開発と標準化活動 株式会社本田技術研究所基礎技術研究センター関谷眞

ホンダにおける RT ミドルウェア開発と標準化活動 株式会社本田技術研究所基礎技術研究センター関谷眞 ホンダにおける RT ミドルウェア開発と標準化活動 株式会社本田技術研究所基礎技術研究センター関谷眞 目次 知能ロボットシステム概要 コンポーネント指向ミドルウェア HRTMの開発 ASIMOへの適用 HRTMとOpenRTM-aistの連携動作 標準化活動 知能ロボットシステム概要 センサーやアクチュエーターは追加や変更される システム構成は変更したくない センサー, アクチュエーターの関係を抽象化した

More information

<4D F736F F F696E74202D D4C82F08A B582BD A A F2E707074>

<4D F736F F F696E74202D D4C82F08A B582BD A A F2E707074> SysML を活用したシステムエンジニアリング オージス総研組み込みソリューション部 1 アジェンダ 概要編なぜシステムエンジニアリングかシステムエンジニアリングとはシステムエンジニアリングとモデリング言語 SysML の特徴実践編機能要求を検討する要求を仕様化する振る舞いを検討する構造を検討する論理ブロックを物理ブロックに割り当てる性能を検討するまとめ 2 概要編 : なぜシステムエンジニアリングか

More information

2008年度 設計手法標準化アンケート 集計結果

2008年度 設計手法標準化アンケート 集計結果 2011 年度 設計手法普及調査アンケート 集計経過報告 2012 年 2 月社団法人組込みシステム技術協会状態遷移設計研究会 目次 1. アンケート実施の目的 3 2. アンケートの実施対象 4 3. アンケート回答数 5 4. 実施したアンケートの内容 6 5. アンケート回答者の構成 8 6. アンケート集計結果 9 6.1 回答者の担当製品分野について 10 6.2 回答者の部門について 11

More information

Microsoft PowerPoint - B3-3_差替版.ppt [互換モード]

Microsoft PowerPoint - B3-3_差替版.ppt [互換モード] SQiP2011 B3-3 状態遷移および機能連携に着 した業務シナリオテストの新 法 2011 年 9 9 株式会社 NTT データ技術開発本部プロアクティブ テスティング COE 岩 真治 所属 紹介 株式会社 NTT データ 主な業務 技術開発本部プロアクティブ テスティング COE 昨年 12/1 に設 先進的な検証 テストサービスの提供とそれを実現するための研究開発に取り組む専 組織 社内のソフトウェア開発標準プロセス

More information

講義の進め方 第 1 回イントロダクション ( 第 1 章 ) 第 2 ~ 7 回第 2 章 ~ 第 5 章 第 8 回中間ミニテスト (11 月 15 日 ) 第 9 回第 6 章 ~ 第 回ローム記念館 2Fの実習室で UML によるロボット制御実習 定期試験 2

講義の進め方 第 1 回イントロダクション ( 第 1 章 ) 第 2 ~ 7 回第 2 章 ~ 第 5 章 第 8 回中間ミニテスト (11 月 15 日 ) 第 9 回第 6 章 ~ 第 回ローム記念館 2Fの実習室で UML によるロボット制御実習 定期試験 2 ソフトウェア工学 第 7 回 木曜 5 限 F205 神原弘之 京都高度技術研究所 (ASTEM RI) http://www.metsa.astem.or.jp/se/ 1 講義の進め方 第 1 回イントロダクション ( 第 1 章 ) 第 2 ~ 7 回第 2 章 ~ 第 5 章 第 8 回中間ミニテスト (11 月 15 日 ) 第 9 回第 6 章 ~ 第 12 14 回ローム記念館 2Fの実習室で

More information

PowerPoint プレゼンテーション

PowerPoint プレゼンテーション BRMS への取り組みと導入事例 2013 年 11 月 15 日 ( 金 ) SCSK 株式会社 IT エンジニアリング事業本部ミドルウェア部 本日の内容 BRMS 適用のポイント BRMS の可能性 Page 1 Page 2 アプリケーション連携基盤 SCSKのRed Hat JBoss / ミドルウェア技術に関する取り組みの取り組み 世界のオープンソース コミュニティーから製品化されたソフトウェア

More information

リソース制約下における組込みソフトウェアの性能検証および最適化方法

リソース制約下における組込みソフトウェアの性能検証および最適化方法 リソース制約下における組込みソフト ウェアの性能検証および最適化方法 広島市立大学 大学院情報科学研究科システム工学専攻 中田明夫倉田和哉百々太市 1 提案技術の概要 組込みシステムの開発 厳しいリソース制約 (CPU, ネットワークなど ) 非機能要求 ( リアルタイム性など ) の達成 開発プロセスにおける設計段階 性能問題を発見することが困難 実装段階で性能問題が発覚 設計の手戻りが発生 設計段階での性能検証手法

More information

C#の基本

C#の基本 C# の基本 ~ 開発環境の使い方 ~ C# とは プログラミング言語のひとつであり C C++ Java 等に並ぶ代表的な言語の一つである 容易に GUI( グラフィックやボタンとの連携ができる ) プログラミングが可能である メモリ管理等の煩雑な操作が必要なく 比較的初心者向きの言語である C# の利点 C C++ に比べて メモリ管理が必要ない GUIが作りやすい Javaに比べて コードの制限が少ない

More information

IPSJ SIG Technical Report Vol.2015-SE-187 No /3/ Checking the Consisteny between Requirements Specification Documents and Regulations A

IPSJ SIG Technical Report Vol.2015-SE-187 No /3/ Checking the Consisteny between Requirements Specification Documents and Regulations A 1 1 1 Checking the Consisteny between Requirements Specification Documents and Regulations Abstract: When developers check the consistency between requirements specification documents and regulations by

More information

POSIXスレッド

POSIXスレッド POSIX スレッド (3) システムプログラミング 2011 年 11 月 7 日 建部修見 同期の戦略 単一大域ロック スレッドセーフ関数 構造的コードロッキング 構造的データロッキング ロックとモジュラリティ デッドロック 単一大域ロック (single global lock) 単一のアプリケーションワイドの mutex スレッドが実行するときに獲得, ブロックする前にリリース どのタイミングでも一つのスレッドが共有データをアクセスする

More information

1(FST ) FST FST FST 2(FST ) FST FST 4 FST MMDAgent FST FST 5 MMDAgent FST FST FST MMDAgent FST FST FSTFST 状態番号, 遷移先状態番号, 遷移条件, 出 FST 例 / ε ε / ε / は 1

1(FST ) FST FST FST 2(FST ) FST FST 4 FST MMDAgent FST FST 5 MMDAgent FST FST FST MMDAgent FST FST FSTFST 状態番号, 遷移先状態番号, 遷移条件, 出 FST 例 / ε ε / ε / は 1 DEIM Forum 2016 B8-5 排他制御機能を有する状態遷移機械に基づく 音声対話コンテンツ制御手法 石川 博規 堤 修平 山本 大介 高橋 直久 名古屋工業大学大学院工学研究科情報工学専攻 466 8555 愛知県名古屋市昭和区御器所町 E-mail: hiroki@moss.elcom.nitech.ac.jp, {tsutsumi.shuhei,yamamoto.daisuke,naohisa}@nitech.ac.jp

More information

Using VectorCAST/C++ with Test Driven Development

Using VectorCAST/C++ with Test Driven Development ホワイトペーパー V2.0 2018-01 目次 1 はじめに...3 2 従来型のソフトウェア開発...3 3 テスト主導型開発...4 4...5 5 TDD を可能にするテストオートメーションツールの主要機能...5 5.1 テストケースとソースコード間のトレーサビリティー...5 5.2 テストケースと要件間のトレーサビリティー...6 6 テスト主導型開発の例...7 2 1 はじめに 本書では

More information

2015 TRON Symposium セッション 組込み機器のための機能安全対応 TRON Safe Kernel TRON Safe Kernel の紹介 2015/12/10 株式会社日立超 LSIシステムズ製品ソリューション設計部トロンフォーラム TRON Safe Kernel WG 幹事

2015 TRON Symposium セッション 組込み機器のための機能安全対応 TRON Safe Kernel TRON Safe Kernel の紹介 2015/12/10 株式会社日立超 LSIシステムズ製品ソリューション設計部トロンフォーラム TRON Safe Kernel WG 幹事 2015 TRON Symposium セッション 組込み機器のための機能安全対応 TRON Safe Kernel TRON Safe Kernel の紹介 2015/12/10 株式会社日立超 LSIシステムズ製品ソリューション設計部トロンフォーラム TRON Safe Kernel WG 幹事 豊山 祐一 Hitachi ULSI Systems Co., Ltd. 2015. All rights

More information

智美塾 ゆもつよメソッドのアーキテクチャ

智美塾 ゆもつよメソッドのアーキテクチャ ゆもつよメソッドのテスト要求分析とテストアーキテクチャ設計 JaSST13 東京智美塾 2013 年 1 月 30 日 湯本剛 ( 日本 HP) tsuyoshi.yumoto@hp.com ゆもつよ風テスト開発プロセス テスト計画 実現したい品質の具体的把握 テスト箇所の選択 テストの目的設定 テスト対象アイテム特定 テスト分析 テストタイプ特定 機能の整理 & 再分類 テスト条件となる仕様項目特定

More information

Linkexpress トラブル初期調査資料 採取コマンド使用手引書

Linkexpress トラブル初期調査資料 採取コマンド使用手引書 FUJITSU Software Linkexpress Standard Edition V5.0L15 Linkexpress Enterprise Edition V5.0L15 Linkexpress トラブル初期調査資料採取コマンド使用手引書 Windows/Windows(64) J2X1-2740-14Z0(00) 2014 年 12 月 まえがき 本書の目的 本書は 下記製品でエラーが発生した場合の初期調査資料の採取方法を説明します

More information

アナリシスパターン勉強会 責任関係事例紹介 株式会社オーエスケイ小井土亨 (CBOP COM 分科会主査 ) 2000/07/19 1

アナリシスパターン勉強会 責任関係事例紹介 株式会社オーエスケイ小井土亨 (CBOP COM 分科会主査 ) 2000/07/19 1 アナリシスパターン勉強会 責任関係事例紹介 株式会社オーエスケイ小井土亨 (CBOP COM 分科会主査 ) 2000/07/19 1 Agenda システム開発概要 事例説明 システム要件 ( 画面イメージ ) 組織型データ管理フレームワーク詳細 人事情報管理システム詳細 フレームワーク利用カタログ 略語説明 FW フレームワーク CS カスタマイズシステム ( 実行可能な具体システム ) IF

More information

製品開発の現場では 各種のセンサーや測定環境を利用したデータ解析が行われ シミュレーションや動作検証等に役立てられています しかし 日々収集されるデータ量は増加し 解析も複雑化しており データ解析の負荷は徐々に重くなっています 例えば自動車の車両計測データを解析する場合 取得したデータをそのまま解析

製品開発の現場では 各種のセンサーや測定環境を利用したデータ解析が行われ シミュレーションや動作検証等に役立てられています しかし 日々収集されるデータ量は増加し 解析も複雑化しており データ解析の負荷は徐々に重くなっています 例えば自動車の車両計測データを解析する場合 取得したデータをそのまま解析 ホワイトペーパー Excel と MATLAB の連携がデータ解析の課題を解決 製品開発の現場では 各種のセンサーや測定環境を利用したデータ解析が行われ シミュレーションや動作検証等に役立てられています しかし 日々収集されるデータ量は増加し 解析も複雑化しており データ解析の負荷は徐々に重くなっています 例えば自動車の車両計測データを解析する場合 取得したデータをそのまま解析に使用することはできず

More information

PowerPoint プレゼンテーション

PowerPoint プレゼンテーション 5 月 Java 基礎 1 タイトル Java 基礎 2 日間 概要 目的 サーバサイドのプログラミング言語で最もシェアの高い Java SE の基本を習得します 当研修ではひとつの技術ごとに実用的なアプリケーションを作成するため 効果的な学習ができます Java SE の多くの API の中で 仕事でよく利用するものを中心に効率よく学びます 実際の業務で最も利用される開発環境である Eclipse

More information

D5-2_S _003.pptx

D5-2_S _003.pptx JaSST 14 Tokyo セッション D5-2 10:30~11:00(30 分 ) キーワード駆動テストを用いた GUI テスト自動化による工期短縮実現への取り組み 2014 年 3 月 8 日 株式会社 NTT データ 技術開発本部プロアクティブ テスティング COE 小林由依 0. 自己紹介 n 氏名 Ø 小林由依 n 所属 Ø 株式会社 NTT データ技術開発本部 プロジェクトマネジメント

More information

An Automated Proof of Equivalence on Quantum Cryptographic Protocols

An Automated Proof of Equivalence on Quantum Cryptographic Protocols 量子暗号のための プロトコル等価性検証ツール 久保田貴大 *, 角谷良彦 *, 加藤豪, 河野泰人, 櫻田英樹 * 東京大学情報理工学系研究科, NTT コミュニケーション科学基礎研究所 背景 暗号安全性証明の検証は難しい 量子暗号でもそうである 検証のための形式体系が提案されているが, 実際には, 形式体系の適用は手作業では非常に煩雑である 形式検証のためには, 検証ツールが開発されることが望ましい

More information

Oracle Business Rules

Oracle Business Rules Oracle Business Rules Manoj Das(manoj.das@oracle.com) Product Management, Oracle Integration 3 Oracle Business Rules について Oracle Business Rules とはビジネスの重要な決定と方針 ビジネスの方針 実行方針 承認基盤など 制約 有効な設定 規制要件など 計算 割引

More information

3. 回路図面の作図 回路図の作成では 部品など回路要素の図記号を配置し 要素どうしを配線するが それぞれの配線には 線番 などの電気的な情報が存在する 配線も単なる線ではなく 信号の入力や出力など部品どうしを結び付ける接続情報をもたせることで回路としての意味をもつ このように回路図を構成する図面は

3. 回路図面の作図 回路図の作成では 部品など回路要素の図記号を配置し 要素どうしを配線するが それぞれの配線には 線番 などの電気的な情報が存在する 配線も単なる線ではなく 信号の入力や出力など部品どうしを結び付ける接続情報をもたせることで回路としての意味をもつ このように回路図を構成する図面は 汎用 CAD に対する電気設計専用 CAD の優位性 株式会社ワコムソフトウェア営業本部ソフトウェア営業部 1. はじめに弊社は 1984 年に電気設計専用 CAD システムを発売以来 日本のものづくりを担うお客様とともに成長し 電気制御設計の現場で 要求レベルの高いお客様ニーズに応えるために改良に改良を重ね 卓越した製品力を誇るまでに至った しかしながら 電気設計の用途でも汎用 CAD を利用されている企業は多く存在している

More information

Microsoft PowerPoint - 教材サンプル1&2.ppt

Microsoft PowerPoint - 教材サンプル1&2.ppt ソフトウェアバグの現状 : 膨大化するソフトウエア開発と生産性 開発機能数 つの機能を開発する時間開発時間 ( 相対 ) ソフトの量 (FP) 2 2 96 97 98 99 2 2 生産性 (H/FP) 7 6 4 3 2 96 97 98 99 2 2 4 3 2 ソフトウェアエンジニアリングの効果 食い止める何かが必要 96 97 98 99 2 2 出典 :Software Metrics

More information

変更の影響範囲を特定するための 「標準調査プロセス」の提案 2014年ソフトウェア品質管理研究会(30SQiP-A)

変更の影響範囲を特定するための 「標準調査プロセス」の提案  2014年ソフトウェア品質管理研究会(30SQiP-A) 変更の影響範囲を特定するための 標準調査プロセス の提案 2014 年ソフトウェア品質管理研究会 [ 第 6 分科会 A グループ ] リーダー : 宇田泰子 ( アンリツエンジニアリング株式会社 ) 夛田一成 ( アンリツエンジニアリング株式会社 ) 川井めぐみ ( サントリーシステムテクノロジー株式会社 ) 伊藤友一 (TIS 株式会社 ) 1. 研究の動機 研究員の現場では 調査を行なっているにも関わらず

More information

Microsoft PowerPoint - H22制御工学I-10回.ppt

Microsoft PowerPoint - H22制御工学I-10回.ppt 制御工学 I 第 回 安定性 ラウス, フルビッツの安定判別 平成 年 6 月 日 /6/ 授業の予定 制御工学概論 ( 回 ) 制御技術は現在様々な工学分野において重要な基本技術となっている 工学における制御工学の位置づけと歴史について説明する さらに 制御システムの基本構成と種類を紹介する ラプラス変換 ( 回 ) 制御工学 特に古典制御ではラプラス変換が重要な役割を果たしている ラプラス変換と逆ラプラス変換の定義を紹介し

More information

Oracle Un お問合せ : Oracle Data Integrator 11g: データ統合設定と管理 期間 ( 標準日数 ):5 コースの概要 Oracle Data Integratorは すべてのデータ統合要件 ( 大量の高パフォーマンス バッチ ローブンの統合プロセスおよ

Oracle Un お問合せ : Oracle Data Integrator 11g: データ統合設定と管理 期間 ( 標準日数 ):5 コースの概要 Oracle Data Integratorは すべてのデータ統合要件 ( 大量の高パフォーマンス バッチ ローブンの統合プロセスおよ Oracle Un お問合せ : 0120- Oracle Data Integrator 11g: データ統合設定と管理 期間 ( 標準日数 ):5 コースの概要 Oracle Data Integratorは すべてのデータ統合要件 ( 大量の高パフォーマンス バッチ ローブンの統合プロセスおよびSOA 対応データ サービスへ ) を網羅する総合的なデータ統合プラットフォームです Oracle

More information

エンジニアリング・サービスから見たMBD導入の成功・失敗

エンジニアリング・サービスから見たMBD導入の成功・失敗 2014 年 12 月 18 日 ( 金 ) 16:40-16:55 JMAAB 中部コンファレンス エンジニアリング サービスから見た MBD 導入の成功 失敗 COPYRIGHT (C) GAIO TECHNOLOGY ALL RIGHTS RESERVED 1 ガイオ テクノロジーとは 組み込み業界向け検証ツールメーカー コンパイラ 検証 テスト 解析ツール プロトタイピングツール エンジニアリングサービス

More information

プログラマブル論理デバイス

プログラマブル論理デバイス 第 8 章プログラマブル論理デバイス 大阪大学大学院情報科学研究科今井正治 E-mail: imai@ist.osaka-u.ac.jp http://www-ise.ist.osaka-u.ac.jp/~imai/ 26/2/5 26, Masaharu Imai 講義内容 PLDとは何か PLA FPGA Gate Arra 26/2/5 26, Masaharu Imai 2 PLD とは何か

More information

並列計算導入.pptx

並列計算導入.pptx 並列計算の基礎 MPI を用いた並列計算 並列計算の環境 並列計算 複数の計算ユニット(PU, ore, Pなど を使用して 一つの問題 計算 を行わせる 近年 並列計算を手軽に使用できる環境が急速に整いつつある >通常のP PU(entral Processing Unit)上に計算装置であるoreが 複数含まれている Intel ore i7 シリーズ: 4つの計算装置(ore) 通常のプログラム

More information

プログラミング基礎

プログラミング基礎 C プログラミング Ⅰ 授業ガイダンス C 言語の概要プログラム作成 実行方法 授業内容について 授業目的 C 言語によるプログラミングの基礎を学ぶこと 学習内容 C 言語の基礎的な文法 入出力, 変数, 演算, 条件分岐, 繰り返し, 配列,( 関数 ) C 言語による簡単な計算処理プログラムの開発 到達目標 C 言語の基礎的な文法を理解する 簡単な計算処理プログラムを作成できるようにする 授業ガイダンス

More information

ビッグデータ分析を高速化する 分散処理技術を開発 日本電気株式会社

ビッグデータ分析を高速化する 分散処理技術を開発 日本電気株式会社 ビッグデータ分析を高速化する 分散処理技術を開発 日本電気株式会社 概要 NEC は ビッグデータの分析を高速化する分散処理技術を開発しました 本技術により レコメンド 価格予測 需要予測などに必要な機械学習処理を従来の 10 倍以上高速に行い 分析結果の迅速な活用に貢献します ビッグデータの分散処理で一般的なオープンソース Hadoop を利用 これにより レコメンド 価格予測 需要予測などの分析において

More information

JTAG バウンダリスキャンテストの容易化設計を支援する OrCAD Capture の無償プラグイン 21 July 2017 ( 富士設備 / 浅野義雄 )

JTAG バウンダリスキャンテストの容易化設計を支援する OrCAD Capture の無償プラグイン 21 July 2017 ( 富士設備 / 浅野義雄 ) JTAG バウンダリスキャンテストの容易化設計を支援する OrCAD Capture の無償プラグイン 21 July 2017 ( 富士設備 / 浅野義雄 ) PACKAGE COMPLEXITY & TRANSISTOR COUNT 課題 : 実装検査 不良解析 デバッグ プローブ接続では BGA 実装の検査 / 解析 / デバッグができない プローブ接続が困難な高密度実装は増加の一方 このままではテスト費用のほうが高くなる!

More information

機能検証トレーニング コース一覧

機能検証トレーニング コース一覧 機能検証トレーニング コース一覧 日本シノプシス合同会社 2016.03 トレーニング コース一覧 VCS/DVE 基本コース VCS-NLP/VC LP 基本コース VC Verification IP AXI 基本コース (UVM 版 ) VC Verification IP USB 基本コース (UVM 版 ) Verdi 3 基本コース SpyGlass Lint コース SpyGlass

More information

Presentation Title

Presentation Title コード生成製品の普及と最新の技術動向 MathWorks Japan パイロットエンジニアリング部 東達也 2014 The MathWorks, Inc. 1 MBD 概要 MATLABおよびSimulinkを使用したモデルベース デザイン ( モデルベース開発 ) 紹介ビデオ 2 MBD による制御開発フローとコード生成製品の活用 制御設計の最適化で性能改善 設計図ですぐに挙動確認 MILS:

More information

目次 1: 安全性とソフトウェア 2: 宇宙機ソフトウェアにおける 安全 とは 3:CBCS 安全要求とは 4: 宇宙機ソフトウェアの実装例 5: 安全設計から得た新たな知見 6: 今後 2

目次 1: 安全性とソフトウェア 2: 宇宙機ソフトウェアにおける 安全 とは 3:CBCS 安全要求とは 4: 宇宙機ソフトウェアの実装例 5: 安全設計から得た新たな知見 6: 今後 2 宇宙機ソフトウェアにおける 安全要求と設計事例 宇宙航空研究開発機構 (JAXA) 情報 計算工学センター (JEDI) 梅田浩貴 (Hiroki Umeda) 目次 1: 安全性とソフトウェア 2: 宇宙機ソフトウェアにおける 安全 とは 3:CBCS 安全要求とは 4: 宇宙機ソフトウェアの実装例 5: 安全設計から得た新たな知見 6: 今後 2 1.1 安全性とは 安全性と信頼性の違いの例開かない踏切りは

More information

NEXCESS基礎コース01 組込みソフトウェア開発技術の基礎 ソフトウェア開発プロセス編

NEXCESS基礎コース01 組込みソフトウェア開発技術の基礎 ソフトウェア開発プロセス編 JaSST 12 Tokai SIG テストエンジニアだからこそ気を付けるテスト仕様書と報告書の書き方 2012 年 11 月 30 日 山本雅基 (ASDoQ/ 名古屋大学 ) E-mail: myamamoto@nces.is.nagoya-u.ac.jp 1 トイレは いつ行ってもいい 気楽に 自己紹介 16:10-16:20 お話 16:20-16:40 個人作業 16:40-16:55 グループ作業

More information

<4D F736F F F696E74202D C190DD B A CB48D65208E DC58F49205B8CDD8AB B83685D>

<4D F736F F F696E74202D C190DD B A CB48D65208E DC58F49205B8CDD8AB B83685D> 今さら聞けない高位合成 ~ 一から学ぶ高位合成 ~ シャープ株式会社電子デバイス事業本部副参事山田晃久 1 ハードウェア設計と抽象度 要求仕様 動作仕様設計制約 ( コスト 性能 消費電力 ) システムの実現方式を決定システム設計 ( 動作レベル設計 ) ( アーキテクチャ アルゴリズム ) システム分割 (HW/SW) 機能ブロック RTL 記述 機能設計 (RTL 設計 ) 論理合成 ハードウェアの処理を設計

More information

arduino プログラミング課題集 ( Ver /06/01 ) arduino と各種ボードを組み合わせ 制御するためのプログラミングを学 ぼう! 1 入出力ポートの設定と利用方法 (1) 制御( コントロール ) する とは 外部装置( ペリフェラル ) が必要とする信号をマイ

arduino プログラミング課題集 ( Ver /06/01 ) arduino と各種ボードを組み合わせ 制御するためのプログラミングを学 ぼう! 1 入出力ポートの設定と利用方法 (1) 制御( コントロール ) する とは 外部装置( ペリフェラル ) が必要とする信号をマイ arduino プログラミング課題集 ( Ver.5.0 2017/06/01 ) arduino と各種ボードを組み合わせ 制御するためのプログラミングを学 ぼう! 1 入出力ポートの設定と利用方法 (1) 制御( コントロール ) する とは 外部装置( ペリフェラル ) が必要とする信号をマイコンから伝える 外部装置の状態をマイコンで確認する 信号の授受は 入出力ポート 経由で行う (2) 入出力ポートとは?

More information

研究レビューミーティング プレゼン資料 テンプレート

研究レビューミーティング プレゼン資料 テンプレート SWIM2012 年度第 4 回研究会 ビジネスモデルの記述に関する一考察 2013 年 2 月 20 日富士通研究所丸山文宏 Copyright 2013 Fujitsu Laboratories Ltd. 目次 ビジネスモデル記述法の提案 ビジネスモデルの記述例 考察 まとめ 1 Copyright 2013 Fujitsu Laboratories Ltd. ビジネスモデルの記述 新しいビジネスモデルとは

More information

今週の進捗

今週の進捗 Virtualize APIC access による APIC フック手法 立命館大学富田崇詠, 明田修平, 瀧本栄二, 毛利公一 2016/11/30 1 はじめに (1/2) マルウェアの脅威が問題となっている 2015年に4 億 3000 万以上の検体が新たに発見されている マルウェア対策にはマルウェアが持つ機能 挙動の正確な解析が重要 マルウェア動的解析システム : Alkanet 仮想計算機モニタのBitVisorの拡張機能として動作

More information

CA

CA PRIMEQUEST 2000 シリーズ Qlogic 製ファイバーチャネルカード ファームウェアアップデート手順書 QLE256x ファームウェア版数 FW:7.04.00, X86 BIOS:V3.29 QLE267x ファームウェア版数 FW:8.03.06, X86 BIOS:V3.43 Copyright 2016-2017 FUJITSU LIMITED 1/10 目次 1. 本書について...

More information

講義「○○○○」

講義「○○○○」 講義 システムの信頼性 内容. 直列システムの信頼性. 並列システムの信頼性 3. 直列 並列の複合システムの信頼性 4. 信頼性向上のための手法 担当 : 倉敷哲生 ビジネスエンジニアリング専攻 システムの構成 種々の機械や構造物, システムを分割していけば. 個々の要素 サブシステム となる. サブシステムの組み合わせ方式 直列系 並列系 m/ 冗長系 待機冗長系 3 直列システムの信頼性 直列系

More information

クラス図とシーケンス図の整合性確保 マニュアル

クラス図とシーケンス図の整合性確保 マニュアル Consistency between Class and Sequence by SparxSystems Japan Enterprise Architect 日本語版 クラス図とシーケンス図の整合性確保マニュアル (2011/12/6 最終更新 ) 1 1. はじめに UML を利用したモデリングにおいて クラス図は最も利用される図の 1 つです クラス図は対象のシステムなどの構造をモデリングするために利用されます

More information

X 線天文衛星ひとみ (ASTRO-H) への FRAM 適用 有人宇宙システム株式会社 IV&V 研究センター道浦康貴 宇宙航空研究開発機構第 3 研究ユニット片平真史 石濱直樹有人宇宙システム株式会社 IV&V 研究センター野本秀樹 道浦康貴 JAXA All Rights

X 線天文衛星ひとみ (ASTRO-H) への FRAM 適用 有人宇宙システム株式会社 IV&V 研究センター道浦康貴 宇宙航空研究開発機構第 3 研究ユニット片平真史 石濱直樹有人宇宙システム株式会社 IV&V 研究センター野本秀樹 道浦康貴 JAXA All Rights X 線天文衛星ひとみ (ASTRO-H) への FRAM 適用 2017.11.8 有人宇宙システム株式会社 IV&V 研究センター道浦康貴 宇宙航空研究開発機構第 3 研究ユニット片平真史 石濱直樹有人宇宙システム株式会社 IV&V 研究センター野本秀樹 道浦康貴 概要 X 線天文衛星 ASTRO-H ひとみ 異常事象調査報告書 を基に FRAM 分析を実施した結果を FRAM の分析手順に沿って紹介する

More information

OPN Terminalの利用方法

OPN Terminalの利用方法 OPN Term, OPN IME の利用方法 株式会社オプトエレクトロニクス 目次 1. 概要...3 1.1 OPN Termについて...3 1.2 OPN IMEについて...3 2. OPN Term 接続手順...3 2.1 OPN-2002 をスレーブに設定して接続する...3 2.3 OPN-2002 をマスターに設定して接続する...5 3. OPN Termを操作する...6 3.1

More information

.......p...{..P01-48(TF)

.......p...{..P01-48(TF) 1 2 3 5 6 7 8 9 10 Act Plan Check Act Do Plan Check Do 11 12 13 14 INPUT OUTPUT 16 17 18 19 20 21 22 23 24 25 26 27 30 33 32 33 34 35 36 37 36 37 38 33 40 41 42 43 44 45 46 47 48 49 50 51 1. 2. 3.

More information

Visual Studio と.NET Framework 概要 Runtime Libraries Languag es Tool.NET Visual Studio 概要 http://download.microsoft.com/download/c/7/1/c710b336-1979-4522-921b-590edf63426b/vs2010_guidebook_pdf.zip 1.

More information

VDM-SL ISO.VDM++ VDM-SL VDM- RT VDM++ VDM,.VDM, [5]. VDM VDM++.,,, [7]., VDM++.,., [7] VDM++.,,,,,,,.,,, VDM VDMTools OvertureTo

VDM-SL ISO.VDM++ VDM-SL VDM- RT VDM++ VDM,.VDM, [5]. VDM VDM++.,,, [7]., VDM++.,., [7] VDM++.,,,,,,,.,,, VDM VDMTools OvertureTo KAOS 1 1 1 1 1,.,. ( ). KAOS VDM++.,.,,, 1. 1.1,, [1].,,, [2].,, [3]. 1.2 ( ),, [3] KAOS, VDM++, KAOS VDM++ 1 Kyushu University, KAOS,, KAOS, KAOS, VDM++., 1.3 2,., 3, KAOS VDM++. 4, 3,. 5 2. 2.1,,,,,

More information

PowerPoint プレゼンテーション

PowerPoint プレゼンテーション 復習 ) 時系列のモデリング ~a. 離散時間モデル ~ y k + a 1 z 1 y k + + a na z n ay k = b 0 u k + b 1 z 1 u k + + b nb z n bu k y k = G z 1 u k = B(z 1 ) A(z 1 u k ) ARMA モデル A z 1 B z 1 = 1 + a 1 z 1 + + a na z n a = b 0

More information

2014 年 11 月 20 日 ET2014 スペシャルセッション C-2 mruby プログラム言語 Ruby による組込みソト開発 九州工業大学田中和明 軽量 Ruby フォーラム Ruby アソシエーション

2014 年 11 月 20 日 ET2014 スペシャルセッション C-2 mruby プログラム言語 Ruby による組込みソト開発 九州工業大学田中和明 軽量 Ruby フォーラム Ruby アソシエーション 2014 年 11 月 20 日 ET2014 スペシャルセッション C-2 mruby プログラム言語 Ruby による組込みソト開発 九州工業大学田中和明 軽量 Ruby フォーラム Ruby アソシエーション 講演の内容 mruby 概要紹介 九州工業大学, 田中和明 mruby デバッガ紹介 福岡 CSK, 三牧弘司 NPO 法人軽量 Ruby フォーラムの紹介 NPO 法人軽量 Ruby

More information

NetworkVantage 9

NetworkVantage 9 DevPartner エラー検出 はじめてのエラー検出 (Unmanaged VC++ 版 ) 本書は はじめてエラー検出を使用する際に参考していただくドキュメントです 詳細な情報につきましては 製品に付属しているオンラインドキュメントならびにオンラインヘルプをご参照ください なお 本書は Visual Studio 2010 をベースとして説明しております Visual Studio 6.0 の場合は

More information

Microsoft PowerPoint - 08LR-conflicts.ppt [互換モード]

Microsoft PowerPoint - 08LR-conflicts.ppt [互換モード] 属性文法 コンパイラ理論 8 LR 構文解析補足 : 属性文法と conflicts 櫻井彰人 Racc (Yacc 系のcc) は属性文法的 非終端記号は 値 (semantic value) を持つ パーザーは パーザースタックをreduceするとき ( 使う規則を X ::= s とする ) s に付随する semantic value (Racc では配列 valueにある ) を用いて action

More information

スライド 1

スライド 1 心理と言語 A 第 13 回 論文レビュー Gass, S., & Mackey, A. (2007). Input, interaction, and output in second language acquisition. Logo The theory and its constructs (1) モデル (models) - 何らかの現象の how を説明 記述する 理論 (theories)

More information

メソッドのまとめ

メソッドのまとめ メソッド (4) 擬似コードテスト技法 http://java.cis.k.hosei.ac.jp/ 授業の前に自己点検以下のことがらを友達に説明できますか? メソッドの宣言とは 起動とは何ですか メソッドの宣言はどのように書きますか メソッドの宣言はどこに置きますか メソッドの起動はどのようにしますか メソッドの仮引数 実引数 戻り値とは何ですか メソッドの起動にあたって実引数はどのようにして仮引数に渡されますか

More information

はじめてのPFD

はじめてのPFD はじめての PFD 派生開発 WG アンリツエンジニアリング株式会社文書番号 :AE-RAEB00000063 初版 Copyright 2016 Anritsu Engineering Co.,Ltd. Publicly available 演習概要 PFDの書き方 : 15 分 演習 : 30 分 + 発表 ( 講評 ) 20 分 まとめ 2 参考文献 PFD(Process Flow Diagram)

More information

大域照明計算手法開発のためのレンダリングフレームワーク Lightmetrica: 拡張 検証に特化した研究開発のためレンダラ 図 1: Lightmetrica を用いてレンダリングした画像例 シーンは拡散反射面 光沢面を含み 複数の面光 源を用いて ピンホールカメラを用いてレンダリングを行った

大域照明計算手法開発のためのレンダリングフレームワーク Lightmetrica: 拡張 検証に特化した研究開発のためレンダラ 図 1: Lightmetrica を用いてレンダリングした画像例 シーンは拡散反射面 光沢面を含み 複数の面光 源を用いて ピンホールカメラを用いてレンダリングを行った 大域照明計算手法開発のためのレンダリングフレームワーク Lightmetrica: 拡張 検証に特化した研究開発のためレンダラ 図 1: Lightmetrica を用いてレンダリングした画像例 シーンは拡散反射面 光沢面を含み 複数の面光 源を用いて ピンホールカメラを用いてレンダリングを行った モデルとして外部から読み込んだ三角形メ ッシュを用いた このように Lightmetrica はレンダラとして写実的な画像を生成する十分な実力を有する

More information

はじめに : ご提案のポイント

はじめに : ご提案のポイント 4. 組織へのフォーマルメソッドの導入方法 本章では フォーマルメソッドを組織に導入する際の障害を解決するための手順やポイントを 示す 本章の概要は以下の通りである 対象読者目的想定知識得られる知見等 (1) ベンダー上級管理者 (2) 開発プロジェクト管理者 (3) 開発技術者 等フォーマルメソッドを組織に導入する際の作業プロセス ( 導入プロセス ) と導入のポイントについて整理する さらに導入検討の際に有用と思われる情報源

More information

Layout 1

Layout 1 Industrial communication センサーのデータにアクセスする ifm の IO-Link Digital connection technology for sensors とは? 今日のセンサーはシンプルな ON/OFF のセンサーから 大量のデータを処理するマイクロプロセッサーを搭載した高性能なデバイスまで進化してきました センサー内のデータにアクセスする IO-Link は以下の特徴があるインターフェースです

More information

PowerPoint Presentation

PowerPoint Presentation ソフトウェア演習 B GUI を持つ Java プログラムの 設計と実装 4.1 例題 :GUI を持った電卓を作ろう プロジェクトCalculator パッケージ名 :example ソースファイル : Calculator.java GUI.java EventProcessor.java 2 4.2 GUI とイベント処理 GUI の構成 :Swing GUI の場合 フレーム JFrame:

More information

shift/reset [13] 2 shift / reset shift reset k call/cc reset shift k shift (...) k 1 + shift(fun k -> 2 * (k 3)) k 2 * (1 + 3) 8 reset shift reset (..

shift/reset [13] 2 shift / reset shift reset k call/cc reset shift k shift (...) k 1 + shift(fun k -> 2 * (k 3)) k 2 * (1 + 3) 8 reset shift reset (.. arisa@pllab.is.ocha.ac.jp asai@is.ocha.ac.jp shift / reset CPS shift / reset CPS CPS 1 [3, 5] goto try/catch raise call/cc [17] control/prompt [8], shift/reset [5] control/prompt, shift/reset call/cc (continuationpassing

More information

1. はじめに 本書は スプリット演算器 MFS2 用コンフィギュレータソフトウェア の取扱方法 操作手順 注意事項などを説明したものです Windows の操作や用語を理解している方を前提にしています Windows の操作や用語については それぞれのマニュアルを参照してください 1.1. MFS

1. はじめに 本書は スプリット演算器 MFS2 用コンフィギュレータソフトウェア の取扱方法 操作手順 注意事項などを説明したものです Windows の操作や用語を理解している方を前提にしています Windows の操作や用語については それぞれのマニュアルを参照してください 1.1. MFS スプリット演算器 MFS2 用コンフィギュレータソフトウェア MFS2CFG バージョン 0.02 取扱説明書 1/10 NM-9307 改 2 1. はじめに 本書は スプリット演算器 MFS2 用コンフィギュレータソフトウェア の取扱方法 操作手順 注意事項などを説明したものです Windows の操作や用語を理解している方を前提にしています Windows の操作や用語については それぞれのマニュアルを参照してください

More information

2) では, 図 2 に示すように, 端末が周囲の AP を認識し, 認識した AP との間に接続関係を確立する機能が必要である. 端末が周囲の AP を認識する方法は, パッシブスキャンとアクティブスキャンの 2 種類がある. パッシブスキャンは,AP が定期的かつ一方的にビーコンを端末へ送信する

2) では, 図 2 に示すように, 端末が周囲の AP を認識し, 認識した AP との間に接続関係を確立する機能が必要である. 端末が周囲の AP を認識する方法は, パッシブスキャンとアクティブスキャンの 2 種類がある. パッシブスキャンは,AP が定期的かつ一方的にビーコンを端末へ送信する ns-2 による無線 LAN インフラストラクチャモードのシミュレーション 樋口豊章 伊藤将志 渡邊晃 名城大学理工学部 名城大学大学院理工学研究科 1. はじめに大規模で複雑なネットワーク上で発生するトラヒックを解析するために, シミュレーションは有効な手段である. ns-2(network Simulator - 2) はオープンソースのネットワークシミュレータであり, 多くの研究機関で利用されている.

More information

スクールCOBOL2002

スクールCOBOL2002 3. 関連資料 - よく使われる機能の操作方法 - (a) ファイルの入出力処理 - 順ファイル等を使ったプログラムの実行 - - 目次 -. はじめに 2. コーディング上の指定 3. 順ファイルの使用方法 4. プリンタへの出力方法 5. 索引ファイルの使用方法 6. 終わりに 2 . はじめに 本説明書では 簡単なプログラム ( ファイル等を使わないプログラム ) の作成からコンパイル 実行までの使用方法は既に理解しているものとして

More information

第 10 回 WOCS2 アシュアランスケースにおける品質到達性と トレーサビリティを考慮した記述ルール提案と 超小型衛星開発への適用評価 田中康平 1, 松野裕 2, 中坊嘉宏 3, 白坂成功 1, 中須賀真一 4 1 慶應義塾大学大学院システムデザイン マネジメント研究科 2 名古屋大学情報連携

第 10 回 WOCS2 アシュアランスケースにおける品質到達性と トレーサビリティを考慮した記述ルール提案と 超小型衛星開発への適用評価 田中康平 1, 松野裕 2, 中坊嘉宏 3, 白坂成功 1, 中須賀真一 4 1 慶應義塾大学大学院システムデザイン マネジメント研究科 2 名古屋大学情報連携 アシュアランスケースにおける品質到達性と トレーサビリティを考慮した記述ルール提案と 超小型衛星開発への適用評価 田中康平 1, 松野裕 2, 中坊嘉宏 3, 白坂成功 1, 中須賀真一 4 1 慶應義塾大学大学院システムデザイン マネジメント研究科 2 名古屋大学情報連携統括本部情報戦略室 3 独立行政法人産業技術総合研究所知能システム研究部門ディペンダブルシステム研究グループ 4 東京大学工学系研究科航空宇宙工学専攻

More information

IBIS Quality Framework IBIS モデル品質向上のための枠組み

IBIS Quality Framework IBIS モデル品質向上のための枠組み Quality Framework モデル品質向上のための枠組み EDA 標準 WG 1 目次 - 目次 - 1. 活動の背景 2. Quality Framework 3. ウェブサイトのご紹介 4. Frameworkの活用方法 2 目次 - 目次 - 1. 活動の背景 2. Quality Framework 3. ウェブサイトのご紹介 4. Frameworkの活用方法 3 1. 活動の背景

More information

モータ HILS の概要 1 はじめに モータ HILS の需要 自動車の電子化及び 電気自動車やハイブリッド車の実用化に伴い モータの使用数が増大しています 従来行われていた駆動用モータ単体のシミュレーション レシプロエンジンとモータの駆動力分配制御シミュレーションの利用に加え パワーウインドやサ

モータ HILS の概要 1 はじめに モータ HILS の需要 自動車の電子化及び 電気自動車やハイブリッド車の実用化に伴い モータの使用数が増大しています 従来行われていた駆動用モータ単体のシミュレーション レシプロエンジンとモータの駆動力分配制御シミュレーションの利用に加え パワーウインドやサ モータ HILS の概要 1 はじめに モータ HILS の需要 自動車の電子化及び 電気自動車やハイブリッド車の実用化に伴い モータの使用数が増大しています 従来行われていた駆動用モータ単体のシミュレーション レシプロエンジンとモータの駆動力分配制御シミュレーションの利用に加え パワーウインドやサンルーフなどのボディー系 電動パワーステアリングやそのアシスト機能など 高度な制御 大電流の制御などが要求されています

More information

3.1 Thalmic Lab Myo * Bluetooth PC Myo 8 RMS RMS t RMS(t) i (i = 1, 2,, 8) 8 SVM libsvm *2 ν-svm 1 Myo 2 8 RMS 3.2 Myo (Root

3.1 Thalmic Lab Myo * Bluetooth PC Myo 8 RMS RMS t RMS(t) i (i = 1, 2,, 8) 8 SVM libsvm *2 ν-svm 1 Myo 2 8 RMS 3.2 Myo (Root 1,a) 2 2 1. 1 College of Information Science, School of Informatics, University of Tsukuba 2 Faculty of Engineering, Information and Systems, University of Tsukuba a) oharada@iplab.cs.tsukuba.ac.jp 2.

More information

CW6_A1441_15_D06.indd

CW6_A1441_15_D06.indd 技術紹介 EPS 用 ECU 試作開発における MBD の適用 小林将之 1 はじめに 従来の組込み制御システム開発の多くは, ドキュメントベースの設計とハンドコーディングにより行われてきた. しかしながら, 自動車分野を中心に電子制御システムの高性能 多機能化が進む一方, 高品質 低コストかつ開発期間の短縮化が要求されている.KYBの代表的な電子制御システムの一つである電動パワーステアリング (

More information

Microsoft PowerPoint - ●SWIM_ _INET掲載用.pptx

Microsoft PowerPoint - ●SWIM_ _INET掲載用.pptx シーケンスに基づく検索モデルの検索精度について 東京工芸大学工学部コンピュータ応用学科宇田川佳久 (1/3) (2/3) 要員数 情報システム開発のイメージソースコード検索機能 他人が作ったプログラムを保守する必要がある 実務面での応用 1 バグあるいは脆弱なコードを探す ( 品質の高いシステムを開発する ) 2 プログラム理解を支援する ( 第 3 者が書いたコードを保守する ) 要件定義外部設計内部設計

More information

SLCONFIG の操作 JF1PYE Ⅰ. PC と slconfig の通信設定 Ⅱ. Slconfig の操作 Ⅲ. 端末ソフトによる Command 機能 Ⅳ. slconfig 実行形式プログラムの作成 Ⅴ. 端末ソフト Tera Term のダウンロード インストー

SLCONFIG の操作 JF1PYE Ⅰ. PC と slconfig の通信設定 Ⅱ. Slconfig の操作 Ⅲ. 端末ソフトによる Command 機能 Ⅳ. slconfig 実行形式プログラムの作成 Ⅴ. 端末ソフト Tera Term のダウンロード インストー SLCONFIG の操作 2011.03.02 JF1PYE Ⅰ. PC と slconfig の通信設定 Ⅱ. Slconfig の操作 Ⅲ. 端末ソフトによる Command 機能 Ⅳ. slconfig 実行形式プログラムの作成 Ⅴ. 端末ソフト Tera Term のダウンロード インストール 設定 Soliloc-10G Slconfig の開発 提供ならびに本書を作成するに当たり情報提供を頂いた

More information

PowerPoint Presentation

PowerPoint Presentation マイコンシステム 第 12 回 青森大学ソフトウェア情報学部 橋本恭能 haship@aomori-u.ac.jp 目次 講義 内部設計 3 Deviceタブ Actionタブの関数実装 例題 定義した機能を実現する方法を検討する 課題 動作確認 2 講義 内部設計 3 残りの関数を実装 3 組込みシステム開発 週テーマ内容 7 キッチンタイマーの組立キッチンタイマーのハードを製作 確認 8 9 10

More information

C#の基本2 ~プログラムの制御構造~

C#の基本2 ~プログラムの制御構造~ C# の基本 2 ~ プログラムの制御構造 ~ 今回学ぶ事 プログラムの制御構造としての単岐選択処理 (If 文 ) 前判定繰り返し処理(for 文 ) について説明を行う また 整数型 (int 型 ) 等の組み込み型や配列型についても解説を行う 今回作るプログラム 入れた文字の平均 分散 標準偏差を表示するプログラム このプログラムでは calc ボタンを押すと計算を行う (value は整数に限る

More information

インターリーブADCでのタイミングスキュー影響のデジタル補正技術

インターリーブADCでのタイミングスキュー影響のデジタル補正技術 1 インターリーブADCでのタイミングスキュー影響のデジタル補正技術 浅見幸司 黒沢烈士 立岩武徳 宮島広行 小林春夫 ( 株 ) アドバンテスト 群馬大学 2 目次 1. 研究背景 目的 2. インターリーブADCの原理 3. チャネル間ミスマッチの影響 3.1. オフセットミスマッチの影響 3.2. ゲインミスマッチの影響 3.3. タイミングスキューの影響 4. 提案手法 4.1. インターリーブタイミングミスマッチ補正フィルタ

More information

TOPPERS 活用アイデア アプリケーション開発 コンテスト 部門 : 活用アイデア部門アプリケーション開発部門 作品のタイトル : Toppers_JSP と Scicos_lab / (Scilab でも可 ) による 組込みメカトロニクス制御シミュレーション 作成者 : 塩出武 ( シオデタ

TOPPERS 活用アイデア アプリケーション開発 コンテスト 部門 : 活用アイデア部門アプリケーション開発部門 作品のタイトル : Toppers_JSP と Scicos_lab / (Scilab でも可 ) による 組込みメカトロニクス制御シミュレーション 作成者 : 塩出武 ( シオデタ TOPPERS 活用アイデア アプリケーション開発 コンテスト 部門 : 活用アイデア部門アプリケーション開発部門 作品のタイトル : Toppers_JSP と Scicos_lab / (Scilab でも可 ) による 組込みメカトロニクス制御シミュレーション 作成者 : 塩出武 ( シオデタケシ ) 対象者 : 実機レス環境でモーター含むメカ制御プログラムの設計 および検証 学習をしてみたい方

More information

平成 19 年度 ( 第 29 回 ) 数学入門公開講座テキスト ( 京都大学数理解析研究所, 平成 19 ~8 年月 72 月日開催 30 日 ) 1 PCF (Programming language for Computable Functions) PCF adequacy adequacy

平成 19 年度 ( 第 29 回 ) 数学入門公開講座テキスト ( 京都大学数理解析研究所, 平成 19 ~8 年月 72 月日開催 30 日 ) 1 PCF (Programming language for Computable Functions) PCF adequacy adequacy 1 PCF (Programming language for Computable Functions) PCF adequacy adequacy 2 N X Y X Y f (x) f x f x y z (( f x) y) z = (( f (x))(y))(z) X Y x e X Y λx. e x x 2 + x + 1 λx. x 2 + x + 1 3 PCF 3.1 PCF PCF

More information

目次 1. システム概要 設置手順 注意事項 動作環境 初期設定 システム設定 ( 環境設定 ) システム設定 ( ログインパスワード変更 ) システム設定 ( ファイルのパスワード変

目次 1. システム概要 設置手順 注意事項 動作環境 初期設定 システム設定 ( 環境設定 ) システム設定 ( ログインパスワード変更 ) システム設定 ( ファイルのパスワード変 厚生労働省版ストレスチェック実施プログラム設置 設定マニュアル Ver.1.1 目次 1. システム概要... 2 2. 設置手順... 3 3. 注意事項... 5 4. 動作環境... 8 5. 初期設定... 9 6. システム設定 ( 環境設定 )... 15 7. システム設定 ( ログインパスワード変更 )... 18 8. システム設定 ( ファイルのパスワード変更 )... 20 9.

More information