Features.Home History
Hide minor edits - Show changes to output - Cancel
Added lines 28-31:
* Common Cause Analysis (CCA)
** Definition of Common Causes
** Fault Tree Analysis with Common Causes
** 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
** 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
** 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
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
** 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:
** 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:
*
**
**
Added lines 35-37:
** Explicit FSM view generation
*** Dump in .xmi format
*** Subject to predicate abstraction
*** Dump in .xmi format
*** Subject to predicate abstraction
Changed lines 12-15 from:
** Range Recoding
** Free input propagation
to:
Added lines 35-37:
** Model simplification and recoding techniques
*** Range Recoding
*** Free input propagation
*** Range Recoding
*** Free input propagation
Deleted lines 35-39:
(:comment Some less important details
** Abstraction via AllSMT, and in combiation with BDDs
*** Refinement via Unsatisfiable Core and Interpolation
)
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
*** Basic abstraction vial AllSMT
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
*** Bounded Model Checking via SMT
** Compositional reasoning techniques
** Model simplification and recoding techniques
*** 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
)
*** 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
Changed line 8 from:
* An extended language
to:
* An extended language for synchronous systems
Deleted line 9:
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
*** 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
** Dependability Assessment
*** Fault tree analysis
*** FMEA analysis
*** FDIR verification
*** Diagnosability checks
to:
*** Property realizability
Changed line 9 from:
** new constructs to represent network of (hybrid-)automata (HyDy)
to:
** new constructs to represent network of (hybrid-)automata (HyDi)
Changed line 9 from:
** new constructs to represent network of (hybrid-)automata
to:
** new constructs to represent network of (hybrid-)automata (HyDy)
Changed line 29 from:
* An extended set of features
to:
* An extended set of functionalities
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
** 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
*** Advanced abstraction based on BDD and SMT
*** Refinement via Unsatisfiable Core and Interpolation
Added lines 23-24:
*** Bounded Model Checking via SMT
*** Abstraction based
*** Abstraction based
Added lines 27-28:
*** Range Recoding
*** Free input propagation
*** Free input propagation
Added line 31:
*** Hybrid and Discrete
Changed line 8 from:
** support for the [[http://aiger|AIGER]] format;
to:
** support for the [[http://fmv.jku.at/aiger/|AIGER]] format;
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
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