(57)【要約】【課題】タイムバジェット最適化装置及び最適化方法を提供する。【解決手段】マルチタスクソフトウェアの設計段階において、性能要求を満足するために各タスクがどれだけ実行時間を使って良いか（タイムバジェット）を適切に決定できれば、性能要求を満たしコストや消費電力を抑えたシステム設計に有用である。本発明は、タスクグラフと各タスクが要するリソースの割り当て及びリソーススケジューリング方針から成る複数タスク動作仕様が与えられたとき、複数タスク動作仕様の任意のリソースについて、これを使用する全タスクのタイムバジェットを一定割合増加させた複数タスク動作仕様を求め、優先権付きストップウォッチペトリネットに変換し、性能要求を満たすか否かを検証しながらタイムバジェットを改善することにより、性能要求を満たすモデルに対し、同性能で各タスクのタイムバジェットを最適化する装置及び方法を提供する。【選択図】図７
2013171353.tif 000002
【特許請求の範囲】
【請求項１】
複数タスク動作仕様Aから優先権付きストップウォッチペトリネットBに変換する第１変換手段、
モデルチェッカを用いて前記ストップウォッチペトリネットBを検証する第１検証手段、
前記ストップウォッチペトリネットBが性能要求を満たすか否か判定する第１判定手段、
該第１判定手段により、該ストップウォッチペトリネットBがスループット要求を満たさずと判定されたとき、前記複数タスク動作仕様A は改善不能と出力する第１出力手段、
前記第１判定手段により、前記ストップウォッチペトリネットBが性能要求を満たすと判定されたとき、前記複数タスク動作仕様Aの任意のリソースriについて、該リソースriを使用する全タスクのタイムバジェットを一定割合増加させた複数タスク動作仕様Aiを求める演算手段、
前記複数タスク動作仕様Aiをそれぞれ優先権付きストップウォッチペトリネットBiに変換する第２変換手段、
モデルチェッカを用いて、前記各優先権付きストップウォッチペトリネットBiを検証する第２検証手段、
スループット要求を満たす前記各優先権付きストップウォッチペトリネットBiが存在するか否か判定する第２判定手段、
該第２判定手段により、性能要求を満たす前記各優先権付きストップウォッチペトリネットBiが存在せずと判定されたとき、前記複数タスク動作仕様A を改善された複数タスク動作仕様として出力する第２出力手段、
前記第２判定手段により、スループット要求を満たす前記各優先権付きストップウォッチペトリネットBiが存在すると判定されたとき、性能要求を満たした前記各優先権付きストップウォッチペトリネットBiのうち、最も最悪レイテンシが小さい前記各優先権付きストップウォッチペトリネットBiに対応する複数タスク動作仕様Aiを、複数タスク動作仕様Aとして選択するとともに該複数タスク動作仕様Aを前記演算手段に入力する選択手段、
を有してなるタイムバジェット最適化装置。
【請求項２】
入力されたデータを、複数タスク動作仕様Aから優先権付きストップウォッチペトリネットBに変換する第１変換ステップ、
モデルチェッカを用いて前記ストップウォッチペトリネットBを検証する第１検証ステップ、
前記ストップウォッチペトリネットBが性能要求を満たすか否か判定する第１判定ステップ、
該第１判定ステップにより、前記ストップウォッチペトリネットBが性能要求を満たさずと判定されたとき、前記複数タスク動作仕様A は改善不能と出力する第１出力ステップ、
前記第１判定ステップにより、前記ストップウォッチペトリネットBが性能要求を満たすと判定されたとき、前記複数タスク動作仕様Aの任意のリソースriについて、該リソースriを使用する全タスクのタイムバジェットを一定割合増加させた複数タスク動作仕様Aiを求める演算ステップ、
前記複数タスク動作仕様Aiをそれぞれ優先権付きストップウォッチペトリネットBiに変換する第２変換ステップ、
モデルチェッカを用いて、前記各優先権付きストップウォッチペトリネットBiを検証する第２検証ステップ、
性能要求を満たす前記各優先権付きストップウォッチペトリネットBiが存在するか否か判定する第２判定ステップ、
該第２判定ステップにより、性能要求を満たす前記各優先権付きストップウォッチペトリネットBiが存在せずと判定されたとき、前記複数タスク動作仕様A を改善された複数タスク動作仕様として出力する第２出力ステップ、
前記第２判定ステップにより、性能要求を満たす前記各優先権付きストップウォッチペトリネットBiが存在すると判定されたとき、性能要求を満たした前記各優先権付きストップウォッチペトリネットBiのうち最も最悪レイテンシが小さい前記各優先権付きストップウォッチペトリネットBiに対応する複数タスク動作仕様Aiを、複数タスク動作仕様Aとして選択するとともに該複数タスク動作仕様Aを前記演算手段に入力する選択ステップ、
を有してなるタイムバジェット最適化方法。
【発明の詳細な説明】
【技術分野】
【０００１】
本発明は、タイムバジェット最適化装置及び最適化方法に関する。
【背景技術】
【０００２】
機器に組み込まれるソフトウェアである組込みソフトウェアにおいては、コストや消費電力などの厳しいリソース制約のもとでの実時間性の実現を要求されることが多く(非特許文献１)、機能的要求に加えて性能などの非機能的要求の達成が重要となる。しかし、伝統的なソフトウェア開発手法においてはソフトウェア機能の正しさに焦点が置かれており、設計の途中で性能が大きく変化することを考慮していない。そのような開発手法においては性能問題が開発プロセスの後半で見つかることが多く、設計の見直しなど手戻りが生じる。そこで、開発プロセスの早期の段階で性能検証を行うことが有用である。
【０００３】
性能検証とは、ソフトウェアシステムがユーザの性能目標を満足するか否かを性能モデルに基づき予測し、検証することを指す。性能検証を行う手法としてはソフトウェア仕様モデルからソフトウェア性能検証モデルへ変換し、性能検証を行う方法が提案されている（非特許文献２）。
【０００４】
ソフトウェア性能モデルには、待ち行列ネットワークなどの確率的モデル（非特許文献３）と時間ペトリネット（非特許文献４）などの確定的モデルに分類される。確率的モデルはシステムの平均性能を考慮するのに対して、時間ペトリネットは最悪時(および最良時)の性能を考慮する。性能とリソース制約がともに厳しく、高い信頼性を要求される組込みソフトウェアを対象とする場合、最悪時に性能要求を満たせるか否かの検証が重要になる。
【０００５】
本発明者らは、従来、複数タスク動作仕様 (タスクグラフとリソース割り当て図の組)を優先権付きストップウォッチペトリネット(PrSwPN)に変換し、そのモデルを用いてスループット(単位時間当たりの処理能力) 要求を満たすか否かの検証を行う手法を提案している（非特許文献５）。しかし、従来手法ではスループット要求を満たすか否かの判断のみ行うため、検証結果をもとにモデルを改良することが困難であった。特に設計段階における各タスクの最悪実行時間は、実装前の段階では大まかな見積もりに基づく各タスクへの実行時間の配分と呼ぶべき性質のものである。これを本発明ではタイムバジェット(time budget)と呼ぶ。システム全体のスループットやレイテンシ（個々のデータが入力されてから出力されるまでの遅延）に関する要求を満たすように各タスクのタイムバジェットを適切に決定し、各タスクの実装段階においてはタイムバジェットの範囲内で実行できるようにプログラムコードおよびプロセッサやネットワークなどのハードウェアプラットフォームの性能を決定することにより、性能要求（スループット要求及びレイテンシ要求）を満たすシステムの効率的な設計が可能となる。
【先行技術文献】
【非特許文献】
【０００６】
【非特許文献１】Henzinger, T.A. and Sifakis、 J., ”Embedded Systems Design Challenge” Proc. of 14th Int. Symp. on Formal Methods (FM 2006), Lecture Notes in Computer Science, Vol.4085, Springer Verlag, pp.1-15, 2006.
【非特許文献２】Balsamo, S,. Marco, A.D., Inverardi, P. and Simeori, M., “Model-Based Performance Prediction in Software Development: A Survey”, IEEE Trans. on Soft. Eng., vol30, No.5, pp.295-310, 2004
【非特許文献３】Balsamo, S. and Marzolla, M., ”Performance evaluation of UML software architectures with multiclass Queueing Network models”, Proc. of 5th Int. Workshop on Software and Performance, Advancing Computing as a Science and Profession、 pp.37-42 ,2005.
【非特許文献４】Berthomieu, B., Peres, F., and Vernadat, F., “Model Checking Bounded Prioritized Time Petri Nets”, Proc. of 5th Int. Symp. on Automated Technology for Verification and Analysis (ATVA 2007), Lecture Notes in Computer Science, vol.4762, pp.523-532, 2007.
【非特許文献５】百々太市、中田明夫, ”プリエンティブスケジューリングによりリソースを共有する複数タスク動作仕様の性能検証”, 組込みシステムシンポジウム(ESS2010)論文集, pp.107-112, 2010.
【非特許文献６】Berthomieu, B. and Vernadat, F. “Time PetriNets Analysis with TINA”, Proc. of 3rd Int.Conf. on the Quantitative Evaluation of Systems(QEST 2006), IEEE Computer Society Press, 2006.
【発明の概要】
【発明が解決しようとする課題】
【０００７】
本発明は、前述のような事情に鑑みてなされたものであり、非特許文献５に示すスループット性能検証手法に対して、モデルのレイテンシ性能を同時に検証するよう従来手法を改良し、与えられたレイテンシ要求に対する余裕時間を各タスクに効果的に配分することにより、同性能で各タスクのタイムバジェットを最適化する装置及び方法を提供するものである。
【課題を解決するための手段】
【０００８】
請求項1に係るタイムバジェット最適化装置は、複数タスク動作仕様Aから優先権付きストップウォッチペトリネットBに変換する第１変換手段、モデルチェッカを用いて前記ストップウォッチペトリネットBを検証する第１検証手段、前記ストップウォッチペトリネットBが性能要求を満たすか否か判定する第１判定手段、該第１判定手段により、該ストップウォッチペトリネットBが性能要求を満たさずと判定されたとき、前記複数タスク動作仕様A は改善不能と出力する第１出力手段、前記第１判定手段により、前記ストップウォッチペトリネットBが性能要求を満たすと判定されたとき、前記複数タスク動作仕様Aの任意のリソースriについて、該リソースriを使用する全タスクのタイムバジェットを一定割合増加させた複数タスク動作仕様Aiを求める演算手段、前記複数タスク動作仕様Aiをそれぞれ優先権付きストップウォッチペトリネットBiに変換する第２変換手段、モデルチェッカを用いて、前記各優先権付きストップウォッチペトリネットBiを検証する第２検証手段、性能要求を満たす前記各優先権付きストップウォッチペトリネットBiが存在するか否か判定する第２判定手段、該第２判定手段により、性能要求を満たす前記各優先権付きストップウォッチペトリネットBiが存在せずと判定されたとき、前記複数タスク動作仕様A を改善された複数タスク動作仕様として出力する第２出力手手段、を有してなるものである。
【０００９】
請求項２に係るタイムバジェット最適化方法は、入力されたデータを、複数タスク動作仕様Aから優先権付きストップウォッチペトリネットBに変換する第１変換ステップ、モデルチェッカを用いて前記ストップウォッチペトリネットBを検証する第１検証ステップ、前記ストップウォッチペトリネットBが性能要求を満たすか否か判定する第１判定ステップ、該第１判定ステップにより、前記ストップウォッチペトリネットBが性能要求を満たさずと判定されたとき、前記複数タスク動作仕様A は改善不能と出力する第１出力ステップ、前記第１判定ステップにより、前記ストップウォッチペトリネットBが性能要求を満たすと判定されたとき、前記複数タスク動作仕様Aの任意のリソースriについて、該リソースriを使用する全タスクのタイムバジェットを一定割合増加させた複数タスク動作仕様Aiを求める演算ステップ、前記複数タスク動作仕様Aiをそれぞれ優先権付きストップウォッチペトリネットBiに変換する第２変換ステップ、モデルチェッカを用いて、前記各優先権付きストップウォッチペトリネットBiを検証する第２検証ステップ、性能要求を満たす前記各優先権付きストップウォッチペトリネットBiが存在するか否か判定する第２判定ステップ、該第２判定ステップにより、性能要求を満たす前記各優先権付きストップウォッチペトリネットBiが存在せずと判定されたとき、前記複数タスク動作仕様A を改善された複数タスク動作仕様として出力する第２出力ステップ、を有してなるものである。
【発明の効果】
【００１０】
本発明では、プリエンプティブスケジューリングでリソースを共有し、分岐や並列などの制御構造を持つ複数タスク動作仕様の入力から出力までの最悪レイテンシを既存のスループット性能検証手法を拡張した手法により求め、得られたレイテンシ要求までの余裕時間を各タスクのタイムバジェットに効果的に配分することにより、性能要求を満たしつつもタスクのタイムバジェットを最適化する装置及び方法を提供するものである。本発明によれば、性能要求の検証に確定的な時間を取り扱うPrSwPNを用いているため、最悪の場合の性能を検証することが可能であり、組込みソフトウェアなどの設計初期段階での性能検証に有効である。
【図面の簡単な説明】
【００１１】
【図１】時間軸上におけるタスクの実行状況を説明するための概略図である。
【図２】複数タスク動作仕様の例を示す図である。
【図３】PrSwPNで表したタスク図である。
【図４】スループット検証を行うためのPrSwPNを表す図である。
【図５】最悪レイテンシの計測を行うPrSwPNを示す図である。
【図６】系内に入力が複数滞留する場合のレイテンシ検証を行うPrSwPNを示す図である。
【図７】本発明に係るタイムバジェット最適化装置を説明するためのブロック図である。
【図８】本発明に係るタイムバジェット最適化方法を説明するためのフローチャートである。
【発明を実施するための形態】
【００１２】
諸定義
本発明が対象とするタイムバジェット最適化装置及び最適化方法に関する定義を述べる。
【００１３】
リアルタイムシステム
リアルタイムシステムとは、設定された時間通りに動作しなければならないコンピュータ 
システムのことをいう。通常、リアルタイムシステムではイベント(event)の発生ごとにタスクがリリースされ、定められたサービスを実行しなければならない。そしてある時刻までにサービスを完了しなければならない。イベントがリアルタイム処理系に発生すると、このイベントに関連づけられたタスクが実行を行う。また、タスクの実行のためには実行に必要となるリソースが全て使用可能であることが必須である。図 3 にタスクの実行状況を示す。
【００１４】
イベントが発生すると、そのイベントに関連づけられたタスクが到着(arrive)という。このことをタスクがリリース(release)されると呼び、この時点を矢印“↑”で示す。四角“□”（黒）の部分はタスクの処理を表している。start はタスクの処理の開始時刻、final はタスクの処理の完了時刻を表す。
【００１５】
タスクの最悪実行時間とはタスクが実行を開始してから実行を完了するまでにかかる一番長い時間のことをいう。図 １ においてはstart からfinal までの時間が最悪実行時間に対応する。タスクの最悪応答時間とはタスクがリリースしてから実行を完了するまでにかかる一番長い時間のことをいう。図１においてはrelease からfinal までの時間が最悪応答時間に対応する。release からdeadline までの時間のことを相対デッドラインという。一方、現在時刻にタスクの相対デッドラインを加えたものをタスクの絶対デッドラインという。タスクの処理の完了時刻final がデッドライン以下であるとき、タスクはデッドラインを満たすという。
【００１６】
スケジューリング方式
スケジューリング方式とは、一般に少数のリソースを共有する複数のタスク群において、すべてのタスクがデッドラインを満たすように、各タスクをどのような順番でいつからいつまで実行するかを決定する方式である。ここでリソースとしては、計算リソース（プロセッサ）のみならず、通信リソース（ネットワークや共有変数など）も含めて考慮する。
【００１７】
本発明では以下の 2つのスケジューリング方式を扱う。
【００１８】
１.早い者勝ち
早い者勝ち(FCFS: First Come First Served)とは先に到着したタスクが即座にリソースを獲得して実行するというスケジューリング方式である。
【００１９】
２.固定優先度スケジューリング
固定優先度スケジューリング(FP: Fixed Priority scheduling)とは、各タスクに固定の優先度を割り当て、複数のタスクがリソースについて競合した場合には割り当てられた固定優先度の大きいタスクがリソースを獲得し実行するというスケジューリング方式である。
【００２０】
優先権付きストップウォッチペトリネット
Nを0を含む自然数全体の集合、R+を非負実数全体の集合とする。ペトリネット(Petri Nets)は並列的・非同期的・分散的なシステムを表すための数学的モデルであり、5つの組PN =(P,T,F,W,M0)で定義される。ここで、Pはプレースの有限集合、Tはトランジションの有限集合、F⊆P×T∪T×P はアークの有限集合、W:FN はアークへの重みづけ関数である。アークp、t∈F に対して、pをtの出力プレースと呼ぶ。
【００２１】
各プレースには一般に複数のトークンを配置することによりシステムの状態を表現する。各プレースにおかれたトークンの数を返す関数M0:PN を初期マーキングと呼ぶ。マーキングMにおいて、トランジションt∈T のすべての入力プレースpについて、M(p)≧W(p,t) のとき、tは発火可能であるという。
【００２２】
またトランジションtが発火するとは、tが発火可能なマーキンにおいて、tの任意の入力プレースpから重みW(p,t )の数だけトークンを取り除き、tの任意の出力プレースp’ に重みW(t,p’) の数だけトークンを追加する動作のことであると定義する。トランジションの発火によりシステムの状態遷移が定義される。
【００２３】
ペトリネットPNの各トランジションt∈T に、発火可能になってから発火するまでの時間の下限(最小発火遅延)dmin:TR+ および、上限(最大発火遅延) dmax:TR+∪{∞}(dmax=∞ ならば上限なし)を付与したペトリネットを時間ペトリネット（TPN: Time Petri Nets）と定義する。
【００２４】
時間ペトリネットにおいては、各トランジションtはtが最後に発火可能になってからの経過時間θ(t)∈R+を保持するものとし(発火可能でないならθ(t)∈-∞ とする)、tが発火不能にならない限り、dmin≦θ(t)≦dmax を満たすいずれかの時刻にtは発火しなければならないと定義される。
【００２５】
時間ペトリネットに、トランジション間の優先権⊆T×T を付与したものを優先権付き時間ペトリネット(PrTPN: Prioritized Time Petri Nets)と定義する。優先権付き時間ペトリネットでは、2つのトランジションt1、 t2 ∈T が同時に発火可能なとき、もしt1 t2 ならば、t1 のみが発火できるものとする。
【００２６】
優先権付き時間ペトリネットに、ストップウォッチアークSｗ ⊆ T× P およびその重み付け関数 Wsw: Sw N を付与したものを優先権付きストップウォッチペトリネット(PrSwPN: Prioritized Stopwatch Petri Nets)と定義する。
【００２７】
優先権付きストップウォッチペトリネットでは、マーキングMにおいてトランジションtのすべてのストップウォッチアーク(t,p)∈Sw に対して、もしM(p)≧Wsw(t,p) ならば、tは最後に発火可能になってからの時間θ(t)を更新し続ける。さもなければ、tはθ(t)の値の更新を停止する。
【００２８】
性能検証手法
複数タスク動作仕様
非特許文献５に示される検証手法では、タスクグラフとリソース割り当て図をモデル化するために、複数タスク動作仕様を用いている。タスクグラフとは、順序関係を持つタスク同士を矢印でつなぎ、有向非閉路グラフとして表現したものである。リソース割り当て図とは、各タスクに割り当てるリソース、および、各リソースの使用が競合した場合にそれを解決するスケジューリング方針を指定した図である。タスクグラフとリソース割り当て図の組を複数タスク動作仕様と呼ぶ。複数タスク動作仕様と等価な振る舞いを行い、かつ、スループット要求を満たさなければ特定の動作を行うPrSwPNを作成し、スループット要求を満たすか否かの検証を行う。
【００２９】
複数タスク動作仕様TG は9つの組TG =(T, R, C, a, c, d, rr, sc) である。ここで、T はタスクの有限集合、R はリソースの有限集合、C は制御ノードの有限集合、→⊆(T×C)∪(C×T) は依存関係、 a:C{inputλ, par,join,choice,endchoice,output}(ただし、λ∈R+ ) は制御ノードの種類を返す関数、c:TR+は各タスクの最悪実行時間を返す関数、d:TR+ は各タスクの相対デッドラインを返す関数、rr: T2^R は各タスクの実行に必要なリソースの集合を返す関数、sc : R{FIFO、FPγ} は各リソースのスケジューリング方式、γ:TN は各タスクへの優先度割り当て関数である。
【００３０】
N=C∪T とし、n∈N を複数タスク動作仕様TGのノードと呼ぶ。G = (N,→) はDAG(閉路の無い有向グラフ) となっているものとする。n1, n2∈Nのとき、(n1, n2)∈→をn1→n2 と書き、n1はn2 に先行する、n2はn1 に後続すると呼ぶことにする。
表１に複数タスク動作仕様における制御ノードの動作意味を表し、図２に複数タスク動作仕様の例を示す。
【表１】
2013171353.tif 000003
【００３１】
複数タスク動作仕様からPrSwPNへの変換
非特許文献５に示される手法に従い、与えられた複数タスク動作仕様 TGから、TGの各動作（任意のタスク τiのリリース、実行開始、実行中断、実行再開、実行終了、リソースの獲得・解放）の実行系列の集合（時間付きトレース集合）と、対応するトランジションの実行時刻も含めた発火系列の集合が等しいようなPrSwPNに変換する。この変換は、まず、タスク、スケジューラなどのシステムの構成要素それぞれに対して、対応するPrSwPNによる部分モデルを構成し、それらを結合することにより行っている。
【００３２】
部分モデルの例として、図３に、PrSwPNで表したタスクを示す。タスクの起動が要求されると、まず起動要求プレースに（外部から）トークンが置かれ、それにより起動トランジションが直ちに発火し、リソース要求プレースおよび起動中プレースにトークンが移動する。リソース要求プレースにトークンが置かれると、スケジューラモジュールは他のタスクからの当該リソース要求を適切に調停し、リソースを獲得できたらならば実行可能プレースおよびリソース獲得中プレースにトークンを移動させる。リソースを獲得しタスクを実行開始してから最悪実行時間（＝タイムバジェット）経過後に、実行完了トランジションが発火し、トークンがリソース返還プレースおよび次状態プレースに移動して実行終了となる。
【００３３】
実行中に他のタスクから横取り（プリエンプション）があった場合、スケジューラモジュールによってリソース獲得中プレースからトークンが引き去られ、ストップウォッチアークにより実行完了トランジションの時間計測が停止する。なお、起動中プレースにトークンが置かれてからの経過時間をデッドライントランジションが計測しており、デッドラインを超過するとデッドライン超過トランジションが発火し、エラー状態（タスク失敗）となる。
【００３４】
スループット検証
性能検証の手法として、性能検証モデルに対しスループット検証を行う。スループット要求が満たされていない状態を検出するアサーションを性能検証モデルに追加してスループットを検証する。入力が入ってくるプレースに対して2個以上トークンがたまるとエラー状態になるようなアサーションをつける。
【００３５】
具体例を図４に示す。errorプレースは、エラーの状態を表すプレースで、トークンがある場合、現在エラーであることを示す。assertionトランジションはエラー処理を行うトランジションを表している。この例では、p0プレースにinputトランジションから100msごとにトークンが入ってくる。つまり、スループットは10単位データ/秒である。もしp0プレースにトークンが2つ以上たまれば、100ms以内に処理できていないことになる。その場合assertionトランジションが即座に発火し、errorプレースにトークンが移動する。
【００３６】
入力から出力までの最悪応答時間（＝最悪レイテンシ）を求めることで、得られたレイテンシ要求に対する余裕時間を各タスクのタイムバジェットに配分する。配分は、同じリソースを共有するタスクのタイムバジェットを同じ倍率増加させることで行う。最適化は、すべてのタスクのタイムバジェットの合計が最大になるような倍率の組み合わせを求めることで行う。
【００３７】
最悪レイテンシの計測
非特許文献５に示されるタスクからPrSwPNへの変換手法に、入力から出力までの処理(以下、パスと呼ぶ)にかかる最悪の場合の時間（最悪レイテンシ）を計測するためのプレースとトランジションの組を追加する。システムに入力が入ると計測を開始し、システムから出力があると計測を停止する。モデルの例を図５に示す。この例においては、単位時間は秒とし、システムのレイテンシ要求は6秒とする。簡単のためシステム内部のプレース、トランジションは省略している。システムへの入力プレースにトークンが到着すると、計測可能プレースにトークンが移動する。計測可能プレースにトークンがある場合、1秒経過毎に1秒経過トランジション、2秒経過トランジションの順に順次発火する。6秒経過トランジションが発火する前にシステムが出力プレースにトークンを出力すると、計測可能プレースからトークンが奪われ、計測が中断される。このとき、k秒経過トランジション(k=1,…,6)のうち、一度も発火していない最小のkを最悪レイテンシと計測される。そのようなkが存在しない、すなわち、6秒経過トランジションが発火した場合、レイテンシ要求違反プレースにトークンが移動し、レイテンシ要求違反を検出する。
【００３８】
系内に入力が複数滞留する場合のレイテンシ要求検証
スループット要求の逆数、すなわち、入力の到着間隔がレイテンシ要求より小さい場合、一般に複数の入力が系内に滞留するため、それぞれの入力に対してレイテンシ要求を検証する必要がある。この場合に対応するため、レイテンシ要求のアサーション部を複数個用意する。モデルの例を図６に示す。レイテンシ要求をpd[単位時間]、スループット要求をλ[入力/単位時間]とすると、系内に滞留する入力の数は最大pd×λであるため、レイテンシ要求のアサーションは pd×λ個必要となる。最悪レイテンシの計測部も同様に複数用意する。
【００３９】
タイムバジェット最適化装置の構成
図７において、１は、データを入力するキーボード等の入力手段、２は、入力データを複数タスク動作仕様Aから優先権付きストップウォッチペトリネットBに変換する第１変換手段、３は、モデルチェッカを用いてストップウォッチペトリネットBを検証する第１検証手段、４は、ストップウォッチペトリネットBが性能要求を満たすか否か判定する第１判定手段、５は、第１判定手段４により、ストップウォッチペトリネットBが性能要求を満たさずと判定されたとき、複数タスク動作仕様A は改善不能と出力する第１出力手段、６は、第１判定手段４により、ストップウォッチペトリネットBが性能要求を満たすと判定されたとき、複数タスク動作仕様Aの任意のリソースriについて、リソースriを使用する全タスクのタイムバジェットを一定割合増加させた複数タスク動作仕様Aiを求める演算手段、７は、複数タスク動作仕様Aiをそれぞれ優先権付きストップウォッチペトリネットBiに変換する第２変換手段、８は、モデルチェッカを用いて、各優先権付きストップウォッチペトリネットBiを検証する第２検証手段、９は、性能要求を満たす各優先権付きストップウォッチペトリネットBiが存在するか否か判定する第２判定手段、１０は、第２判定手段９により、性能要求を満たす各優先権付きストップウォッチペトリネットBiが存在せずと判定されたとき、複数タスク動作仕様A を改善された複数タスク動作仕様として出力する第２出力手段、１１は、第２判定手段９により、性能要求を満たす各優先権付きストップウォッチペトリネットBiが存在すると判定されたとき、性能要求を満たした各優先権付きストップウォッチペトリネットBiのうち、最も最悪レイテンシが小さい優先権付きストップウォッチペトリネットBiに対応する複数タスク動作仕様Aiを、複数タスク動作仕様Aとして選択するとともに複数タスク動作仕様Aを演算手段に入力する選択手段である。これらの各構成部分は、コンピュータにて構成される。なお、第１及び第２出力手段５、１０は、１つの出力手段、例えばモニタ、プリンタ等を使用することができる。
【００４０】
タイムバジェット最適化方法
図８に示すように、本実施形態にかかるタイムバジェット最適化方法は下のステップよりなる。
ステップS1：入力されたデータを、複数タスク動作仕様Aから優先権付きストップウォッチペトリネットBに変換する第１変換ステップ、
ステップS2：モデルチェッカを用いてストップウォッチペトリネットBを検証する第１検証ステップ、
ステップS3：ストップウォッチペトリネットBが性能要求を満たすか否か判定する第１判定ステップ、
ステップS4：第１判定ステップにより、ストップウォッチペトリネットBが性能要求を満たさずと判定されたとき、複数タスク動作仕様A は改善不能と出力する第１出力ステップ、
ステップS5：第１判定ステップにより、ストップウォッチペトリネットBが性能要求を満たすと判定されたとき、複数タスク動作仕様Aの任意のリソースriについて、リソースriを使用する全タスクのタイムバジェットを一定割合増加させた複数タスク動作仕様Aiを求める演算ステップ、
ステップS6：複数タスク動作仕様Aiをそれぞれ優先権付きストップウォッチペトリネットBiに変換する第２変換ステップ、
ステップS7：モデルチェッカを用いて、各優先権付きストップウォッチペトリネットBiを検証する第２検証ステップ、
ステップS8：性能要求を満たす各優先権付きストップウォッチペトリネットBiが存在するか否か判定する第２判定ステップ、
ステップS9：第２判定ステップS8により、性能要求を満たす各優先権付きストップウォッチペトリネットBiが存在せずと判定されたとき、複数タスク動作仕様A を改善された複数タスク動作仕様として出力する第２出力ステップ、
ステップS10：第２判定ステップS8により、性能要求を満たす前記各優先権付きストップウォッチペトリネットBiが存在すると判定されたとき、性能要求を満たした各優先権付きストップウォッチペトリネットBiのうち最も最悪レイテンシが小さい各優先権付きストップウォッチペトリネットBiに対応する複数タスク動作仕様Aiを、複数タスク動作仕様Aとして選択するとともに該複数タスク動作仕様Aを演算手段に入力する選択ステップ。
【００４１】
複数タスク動作仕様の最適化
最適化は、すべてのタスクのタイムバジェットの合計が最大になるような組み合わせを求めることで行う。同じリソースを共有するタスク群のうち、一部のタスクのみのタイムバジェットを増やすと、増やさなかったタスクがリソースをとることが難しくなり、リソース共有の飢餓状態が発生する恐れがある。そのため、同じリソースを共有するタスクのタイムバジェットを同じ倍率で増加させる。以下に最適化の手順を示す。
【００４２】
ここで、 fはタイムバジェットを増加させる割合（増加率）、 WCL(TG)は複数タスク動作仕様TGの最悪レイテンシとする。
【００４３】
1.複数タスク動作仕様TGを入力する。
2.TGを性能検証モデルに変換し、変換したモデルに対し性能検証を行う。
3.2.において、もしTGが性能要求を満たさないならば、TGは改善不能である旨出力する。
4.TGのすべてのリソースri∈Rにおいて、riを共有するタスクtij∈Tのタイムバジェットc(tij)をc’(tij)に置き換えたものを複数タスク動作仕様TGiとする。c’(tij)は以下のように求める。
【数１】
2013171353.tif 000004
【００４４】
5.すべてのTGiを性能検証モデルに変換し、変換したモデルに対し性能検証を行い、 WCL(TGi)を求める。
6.5．において、もしすべてのTGiが性能要求を満たさないならば、8．に移る。
7.すべての TGi のうちWCL(TGi)が最小の値となるTGiを、更新された複数タスク動作仕様TGとし、1．に戻る。
8.現在の複数タスク動作仕様TGを出力する。
【００４５】
一般に、タスクのタイムバジェットを増やすと、その分リソースを使用する時間が増えるので、ほかのタスクのリソース使用時間を圧迫してしまう。4．において、最悪レイテンシが最小になるようなTGを選択しているのは、タイムバジェット増加による他のタスクへの影響が最も少ないと考えられるためである。
【００４６】
実験
図２の例について、性能検証モデルへの変換を行い、そのモデルに対し性能検証を行った。また、検証結果をもとにモデルの最適化を行った。なお、スループット要求は10[入力/s]、レイテンシ要求は200[ms]、増加率fは0．5[%]とする。
【００４７】
検証環境
検証にはPrSwPN検証ツールTINA（非特許文献６）を用いる。TINAはPrSwPNをグラフィカルに描写することができ、作成したPrSwPNをテキストファイルに変換することもできる。ランダムシミュレータでは、トランジションの発火時間をランダムに選んで、解析を行う。到達可能性解析では、すべてのマーキングを調べ、PrSwPNがデッドロックかどうかを解析することができる。つまり、TINAはデッドロックの検証を行う機能を持っている。
【００４８】
検証結果
最適化前、最適化後それぞれについての性能検証結果と各タスクのタイムバジェットを表２（最適化前後の性能検証結果を示す表）及び表３（最適化前後の各タスクのタイムバジェットを示す表）に示す。
【表２】
2013171353.tif 000005
【表３】
2013171353.tif 000006
【００４９】
本発明によれば、resource1、resource2を共有するタスクのタイムバジェットをそれぞれ146.0％、39.5％増加させても、最適化前と同性能のモデルを得ることができた。先行研究（非特許文献５）に示される変換手法で同モデルを変換した場合、状態数は100程度であったが、本発明では、最悪レイテンシの計測を行うプレースとトランジションの組を追加したことによりトークンの移動が複雑になったため、状態数が増大したものと考えられる。しかし、それでも数秒程度で検証が完了している。従って、本発明で扱った例の規模であれば、性能検証、および、タイムバジェットの最適化が行えるといえる。
【産業上の利用可能性】
【００５０】
本発明は、性能とリソースの制約が共に厳しく、高い信頼性を要求される組込みソフトウェア開発において、特に有用であり、設計モデルの段階で時間制約やリソース制約を考慮した最悪時の性能検証を行うことができる。
【符号の説明】
【００５１】
１         入力手段
２、７      第１、第２変換手段
３、８      第１、第２検証手段
４、９      第１、第２判定手段
５、１０      第１、第２出力手段
６        演算手段
１１         選択手段  
【図１】
2013171353.tif 000007
【図２】
2013171353.tif 000008
【図３】
2013171353.tif 000009
【図４】
2013171353.tif 000010
【図５】
2013171353.tif 000011
【図６】
2013171353.tif 000012
【図７】
2013171353.tif 000013
【図８】
2013171353.tif 000014