ProFeat documentation

Welcome to the ProFeat documentation.

ProFeat is a tool for the analysis of stochastic system families. It provides a modeling language that extends the input language of the probabilistic model checker PRISM by feature-oriented concepts, including support for dynamic feature switches, multi-features and feature attributes.

ProFeat follows a translational approach for the quantitative analysis of system families. A ProFeat family model is translated into the input language of PRISM. Then, the actual analysis is performed by invoking PRISM on the translated models. The output generated by PRISM is then post-processed and ProFeat presents the results for each family member in a feature-aware fashion.

Contents:

• Installation
  • Prerequisites
  • Building from source
• Running ProFeat
  • Basic usage
  • Options
• The ProFeat language
  • Feature model
  • Family definition
  • Feature modules
  • Dynamic feature switches
  • Constants
  • Global variables
  • Formulas
  • Expressions
  • Costs and rewards
  • Labels
  • Multiple initial states
  • Invariants
  • Block syntax
• Property specification