Skip to main content

Specification and verification of ROS-based robot software

Project description

rospec

ruff pytest

Description

rospec is a domain specification language to specify configurations of ROS components and their integration. Current approaches focus on runtime verification or require system execution to detect misconfigurations. rospec allows component writer developers to express specifications for their ROS components, while component integrators select their components and provide their configurations --- any mismatches are raised statically prior to execution. By providing a formal way to describe the expected configuration and integration of ROS components, rospec helps identify misconfigurations early in the development process, preventing costly errors during system execution.

The tool can be used to validate various aspects of ROS components configuration and integration, including but not only:

  • Topic, service, and action connections between nodes;
  • Parameter value constraints and dependencies;
  • Component compatibility requirements.

Installation

rospec can be installed using either pip or by building from source. We recommend using a virtual environment to avoid conflicts with other Python packages.

Prerequisites

Setup

Option 1: Install from PyPI (when available)

# Create and activate a virtual environment
uv venv
source .venv/bin/activate  # On Windows: .venv\Scripts\activate

# Install rospec
uv add rospec

Option 2: Install from source

  1. Clone the repository:

    git clone https://github.com/pcanelas/rospec.git
    cd rospec
    
  2. Create a virtual environment and install dependencies:

    uv venv
    source .venv/bin/activate  # On Windows: .venv\Scripts\activate
    uv sync
    
  3. Install in development mode (if you plan to contribute):

    uv sync --dev
    

Usage

rospec offers a command line interface (CLI) for parsing and verifying specifications. To run the CLI, you can use the following command:

rospec --specifications path/to/your/spec.rospec

Or if installed in development mode:

uv run rospec --specifications path/to/your/spec.rospec

Basic Example

Here's a simple example of a rospec specification containing the specification for one component and its integration:

node type move_group_type {
   param elbow_joint/max_acceleration: double where {_ >= 0};
   optional param elbow_joint/max_velocity: double = 2.0;
   optional param elbow_joint/has_velocity_limits: bool = false;
   optional param elbow_joint/has_acceleration_limits: bool = false;
} where {
    exists(elbow_joint/max_acceleration) -> elbow_joint/has_acceleration_limits;
}

system {
   node instance move_group: move_group_type {
       param elbow_joint/max_acceleration = 0;
       param elbow_joint/max_velocity = 3.14;
       param elbow_joint/has_acceleration_limits = false;
       param elbow_joint/has_velocity_limits = false;
   }
}

To verify this specification:

rospec --specifications examples/evaluation/detectable-364801.rospec

Development

For development setup and contribution guidelines, see CONTRIBUTING.md.

Quick Development Setup

git clone https://github.com/pcanelas/rospec.git
cd rospec
uv venv
source .venv/bin/activate  # On Windows: .venv\Scripts\activate
uv sync --dev
uv run pre-commit install

Running Tests

uv run pytest

Code Formatting

uv run ruff format
uv run ruff check --fix

Authors

This project is a research project within the Software and Societal Systems Department (S3D) and the Robotics Institute at Carnegie Mellon University, and LASIGE at University of Lisbon, by:

Acknowledgements

This work was supported by Fundação para a Ciência e Tecnologia (FCT) in the LASIGE Research Unit under the ref. (UID/00408/2025 and EXPL/CCI-COM/1306/2021), and the CMU Portugal Dual PhD program (SFRH/BD/151469/2021).

Publications

The Usability Argument for ROS-based Robot Architectural Description Languages, at PLATEAU 2025.

Understanding Misconfigurations in ROS: An Empirical Study and Current Approaches, at ISSTA 2024.

Project details


Download files

Download the file for your platform. If you're not sure which to choose, learn more about installing packages.

Source Distribution

rospec-0.0.3.tar.gz (98.4 kB view details)

Uploaded Source

Built Distribution

If you're not sure about the file name format, learn more about wheel file names.

rospec-0.0.3-py3-none-any.whl (44.2 kB view details)

Uploaded Python 3

File details

Details for the file rospec-0.0.3.tar.gz.

File metadata

  • Download URL: rospec-0.0.3.tar.gz
  • Upload date:
  • Size: 98.4 kB
  • Tags: Source
  • Uploaded using Trusted Publishing? No
  • Uploaded via: twine/6.1.0 CPython/3.13.3

File hashes

Hashes for rospec-0.0.3.tar.gz
Algorithm Hash digest
SHA256 82ab65470e8d0919a5bf1a917e3067a9eacd3c97e59b1148b1431b4d1774af9b
MD5 2e0e0b334376b7cd107e3746958453a5
BLAKE2b-256 ab319adb59b1bf519f19acd00a2a461f7abe10775c0110eef9e4ae97bf704117

See more details on using hashes here.

File details

Details for the file rospec-0.0.3-py3-none-any.whl.

File metadata

  • Download URL: rospec-0.0.3-py3-none-any.whl
  • Upload date:
  • Size: 44.2 kB
  • Tags: Python 3
  • Uploaded using Trusted Publishing? No
  • Uploaded via: twine/6.1.0 CPython/3.13.3

File hashes

Hashes for rospec-0.0.3-py3-none-any.whl
Algorithm Hash digest
SHA256 3fb4794fde0712a59d5e62c89039ad22a0184e5b50d4847345f208a2bc7e4f41
MD5 1f26880aca1ec1ebbb94be07c798906a
BLAKE2b-256 8faf7f8821766c7739333726d9e98f87774e803255a17d743296e423cad8dc9f

See more details on using hashes here.

Supported by

AWS Cloud computing and Security Sponsor Datadog Monitoring Depot Continuous Integration Fastly CDN Google Download Analytics Pingdom Monitoring Sentry Error logging StatusPage Status page