本页翻译不是最新的。点击此处可查看最新英文版本。

将 Code Prover 分析从桌面端发送到本地托管的服务器端

您可以在桌面端执行本地 Polyspace® 分析，也可以将分析负载转移到一台或多台专用服务器。本主题展示一个用于转移 Polyspace 分析负载的简单服务器-客户端配置。在此配置中，同一计算机既充当提交 Polyspace 分析的客户端，又充当运行分析的服务器。

您可以对本教程进行扩展，以进行更复杂的配置。有关完整的设置和工作流说明，请参阅下面的相关链接。

注意

客户端计算机和服务器计算机上的 Polyspace 版本必须一致。

用于运行 Bug Finder 分析的客户端-服务器工作流

进行初始设置后，您可以将 Polyspace 分析从客户端桌面提交到服务器端。客户端-服务器工作流分为三个步骤。所有三个步骤可以在同一台计算机上执行，也可以在三台不同的计算机上执行。本教程使用同一台计算机执行整个工作流。

  1. 客户端节点：您需要在客户端桌面指定 Polyspace 分析选项并启动分析。分析的初始阶段（直到编译）在桌面端运行。在编译后，分析作业将提交到服务器。

    在充当客户端节点的计算机上，需要具有 Polyspace 桌面端产品 Polyspace Bug Finder™。

  2. 主节点：服务器由一个主节点和多个工作节点构成。主节点使用作业调度器管理来自多个客户端桌面的提交。然后，作业将被分发给可用的工作节点。

    在充当主节点的计算机上，需要具有 MATLAB® Parallel Server™ 产品。

  3. 工作节点：当某个工作进程可用时，作业调度器会将分析指定给该工作进程。Polyspace 分析将在该工作进程上运行，并且结果将下载回客户端桌面供审查。

    在充当工作节点的计算机上，需要具有 MATLAB Parallel Server 产品。您还需要具有 Polyspace 服务器端产品 Polyspace Bug Finder Server™ 和 Polyspace Code Prover™ Server 才能运行分析。

Flow diagram of a typical workflow for submitting analysis jobs from a client to a server.

另请参阅安装用于将 Polyspace 分析从桌面端提交到远程服务器端的产品。

前提条件

本教程使用同一台计算机作为客户端和服务器。您必须在计算机上安装以下产品：

  • 客户端产品：Polyspace Bug Finder

  • 服务器端产品：MATLAB Parallel Server、Polyspace Bug Finder Server 和 Polyspace Code Prover Server。

有关详细信息，请参阅安装用于将 Polyspace 分析从桌面端提交到远程服务器端的产品。

您必须知道您的计算机的主机名。例如，在 Windows® 中，打开一个命令行终端并输入以下命令：

hostname

配置和启动服务器

停止先前的服务

如果您先前已启动 MATLAB Parallel Server 的服务，请确保已停止所有服务。尤其需要指出的是，您必须：

  • 检查临时文件夹，例如 Windows 中的 C:\Windows\Temp，并删除其中的 MDCE 文件夹（如果存在）。

  • 显式停止所有服务。在 Linux® 中不需要执行此步骤。

    打开一个命令行终端。导航到 matlabroot\toolbox\parallel\bin（使用 cd）并输入以下命令：

    mjs uninstall -clean
    其中，matlabroot 是 MATLAB Parallel Server 的安装文件夹，例如 C:\Program Files\MATLAB\R2024b。

如果这是您第一次启动服务，则不必执行这些步骤。

配置 mjs 服务设置

在启动服务之前，您必须配置 mjs 服务设置。导航到 matlabroot\toolbox\parallel\bin，其中，matlabroot 是 MATLAB Parallel Server 的安装文件夹，例如 C:\Program Files\MATLAB\R2024b。修改以下两个文件。要编辑并保存这些文件，必须在管理员模式下打开编辑器。

  • mjs_def.bat (Windows) 或 mjs_def.sh (Linux)

    阅读文件中的说明并根据需要取消注释某些行。您可能至少要取消注释下面这些行：

    • 主机名： 

      REM set HOSTNAME=myHostName
      （在 Windows 中）或
      #HOSTNAME=`hostname -f`
      （在 Linux 中）。删除 REM 或 # 并显式指定您的计算机主机名。

    • 安全级别：

      REM set SECURITY_LEVEL=
      （在 Windows 中）或
      #SECURITY_LEVEL=""
      （在 Linux 中）。删除 REM 或 # 并显式指定一个安全级别。

    否则，稍后在启动作业调度器时可能会出现错误。

  • mjs_polyspace.conf

    对指示 Polyspace 服务器端产品根目录的行进行修改并取消注释。该行应当指示您安装的 Polyspace 服务器产品的版本号和根文件夹。例如，如果已在根文件夹 C:\Program Files\Polyspace Server\R2024b 中安装 R2024b 版本的 Polyspace Code Prover Server，请将该行修改为：

    POLYSPACE_SERVER_ROOT=C:\Program Files\Polyspace Server\R2024b

    否则，所安装的 MATLAB Parallel Server 将无法找到安装的 Polyspace Code Prover Server 来运行分析。

启动服务

启动 mjs 服务，并将当前计算机同时指定为主节点和工作节点。

导航到 matlabroot\toolbox\parallel\bin，其中，matlabroot 是 MATLAB Parallel Server 的安装文件夹，例如 C:\Program Files\MATLAB\R2024b。运行以下命令（可以直接从命令行运行，也可以使用脚本）：

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 命令。

除了使用命令行之外，还可以从 Admin Center 界面启动服务。请参阅安装用于将 Polyspace 分析从桌面端提交到远程服务器端的产品。

有关命令的详细信息，请参阅配置 MATLAB 作业调度器集成的高级选项 (MATLAB Parallel Server)。

配置客户端

打开 Polyspace Bug Finder（或 Polyspace Code Prover）桌面端产品的用户界面。导航到 polyspaceroot\polyspace\bin（其中，polyspaceroot 是 Polyspace 桌面端产品的安装文件夹，例如 C:\Program Files\Polyspace\R2024b），然后双击 polyspace 可执行文件。

选择工具 > 预设项。在服务器配置选项卡上，在作业调度器主机名选项中输入您计算机的主机名。

Example server configuration in Polyspace Preferences.

现在，您的服务器-客户端工作流便设置好了。

将分析从客户端发送到服务器

对随安装提供的 example.c 文件运行 Code Prover。

在运行这些步骤之前，为免于输入 Polyspace 可执行文件的完整路径，请将路径 polyspaceroot\polyspace\bin 添加到您的操作系统上的 PATH 环境变量中。其中，polyspaceroot 是 Polyspace 桌面端产品的安装文件夹，例如 C:\Program Files\Polyspace\R2024b。要检查是否已添加该路径，请打开一个命令行终端并输入：

polyspace-code-prover -h
如果已添加该命令的路径，则会看到完整的选项列表。

  1. 将文件 example.c 和所有头文件从 polyspaceroot\polyspace\examples\cxx\Code_Prover_Example\sources 复制到一个您有写权限的文件夹。

  2. 打开一个命令行终端。导航到保存 example.c 的文件夹并输入以下命令：

    polyspace-code-prover -sources example.c -I . -main-generator -results-dir resultsFolder -batch -scheduler hostname
    其中，hostname 是您的计算机的主机名。要运行 Bug Finder 分析，请使用 polyspace-bug-finder，而不是 polyspace-code-prover。请注意：如果使用 -batch 选项，则只能使用 Polyspace Bug Finder 许可证运行 polyspace-code-prover 命令。

    在编译后，会将分析提交到服务器并返回一个作业 ID。

  3. 查看当前作业的状态。

    polyspace-jobs-manager listjobs -scheduler hostname
    可以使用作业 ID 来定位当前作业。

  4. 在作业完成后，您可以显式下载结果。

    polyspace-jobs-manager download -job jobID -results-folder . -scheduler hostname

    其中，jobID 是来自提交的作业 ID。

结果文件夹包含已下载的结果文件（扩展名为 .pscp）。在 Polyspace Bug Finder 桌面端产品的用户界面中打开结果。

另请参阅

主题