Automated Synthesis of Timed Failure Propagation Graphs
Authors: Benjamin Bittner, Marco Bozzano, Alessandro Cimatti
IJCAI 2016 | Conference PDF | Archive PDF | Plain Text | LLM Run Details
| Reproducibility Variable | Result | LLM Response |
|---|---|---|
| Research Type | Experimental | The proposed approach has been implemented on top of state-of-the-art symbolic model-checking techniques, and thoroughly evaluated on a number of synthetic and industrial benchmarks. |
| Researcher Affiliation | Academia | Benjamin Bittner1,2 and Marco Bozzano1 and Alessandro Cimatti1 1Fondazione Bruno Kessler, 2University of Trento |
| Pseudocode | Yes | Algorithm 1 TFPG-by-FTA |
| Open Source Code | No | Benchmark files can be downloaded at es.fbk.eu/people/bittner/ijcai16.tar.gz - This link is for benchmark files, not the source code of the implemented methodology. The paper states 'The proposed approach has been implemented on top of state-of-the-art symbolic model-checking techniques', referring to tools like x SAP and nu Xmv, but does not provide their own source code. |
| Open Datasets | Yes | Benchmark files can be downloaded at es.fbk.eu/people/bittner/ijcai16.tar.gz |
| Dataset Splits | No | No specific dataset split information (e.g., percentages, sample counts, or detailed splitting methodology) for training, validation, or testing was provided in the paper. |
| Hardware Specification | Yes | All tests were run on a dedicated 64bit Linux computer with a 12 core CPU at 2.67 GHz and 100GB of RAM. Four cores were reserved for each test run to limit potential time skew. Each test was executed on a single core with a time limit of 900 seconds and a memory limit of 4GB. |
| Software Dependencies | No | For the FTA part we use the techniques of [Bozzano et al., 2015c] off-the-shelf, as implemented in the safety analysis toolkit x SAP [Bittner et al., 2016a], which itself is based on nu Xmv [Cavada et al., 2014], a symbolic model checker for infinite-state transition systems. The simplification step was implemented based on the SMT solver Math SAT5 [Cimatti et al., 2013]. - While specific tools are mentioned, their version numbers are not explicitly stated within the text. |
| Experiment Setup | Yes | Each test was executed on a single core with a time limit of 900 seconds and a memory limit of 4GB. |