부산대학교 도서관

Artificial neural networks (ANNs) are increasingly being used within safety-critical cyber-physical systems (CPSs). It is important to validate both the timing and functional correctness of these systems. However, most approaches in the literature consider guaranteeing only the functionality of the ANN-based controllers. This issue stems largely from the implementation strategies used within common neural network frameworks—their underlying source code is often simply unsuitable for formal techniques such as static timing analysis. As a result, developers of safety-critical CPS must rely on informal techniques, such as measurement-based approaches, to prove correctness, techniques that provide weak guarantees at best. In this letter, we address this challenge. We propose a design pipeline whereby neural networks trained using the popular deep learning framework Keras are compiled to functionally equivalent C code. This C code is restricted to simple constructs that may be analyzed by the existing static timing analysis tools. As a result, if compiled to a suitable time-predictable platform, all execution bounds may be statically derived. To demonstrate the benefits of our approach, we execute an ANN trained to drive an autonomous vehicle around a race track. We compile the ANN to the Patmos time-predictable controller and show that we can derive the worst-case execution timings.