A Statistical Approach for Timed Reachability in AADL Models

We introduce a simulator (slimsim) for a subset of AADL extended with formalized behavioral semantics for nominal and error models. The simulator allows to perform probabilistic analysis using the Monte Carlo method, on linear-hybrid, stochastic models, which describe a combination of nominal and error behaviors of hard- and software components. The tool supports the use of different strategies, which control the behavior of the simulator when dealing with various forms of non-determinism. The simulator is tested using benchmarks of the COMPASS toolset, as well as a case study by Airbus Defense and Space.