The ProFeat language

ProFeat provides a modeling language for describing families of stochastic systems. The ProFeat language extends the input language of the probabilistic model checker PRISM by feature-related concepts and meta-programming constructs.

A ProFeat model consists of two parts. The first part, the feature model, defines a set of features and specifies the allowed feature combinations. The second part describes the behavior of the individual features using feature modules. It optionally includes a feature controller, which specifies the dynamic feature switches.

Contents:

• Feature model
• Family definition
• Feature modules
• Dynamic feature switches
• Constants
• Global variables
• Formulas
• Expressions
• Costs and rewards
• Labels
• Multiple initial states
• Invariants
• Block syntax