このページの内容は最新ではありません。最新版の英語を参照するには、ここをクリックします。
デスクトップからローカルでホストされているサーバーへの Code Prover 解析の送信
Polyspace® 解析をデスクトップでローカルに実行したり、解析の負荷を 1 台以上の専用サーバーに移したりできます。このトピックでは、Polyspace 解析の負荷を移すための単純なサーバー/クライアント構成について説明します。この構成では、同じコンピューターが、Polyspace 解析を送信するクライアントおよび解析を実行するサーバーとして機能します。
このチュートリアルは、より複雑な構成に拡張できます。完全な設定とワークフローの手順については、下記の関連リンクを参照してください。
メモ
クライアント マシンとサーバー マシンの Polyspace のバージョンは一致している必要があります。
Bug Finder 解析を実行するためのクライアント/サーバー ワークフロー
初期設定の後、Polyspace 解析をクライアント デスクトップからサーバーに送信できます。クライアント/サーバー ワークフローは 3 つのステップで行われます。3 つのステップすべてが同じコンピューターで実行されるか、3 つの異なるコンピューターで実行されます。このチュートリアルでは、ワークフロー全体に対して同じコンピューターを使用します。
クライアント ノード:Polyspace 解析オプションを指定し、クライアント デスクトップで解析を開始します。コンパイルまでの解析の初期フェーズは、デスクトップ上で実行されます。コンパイル後、解析ジョブはサーバーに送信されます。
クライアント ノードとして機能するコンピューター上に Polyspace デスクトップ製品 Polyspace Bug Finder™ が必要です。
ヘッド ノード:サーバーはヘッド ノードと複数のワーカー ノードで構成されています。ヘッド ノードは、ジョブ スケジューラを使用して複数のクライアント デスクトップからの送信を管理します。ジョブはワーカー ノードが使用可能になると、ワーカー ノードに分散されます。
ヘッド ノードとして機能するコンピューター上に製品 MATLAB® Parallel Server™ が必要です。
ワーカー ノード:ワーカーが使用可能になると、ジョブ スケジューラが解析をそのワーカーに割り当てます。Polyspace 解析はワーカーで実行され、結果はレビューのために元のクライアント デスクトップにダウンロードされます。
ワーカー ノードとして機能するコンピューター上に製品 MATLAB Parallel Server が必要です。解析を実行するには、Polyspace サーバー製品 Polyspace Bug Finder Server™ および Polyspace Code Prover™ Server も必要です。
Install Products for Submitting Polyspace Analysis from Desktops to Remote Serverも参照してください。
前提条件
このチュートリアルでは、クライアントおよびサーバーとして同じコンピューターを使用します。コンピューターに以下をインストールしなければなりません。
クライアント側製品: Polyspace Bug Finder
サーバー側製品: MATLAB Parallel Server、Polyspace Bug Finder Server、および Polyspace Code Prover Server
詳細は、Install Products for Submitting Polyspace Analysis from Desktops to Remote Serverを参照してください。
コンピューターのホスト名を知っておかなければなりません。たとえば、Windows® では、コマンド ライン ターミナルを開いて、次のように入力します。
hostname
サーバーの構成と起動
以前のサービスの停止
あらかじめ MATLAB Parallel Server のサービスを開始していた場合、すべてのサービスを停止していることを確認します。特に、以下を行う必要がある可能性があります。
Windows の
C:\Windows\Temp
などの一時フォルダーをチェックして、MDCE
フォルダーが存在する場合は削除。すべてのサービスを明示的に停止。Linux® ではこの手順は不要。
コマンド ライン ターミナルを開きます。(
cd
を使用して)
に移動し、以下を入力します。matlabroot
\toolbox\parallel\binここで、mjs uninstall -clean
は MATLAB Parallel Server インストール フォルダーです。たとえば、matlabroot
C:\Program Files\MATLAB\R2025a
です。
初めてサービスを開始する場合は、これらの手順を実行する必要はありません。
mjs
サービス設定の構成
サービスを開始する前に、mjs
サービス設定を構成しなければなりません。
に移動します。ここで matlabroot
\toolbox\parallel\bin
は MATLAB Parallel Server インストール フォルダーです。たとえば、matlabroot
C:\Program Files\MATLAB\R2025a
です。以下の 2 つのファイルを変更します。これらのファイルを編集して保存するには、エディターを管理者モードで開かなければなりません。
mjs_def.bat
(Windows) またはmjs_def.sh
(Linux)ファイル内の説明を読み、必要に応じて行のコメントを解除します。少なくとも、以下の行のコメントは解除しなければならない場合があります。
ホスト名:
(Windows の場合) またはREM set HOSTNAME=myHostName
(Linux の場合)。#HOSTNAME=`hostname -f`
REM
または#
を削除し、コンピューターのホスト名を明示的に指定します。セキュリティ レベル:
(Windows の場合) またはREM set SECURITY_LEVEL=
(Linux の場合)。#SECURITY_LEVEL=""
REM
または#
を削除し、セキュリティ レベルを明示的に指定します。
そうしない場合、後でジョブ スケジューラを開始する際にエラーが発生する可能性があります。
mjs_polyspace.conf
Polyspace Server 製品のルートを参照する行を変更し、コメントを解除します。この行は、Polyspace サーバー製品インストールのリリース番号とルート フォルダーを参照する必要があります。たとえば、Polyspace Code Prover Server の R2025a リリースがルート フォルダー
C:\Program Files\Polyspace Server\R2025a
にインストールされている場合は、この行を次のように変更します。POLYSPACE_SERVER_ROOT=C:\Program Files\Polyspace Server\R2025a
そうしない場合、MATLAB Parallel Server インストールは、解析を実行する Polyspace Code Prover Server インストールを見つけることができません。
サービスの開始
mjs
サービスを開始し、現在のコンピューターをヘッド ノードとワーカー ノードの両方として割り当てます。
に移動します。ここで matlabroot
\toolbox\parallel\bin
は MATLAB Parallel Server インストール フォルダーです。たとえば、matlabroot
C:\Program Files\MATLAB\R2025a
です。以下のコマンドを (コマンド ラインで直接またはスクリプトを使用して) 実行します。
mjs install
mjs start
startjobmanager -name JobScheduler -remotehost hostname -v
startworker -jobmanagerhost hostname -jobmanager JobScheduler -remotehost hostname -v
hostname
はコンピューターのホスト名です。これは、ファイル mjs_def.bat
(Windows) または mjs_def.sh
(Linux) で指定したホスト名です。Linux の場合は、コマンド mjs install
は不要であることに注意してください。コマンド ラインの代わりに、管理センター インターフェイスからサービスを開始することもできます。Install Products for Submitting Polyspace Analysis from Desktops to Remote Serverを参照してください。
コマンドの詳細は、MATLAB ジョブ スケジューラを統合するための詳細オプションの設定 (MATLAB Parallel Server)を参照してください。
クライアントの設定
デスクトップ製品 Polyspace Bug Finder (または Polyspace Code Prover) のインターフェイスを開きます。
に移動します。ここで polyspaceroot
\polyspace\bin
は Polyspace デスクトップ製品のインストール フォルダーです。たとえば、polyspaceroot
C:\Program Files\Polyspace\R2025a
です。実行可能ファイル polyspace
をダブルクリックします。
[ツール] 、 [基本設定] を選択します。[サーバー設定] タブで、[ジョブ スケジューラのホスト名] にコンピューターのホスト名を入力します。
これでサーバー/クライアント ワークフローの設定が完了しました。
クライアントからサーバーへの解析の送信
インストールで提供されるファイル example.c
に対して Code Prover を実行します。
以下の手順を実行する前に、Polyspace の実行可能ファイルへの絶対パスを入力しなくてもよいように、パス
をオペレーティング システムの環境変数 polyspaceroot
\polyspace\binPATH
に追加します。ここで、
は Polyspace デスクトップ製品のインストール フォルダーです。たとえば、polyspaceroot
C:\Program Files\Polyspace\R2025a
です。パスが既に追加されているかどうかをチェックするには、コマンド ライン ターミナルを開いて、次のように入力します。
polyspace-code-prover -h
ファイル
example.c
およびすべてのヘッダー ファイルを、
から書き込み権限のあるフォルダーにコピーします。polyspaceroot
\polyspace\examples\cxx\Code_Prover_Example\sourcesコマンド ターミナルを開きます。
example.c
を保存したフォルダーに移動し、以下を入力します。ここで、polyspace-code-prover -sources example.c -I . -main-generator -results-dir resultsFolder -batch -scheduler hostname
はコンピューターのホスト名です。Bug Finder 解析を実行する場合は、hostname
polyspace-code-prover
の代わりにpolyspace-bug-finder
を使用します。polyspace-code-prover
コマンドは、-batch
オプションを使用する場合、Polyspace Bug Finder ライセンスのみで実行できます。コンパイル後、解析はサーバーに送信され、ジョブ ID を返します。
現在のジョブのステータスを確認します。
ジョブ ID を使用して現在のジョブを見つけることができます。polyspace-jobs-manager listjobs -scheduler hostname
ジョブが完了したら、明示的に結果をダウンロードできます。
polyspace-jobs-manager download -job jobID -results-folder . -scheduler hostname
ここで、
は送信時に得られたジョブ ID です。jobID
結果フォルダーには、ダウンロードされた結果ファイル (拡張子 .pscp
) が格納されます。デスクトップ製品 Polyspace Bug Finder のユーザー インターフェイスで結果を開きます。