xsap - - Features

* 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

Restore

November 18, 2014, at 03:02 PM by bozzano -

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:

*
**

Restore

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

Restore

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

Restore

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
)

Restore

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

Restore

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

Restore

June 12, 2011, at 08:04 PM by 94.39.213.133 -

Added line 4:

%rfloat height=100px% {$TopLevelUrl}/images/uc.gif

Restore

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)

Restore

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)

Restore

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

Restore

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

Restore

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;

Restore

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

Restore

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