Marco Gario

Sabiha Tahrat, German Braun, Alessandro Artale et al.

This paper investigates the feasibility of automated reasoning over temporal DL-Lite (TDL-Lite) knowledge bases (KBs). We test the usage of off-the-shelf LTL reasoners to check satisfiability of TDL-Lite KBs. In particular, we test the robustness and the scalability of reasoners when dealing with TDL-Lite TBoxes paired with a temporal ABox. We conduct various experiments to analyse the performance of different reasoners by randomly generating TDL-Lite KBs and then measuring the running time and the size of the translations. Furthermore, in an effort to make the usage of TDL-Lite KBs a reality, we present a fully fledged tool with a graphical interface to design them. Our interface is based on conceptual modelling principles and it is integrated with our translation tool and a temporal reasoner.

Benjamin Bittner, Marco Bozzano, Roberto Cavada et al.

This paper describes the xSAP safety analysis platform. xSAP provides several model-based safety analysis features for finite- and infinite-state synchronous transition systems. In particular, it supports library-based definition of fault modes, an automatic model extension facility, generation of safety analysis artifacts such as Dynamic Fault Trees (DFTs) and Failure Mode and Effects Analysis (FMEA) tables. Moreover, it supports probabilistic evaluation of Fault Trees, failure propagation analysis using Timed Failure Propagation Graphs (TFPGs), and Common Cause Analysis (CCA). xSAP has been used in several industrial projects as verification back-end, and is currently being evaluated in a joint R&D Project involving FBK and The Boeing Company.