|
Oris is a tool for qualitative verification and quantitative evaluation of reactive timed systems [QEST06][QEST04].
Oris supports modeling based on various classes of timed extensions of Petri Nets:
- Time Petri Nets (TPN): the classical model of [TSE01].
- communicating Time Petri Nets (cmTPN): a modular extension of Time Petri Nets [TSE95]. The model is not supported in the current baseline of the tool.
- preemptive Time Petri Nets (pTPN): an extension of Time Petri Nets supporting representation of suspension in a manner that can compare against stopwatch automata, which can
be applied to the representation of preemptive systems [TSE04][Ada08][ECRTS07][ETFA07][ECRTS03].
- stochastic preemptive Time Petri Nets (spTPN): a discrete time variant, based on a maximal step semantics of concurrency, with preemption and quantitative probabilities
associated with timers and switches [TSE05].
- stochastic Time Petri Nets (sTPN): a kind of non-Markovian Stochastic Petri Net obtained by extending (continuous time) Time Petri Nets with a stochastic
characterization of time distributions and choices [TSE09-2][TSE09][QEST08][QEST07][QEST05].
As salient a core capability, the ORIS tool supports a suite of qualitative and quantitative analysis techniques based on symbolic state space enumeration:
- for Time Petri Nets: state space analysis through symbolic coverage based on DBM state classes. The analysis includes also a technique for the evaluation of a tight
profile of timings accepted by a symbolic run [TSE01].
- for communicating Time Petri Nets: a technique for compositional analysis. The symbolic state space of each module is enumerated
separately under the assumption of a required interface; state spaces of individual modules can be integrated to obtain the state space of the overall model; the assumptions made on required interfaces are
verified during the integration; projections on the state spaces of individual modules before integration enable a containment of the state space explosion in the overall integrated model [TSE95]. This feature
is not supported in the current baseline of the tool.
- for preemptive Time Petri Nets, the analysis relies on the over-approximation of state space through tight DBM classes and a clean-up algorithm for the identification of false
behaviors and for the tight refinement of the timing profile of any selected symbolic run [TSE04].
- for stochastic preemptive Time Petri Nets: state space analysis with construction and solution of of the underlying Discrete Time Markov Chain.
- for stochastic Time Petri Nets: quantitative evaluation based on the theory of stochastic state classes, evaluation of the probability of selected symbolic runs and steady
state analysis for regenerative classes based on Markov Renewal Theory. A closed form calculus supports efficient analysis for the class of models with transitions associated with timings that are: immediate,
deterministic, expolynomial [TSE09-2][QEST07].
An approximate analysis is developed for models where all transitions with infinite support are exponential: under this assumption multivariate distributions
associated with state classes are approximated through Bernstein Polynomials, enabling the analysis of models where enumeration of the state space is unfeasible due to practical factors of explosion or to the
presence of cycles with overlapping activity of non-Markovian transitions [TSE09].
The Oris tool also includes various additional components with specific purposes:
- for each model: timed and stochastic simulation in offline mode or with interactive token game [QEST06]. The module was recently extended to support also
stochastic simulation; however, the extension was instrumental to an internal experimentation and is presently limited to models with uniform and exponential distributions.
- for each model: a model checker for real time temporal logic formulae (state and action based, with timing constraints on temporal operators)
[QEST06]. As special features: the model checker identifies all the witnesses that satisfy the formula; and the formulae can be expressed using a visual formalism [JVLC01][TACAS98].
- a visual interface for the automated generation of preemptive Time Petri Nets from timeline schema of real time task sets [QEST06].
- a module for automated generation of code running under Linux-RTAI Real Time operating system [Ada08][RSP09].
- various components supporting test case selection, test sensitization, and coverage analysis in real time testing
[ECRTS07][ETFA07][Ada08][RSP09].
|
