Search

When data-driven algorithms, especially the ones based on deep neural networks (DNNs), replace classical ones, their superior performance often comes with difficulty in their analysis. On the way to compensate for this drawback, formal verification techniques, which can provide reliable guarantees on program behavior, were developed for DNNs. These techniques, however, usually consider DNNs alone, excluding real-world environments in which they operate, and the applicability of techniques that do account for such environments is often limited. In this work, we consider the problem of formally verifying a neural controller for the routing problem in a conveyor network. Unlike in known problem statements, our DNNs are executed in a distributed context, and the performance of the routing algorithm, which we measure as the mean delivery time, depends on multiple executions of these DNNs. Under several assumptions, we reduce the problem to a number of DNN output reachability problems, which can be solved with existing tools. Our experiments indicate that sound-and-complete formal verification in such cases is feasible, although it is notably slower than the gradient-based search of adversarial examples.The paper is structured as follows. Section 1 introduces basic concepts. Then, Section 2 introduces the routing problem and DQN-Routing, the DNN-based algorithm that solves it. Section 3 proposes the contribution of this paper: a novel sound and complete approach to formally check an upper bound on the mean delivery time of DNN-based routing. This approach is experimentally evaluated in Section 4. The paper is concluded with some discussion of the results and outline of possible future work.

Recent studies have shown that modern deep neural network classifiers are easy to fool, assuming that an adversary is able to slightly modify their inputs. Many papers have proposed adversarial attacks, defenses and methods to measure robustness to such adversarial perturbations. However, most commonly considered adversarial examples are based on perturbations in the input space of the neural network that are unlikely to arise naturally. Recently, especially in computer vision, researchers discovered “natural” perturbations, such as rotations, changes of brightness, or more high-level changes, but these perturbations have not yet been systematically used to measure the performance of classifiers. In this paper, we propose several metrics to measure robustness of classifiers to natural adversarial examples, and methods to evaluate them. These metrics, called latent space performance metrics, are based on the ability of generative models to capture probability distributions. On four image classification case studies, we evaluate the proposed metrics for several classifiers, including ones trained in conventional and robust ways. We find that the latent counterparts of adversarial robustness are associated with the accuracy of the classifier rather than its conventional adversarial robustness, but the latter is still reflected on the properties of found latent perturbations. In addition, our novel method of finding latent adversarial perturbations demonstrates that these perturbations are often perceptually small.

Closed-loop model checking, a formal verification technique for industrial automation systems, increases the richness of specifications to be checked and reduces the state space to be verified compared to the open-loop case. To be applied, it needs the controller and the plant formal models to be coupled. There are approaches for controller synthesis, but little has been done regarding plant model construction. While manual plant modeling is time consuming and error-prone, discretizing a simulation model of the plant leads to state excess. This paper aims to solve the problem of automatic plant model construction from existing specification, which is represented in the form of plant behavior examples, or traces, and temporal properties. The proposed method, which is based on the translation of the problem to the Boolean satisfiability problem, is evaluated and shown to be applicable on several case study plant model synthesis tasks and on randomly generated problem instances.

One of the challenges of requirements engineering is the fact that requirements are often formulated in natural language. This represents difficulty if requirements must be processed by formal approaches, especially if these approaches are intended to check the requirements. In model checking, a formal technique of verification by exhaustive state space exploration, requirements must be stated in formal languages (most commonly, temporal logics) which are essentially supersets of the Boolean propositional logic. Translation of natural language requirements to these languages is a process which requires much knowledge and expertise in model checking as well the ability to correctly understand these requirements, and hence automating this process is desirable. This paper reviews existing approaches of requirements formalization that are applicable for, or at least can be adapted to generation of discrete time temporal logic requirements. Based on the review, conclusions are made regarding the practical applicability of these approaches for the considered problem.

A method for control finite state machine (FSM) induction in which an ant colony opti� mization algorithm is used for search optimization is proposed. The efficiency of this method is esti� mated using the generation of FSMs for controlling a model of an unmanned aerial vehicle (UAV). It is shown that the proposed method outperforms the method based on genetic algorithms both in terms of performance and quality.

In this paper we improve an earlier developed method of finite-state machine (FSM) induction for controlling objects with complex behavior. This method allows to construct FSMs with continuous (real-valued) output actions. A set of human-created training samples serves as input data for it. We apply an ant colony optimization algorithm and a (μ, λ)-evolution strategy for solving the problem as more effective than a genetic algorithm used in the initial method. The modification of the method is evaluated on the problem of unmanned aircraft control.

Formal methods and languages are used to prove the correctness of various industrial systems, especially mission-critical ones. They can also be viewed as a means to provide safety and correctness demonstration to the stakeholders of such systems. In domains such as nuclear power plant engineering, the benefits from structured safety evidences would seem obvious. However, most stakeholders in nuclear power industry are not even familiar with formal notations. As a result, to promote the applications of formal methods in practice, the first step is to make formal specification languages (FSLs) more accessible. With user-friendly FSLs, users can focus on safety requirements rather than on their sophisticated formalization. This paper, as a preliminary work towards an integrated framework supporting transparent safety demonstration, reviews existing approaches applied to facilitate requirements formalization and formal specifications. Moreover, the common features of user-friendly languages and their tool supports are also summarized.

Finite-state models, such as finite-state machines (FSMs), aid software engineering in many ways. They are often used in formal verification and also can serve as visual software models. The latter application is associated with the problems of software synthesis and automatic derivation of software models from specification. Smaller synthesized models are more general and are easier to comprehend, yet the problem of minimum FSM identification has received little attention in previous research. This paper presents four exact methods to tackle the problem of minimum FSM identification from a set of test scenarios and a temporal specification represented in linear temporal logic. The methods are implemented as an open-source tool. Three of them are based on translations of the FSM identification problem to SAT or QSAT problem instances. Accounting for temporal properties is done via counterexample prohibition. Counterexamples are either obtained from previously identified FSMs, or based on bounded model checking. The fourth method uses backtracking. The proposed methods are evaluated on several case studies and on a larger number of randomly generated instances of increasing complexity. The results show that the Iterative SAT-based method is the leader among the proposed methods. The methods are also compared with existing inexact approaches, i.e. the ones which do not necessarily identify the minimum FSM, and these comparisons show encouraging results., Comment: 21 pages, 9 figures, 7 tables, accepted to International Journal on Software Tools for Technology Transfer. Major changes: the description and results of the Iterative method were updated, the last sections were restructured, new figures were added

The paper addresses the problem of coverage testing of industrial automation software represented in the IEC 61499 standard, one of the recent standards for distributed control system design. Contrary to model-based testing (MBT), the paper focuses on implementation coverage, not model coverage. An approach based on evolutionary algorithms is presented which generates coverage test suites for both basic and composite IEC 61499 function blocks. It employs two third-party tools, FBDK and EvoSuite. The evaluation of the approach was performed on a set of control applications for two lab-scale demonstration plants. Results show that the approach is applicable and shows good performance at least on basic function blocks. The generated tests suites helped to discover several unreachable system parts, which pinpointed errors in the systems under test.

The use of finite-state machines (FSMs) is a reliable choice for control system design since they can be formally verified. In this paper a problem of constructing FSMs with real-valued input and control parameters is considered. It is supposed that a set of human-created behavior examples, or tests, is available. One of the earlier approaches for solving the problem suggested using genetic algorithms together with a transition labeling algorithm. This paper improves this approach via the use of real-valued variables which are calculated using the FSM's input data. FSMs with real-valued variables are represented as systems of linear controllers. The new approach allows to synthesize FSMs of better quality than it was possible earlier.

In this paper a search-based method for constructing finite-state machines (FSMs) with continuous (real-valued) output actions is improved. A more flexible FSM representation model is presented and compared with the previous one on the problem of unmanned aircraft control.

Our general objective in SAUNA (2015-2018) has been to develop integrated methods and tools for safety assessment and transparent safety demonstration of nuclear power plant instrumentation and control (I&C) systems. Due to the multidisciplinary nature of the nuclear power plant as a whole, I&C safety assessment calls for an overall safety point-of-view. We have worked towards that goal by 1) specifying model-based Systems Engineering approaches for I&C, 2) developing concepts and models for analysing Defence-in-Depth issues in I&C architectures, 3) integrating existing methods and finding novel tools for analysing overall safety (with particular focus on formal verification), and 4) developing model-based ways for attesting conformity in the I&C qualification process.