Features.Home History

Hide minor edits - Show changes to output - Cancel

Added line 40:
** TFPG Filtering
Added lines 28-31:
* Common Cause Analysis (CCA)
** Definition of Common Causes
** Fault Tree Analysis with Common Causes

Deleted lines 39-42:

* Common Cause Analysis (CCA)
** Definition of Common Causes
** Fault Tree Analysis with Common Causes
Added lines 41-44:
* Fault Detection and Isolation (FDI)
** Diagnosability Analysis
** Generation of minimum observables set
** Synthesis of diagnoser
Added lines 32-35:
** TFPG tightening
** TFPG possibility, necessity, consistency and activability
** TFPG refinement
** TFPG diagnosis
Changed line 4 from:
%rfloat height=100px% {$TopLevelUrl}/images/uc.gif
to:
(:comment %rfloat height=100px% {$TopLevelUrl}/images/uc.gif :)
Added lines 32-36:

* Common Cause Analysis (CCA)
** Definition of Common Causes
** Fault Tree Analysis with Common Causes

Added line 22:
** Monotonic and non-monotonic FTA
Changed lines 8-9 from:
*
**
to:
* Library-based specification of faults
** Injection of faults retrieved from a fault library
** Local effects library
** Global dynamics library

* Automatic model-extension with fault specifications
** Injection of library-based fault definitions into nominal model
** Automatic generation of resulting extended model

* Fault Tree Analysis (FTA) and generation of Minimal Cut Sets (MCS) for dynamic systems
** BDD-based algorithms
** SAT-based algoritmhs
** SAT+BDD-based algorithms
** SMT-based algorithms

* Failure Modes and Effects Analysis (FMEA)
** BDD-based algorithms
** SMT-based algorithms

* Fault propagation analysis based on Timed Failure Propagation Graphs (TFPG)
** TFPG association with extended model
** TFPG behavioral validation
** TFPG synthesis
Changed lines 8-45 from:
* An extended language for synchronous systems
** support for the [[http://fmv.jku.at/aiger/|AIGER]] format
** new set of types, namely 'Integer' and 'Reals'


* New model checking algorithms for finite state systems
** Full support for PSL model checking
** Interpolation based invariant checking
*** CAV'03 Mc Millan's interpolation algorithm
*** Interpolation sequences algorithm
** IC3
** Guided reachability
*** Reachability analysis guided by a regular expression

* New model checking algorithms for infinite state systems
** SMT-based techniques
*** Bounded Model Checking
*** K-induction
*** Interpolation Based
*** IC3
** Abstraction based techniques
*** Counter-Example Guided Abstraction Refinement (CEGAR)
*** Refinement via Unsatisfiable Core and Interpolation
*** K-induction with implicit abstraction
*** IC3 with implicit abstraction

* An extended set of functionalities
** Explicit FSM view generation
*** Dump in .xmi format
*** Subject to predicate abstraction
** Model simplification and recoding techniques
*** Range Recoding
*** Free input propagation
** Discrete Requirements Analysis
*** Property satisfiability
*** Property entailment
*** Unsatisfiable core extraction
*** Property realizability
to:
*
**
November 05, 2013, at 03:01 PM by 192.168.156.46 -
Added lines 35-37:
** Explicit FSM view generation
*** Dump in .xmi format
*** Subject to predicate abstraction
November 05, 2013, at 02:59 PM by 192.168.156.46 -
Changed lines 12-15 from:
* Model simplification and recoding techniques
** Range Recoding
** Free input propagation

to:
Added lines 35-37:
** Model simplification and recoding techniques
*** Range Recoding
*** Free input propagation
November 05, 2013, at 02:58 PM by 192.168.156.46 -
Deleted lines 35-39:

(:comment Some less important details
** Abstraction via AllSMT, and in combiation with BDDs
*** Refinement via Unsatisfiable Core and Interpolation
)
November 05, 2013, at 02:57 PM by 192.168.156.46 -
Added line 9:
** support for the [[http://fmv.jku.at/aiger/|AIGER]] format
Changed lines 11-13 from:
** support for the [[http://fmv.jku.at/aiger/|AIGER]] format

* new advanced model checking algorithms for synchronous systems
to:

* Model simplification and recoding techniques
** Range Recoding
** Free input propagation

* New model checking algorithms for finite state
systems
Changed line 19 from:
*** [[http://www.kenmcmil.com/pubs/CAV03.pdf|CAV 2003]] Mc Millan algorithm
to:
*** CAV'03 Mc Millan's interpolation algorithm
Added line 21:
** IC3
Changed lines 24-26 from:
** Counter-Example Guided Abstraction Refinement (CEGAR)
*** Basic abstraction vial AllSMT
*** Advanced abstraction based on BDD and SMT
to:

* New model checking algorithms for infinite state systems
** SMT-based techniques
*** Bounded Model Checking
*** K-induction
*** Interpolation Based
*** IC3
** Abstraction based techniques
*** Counter-Example Guided Abstraction Refinement (CEGAR)
Changed lines 34-40 from:
** Infinite state model checking based on SMT techniques
*** Bounded Model Checking via SMT
*** Abstraction based
** Compositional reasoning techniques
** Model simplification and recoding techniques
*** Range Recoding
*** Free input propagation
to:
*** K-induction with implicit abstraction
*** IC3 with implicit abstraction

(:comment Some less important details
** Abstraction via AllSMT, and in combiation with BDDs
*** Refinement via Unsatisfiable Core and Interpolation
)

Changed line 47 from:
*** Property realizability
to:
*** Property realizability
October 31, 2013, at 03:45 PM by 192.168.156.43 -
Changed line 8 from:
* An extended language
to:
* An extended language for synchronous systems
Deleted line 9:
** new constructs to represent network of (hybrid-)automata (HyDi)
Changed lines 11-12 from:
* new advanced model checking algorithms
to:

* new advanced model checking algorithms for synchronous systems
Changed lines 31-32 from:
** Requirements Analysis
*** Hybrid and Discrete
to:
** Discrete Requirements Analysis
Changed lines 35-41 from:
*** Property realizability
** Dependability Assessment
*** Fault tree analysis
*** FMEA analysis
*** FDIR verification
*** Diagnosability checks

to:
*** Property realizability
June 12, 2011, at 08:04 PM by 94.39.213.133 -
Added line 4:
%rfloat height=100px% {$TopLevelUrl}/images/uc.gif
June 12, 2011, at 07:47 PM by 94.39.213.133 -
Changed line 9 from:
** new constructs to represent network of (hybrid-)automata (HyDy)
to:
** new constructs to represent network of (hybrid-)automata (HyDi)
June 12, 2011, at 07:47 PM by 94.39.213.133 -
Changed line 9 from:
** new constructs to represent network of (hybrid-)automata
to:
** new constructs to represent network of (hybrid-)automata (HyDy)
June 12, 2011, at 04:29 PM by 94.39.213.133 -
Changed line 29 from:
* An extended set of features
to:
* An extended set of functionalities
June 12, 2011, at 04:10 PM by 94.39.213.133 -
Added lines 3-4:
(:comment Here the idea is to create several pages one per each category :)
Changed lines 8-10 from:
** new set of types, namely 'Integer' and 'Reals';
** new constructs to represent network of (hybrid-)automata;
** support for the [[http://fmv.jku.at/aiger/|AIGER]] format;
to:
** new set of types, namely 'Integer' and 'Reals'
** new constructs to represent network of (hybrid-)automata
** support for the [[http://fmv.jku.at/aiger/|AIGER]] format
Added line 12:
** Full support for PSL model checking
Added lines 19-21:
*** Basic abstraction vial AllSMT
*** Advanced abstraction based on BDD and SMT
*** Refinement via Unsatisfiable Core and Interpolation
Added lines 23-24:
*** Bounded Model Checking via SMT
*** Abstraction based
Added lines 27-28:
*** Range Recoding
*** Free input propagation
Added line 31:
*** Hybrid and Discrete
June 12, 2011, at 04:06 PM by 94.39.213.133 -
Changed line 8 from:
** support for the [[http://aiger|AIGER]] format;
to:
** support for the [[http://fmv.jku.at/aiger/|AIGER]] format;
June 12, 2011, at 03:58 PM by 94.39.213.133 -
Added lines 1-30:
(:title Features :)

The following is an incomplete list of the provided features:

* An extended language
** new set of types, namely 'Integer' and 'Reals';
** new constructs to represent network of (hybrid-)automata;
** support for the [[http://aiger|AIGER]] format;
* new advanced model checking algorithms
** Interpolation based invariant checking
*** [[http://www.kenmcmil.com/pubs/CAV03.pdf|CAV 2003]] Mc Millan algorithm
*** Interpolation sequences algorithm
** Guided reachability
*** Reachability analysis guided by a regular expression
** Counter-Example Guided Abstraction Refinement (CEGAR)
** Infinite state model checking based on SMT techniques
** Compositional reasoning techniques
** Model simplification and recoding techniques
* An extended set of features
** Requirements Analysis
*** Property satisfiability
*** Property entailment
*** Unsatisfiable core extraction
*** Property realizability
** Dependability Assessment
*** Fault tree analysis
*** FMEA analysis
*** FDIR verification
*** Diagnosability checks


Page last modified on August 22, 2017, at 04:08 PM