## 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