The workflow is a semi-automated approach for determining whether a system model conforms to a given set of requirements. It supports both verification and falsification of the given system model w.r.t. requirements. Falsification is conducted by Monte-Carlo simulation runs, while verification is essentially symbolic simulation of the system model using Affine arithmetic. System model and requirement monitors are expected to be provided as C++ code. This enables analysis throughout the design cycle (even when moving to implementation). There is support for automatic generation of C++ code from parametrized requirement / system templates. Once the system model and requirements are provided, depending on the choice (verification or falsification) made by the user (via the configuration file), the appropriate algorithm is run, generating a report with analysis results.

The workflow has three inputs: System Model, Requirements, and Configuration. There is also one output: Analysis Report.

The main activities included in the workflow are:

• Parse Configuration: Reads set of YAML configuration files containing information such as whether to perform verification or falsification, whether to plot the results, etc.
• Translate Model: Generates C++ code representing the system model based on a parametrized template and a YAML file containing specific values for parameters. (Note: system template has to be created manually).
• Translate Requirements: Generates C++ code representing the system requirements based on parametrized templates and a YAML file containing specific values for parameters. (Note: requirement templates have to be created manually).
• Falsification: Performs Monte Carlo simulation runs.
• Verification: Performs reachability-analysis-based verification for safety-critical hybrid systems (through Affine Arithmetic).
• Generate Report: Creates textual report based on system analysis results. Optionally, includes plots.