Welcome to PyCASSE, a Python Contract-based Analysis for Stochastic Systems Exploration Toolbox. PyCASSE enables automated reasoning with assume-guarantee (A/G) contracts expressed in Signal Temporal Logic (STL) and Stochastic Signal Temporal Logic (StSTL).

To cite PyCASSE in an academic work, please use the following bibtex entry:

@inproceedings{Oh22,
   author = {Oh, Chanwook and Lora, Michele and Nuzzo, Pierluigi},
   title = {Quantitative verification and design space exploration under uncertainty with parametric stochastic contracts},
   year = {2022},
   booktitle = {Proceedings of the 41th International Conference on Computer-Aided Design},
   location = {San Diego, CA, USA},
   series = {ICCAD '22}
}

• 1. Installing PyCASSE
  • 1.1. Pre-requisites
  • 1.2. Optimization Solver
  • 1.3. PyCASSE
• 2. Writing Specifications for PyCASSE
  • 2.1. PyCASSE Syntax
• 3. Assume-Guarantee (A/G) Contracts
  • 3.1. What is an A/G Contract?
  • 3.2. A/G Contracts in PyCASSE
  • 3.3. A/G Contracts Operations
  • 3.4. A/G Contracts Operations in PyCASSE
• 4. Control Synthesis with A/G Contract
  • 4.1. Control Synthesis with STL A/G Contract in PyCASSE
  • 4.2. Control Synthesis with StSTL A/G Contract in PyCASSE
  • 4.3. PyCASSE MILPSolver Class
• 5. Parameter Synthesis with A/G Contract
  • 5.1. Parameterization of StSTL Formulas and Component Models
  • 5.2. Parameter Synthesis with PStSTL A/G Contract in PyCASSE
  • 5.3. PyCASSE Parameter Synthesis Functions
• 6. Examples
  • 6.1. Parameter Synthesis using StSTL Contracts (ICCAD 2022)
• 7. Bibiliography

Indices and tables

• Index
• Module Index
• Search Page