The wide deployment of Deep Neural Networks (DNNs), though achieving great success in many domains, has severe safety concerns. Inspired by testing criteria from traditional software engineering, various coverage criteria have been proposed to ensure the safety of DNNs. However, the validity of coverage criteria was questioned in related researches. In this paper, we evaluate the performance of dominating coverage criteria in two aspects: 1) distinguishing different qualities of test sets, 2) improving the safety and robustness of DNNs. The evaluation result confirms that coverage criteria are meaningful metrics for DNNs. Specifically, the way for improving robustness is contrary to the previous assumption: the higher coverage criterion score, the better. In addition, we propose a new coverage criterion called Independence Neuron Coverage (INC) which is finer grained to capture DNNs' subtle behaviour. Experiments show that INC is efficient and performs better than other evaluated coverage criteria in both aspects.

Deep Learning (DL) offers a data-driven programming paradigm in which Deep Neural Networks (DNNs) can be constructed through a set of training data.It has been widely adopted in many real-world applications.However, many studies have shown that DL systems suffer from adversarial attacks, especially when they are applied to security-and safetycritical domains.Given that formal verification has proved a great success in many areas such as software engineering, using it to achieve a high-level security assurance in DL systems is considered promising.In this paper, we design and implement DeepAuto which makes the significant bridge between automata and DNNs.With the aid of DeepAuto, we demonstrate how DNNs can be modeled as automata and be verified formally in the widely used model checker UPPAAL.The potential usefulness of DeepAuto shows the connection between DNNs and automata and provides a solution for the construction of more trustworthy DL systems.

Component-Based Software Engineering (CBSE) has played an important role in software industry for several decades.The Mediator language is proposed to formally model complex hierarchical component-based systems, which provides a proper automata-based formalism for specifying both high-level system layouts and low-level behavior units.In this paper, we develop a framework for translating Mediator models into the model checker PRISM, and build such a "translator" which can generate PRISM codes from Mediator models automatically and cooperates with PRISM to verify properties of Mediator models.