SMT-Based Validation of Timed Failure Propagation Graphs
Authors: Marco Bozzano, Alessandro Cimatti, Marco Gario, Andrea Micheli
AAAI 2015 | Conference PDF | Archive PDF | Plain Text | LLM Run Details
| Reproducibility Variable | Result | LLM Response |
|---|---|---|
| Research Type | Experimental | We implemented a prototype tool using the techniques described in this paper. The tool is able to generate partial traces for a TFPG, test possibility and necessity of arbitrary conditions, check refinement, and perform diagnosis and diagnosability. Due to the lack of publicly available TFPGs, we evaluated the scalability of the approach on a benchmark of randomly generated TFPGs. We run two sets of experiments: refinement and diagnosability. |
| Researcher Affiliation | Academia | Marco Bozzano, Alessandro Cimatti, Marco Gario and Andrea Micheli Fondazione Bruno Kessler Italy {bozzano,cimatti,gario,amicheli}@fbk.eu |
| Pseudocode | No | The paper uses mathematical formulas for encoding TFPGs (e.g., Bor, Tor, Band, Tand) but does not include any clearly labeled pseudocode or algorithm blocks. |
| Open Source Code | Yes | Prototype tool and benchmarks are available at http://es.fbk.eu/people/gario/aaai15/ |
| Open Datasets | Yes | Due to the lack of publicly available TFPGs, we evaluated the scalability of the approach on a benchmark of randomly generated TFPGs. Prototype tool and benchmarks are available at http://es.fbk.eu/people/gario/aaai15/ |
| Dataset Splits | No | The paper describes using randomly generated TFPGs as benchmarks for evaluation, but it does not specify explicit training, validation, or test splits of a dataset in the context of model training/evaluation. |
| Hardware Specification | Yes | We run our experiments using Z3 (de Moura and Bjørner 2008) as SMT Solver on an Intel i7 2.93GHz, using a time-out of 300 seconds and memory-out of 2GB for all experiments. |
| Software Dependencies | No | The paper mentions 'Z3 as SMT Solver' but does not specify a version number for Z3 or any other software libraries or dependencies with their versions. |
| Experiment Setup | Yes | We run our experiments using Z3 (de Moura and Bjørner 2008) as SMT Solver on an Intel i7 2.93GHz, using a time-out of 300 seconds and memory-out of 2GB for all experiments. |