Abstract SCADE is both a formal language and a model-based development environment, widely used to build and verify the models of safety-critical system (SCS). The SCADE Design Verifier (DV) provides SAT-based verification. However, DV cannot adequately express complex temporal specifications, and it may fail due to complexity problems such as floating numbers which are often used in the aeronautics domain. In addition, manually writing temporal specifications is not only time-consuming but also error-prone. To address these challenges, we propose an AGVTS method that can automate the task of generating temporal specifications and verifying aeronautics SCADE models. At first, we define a modular pattern language for precisely expressing Chinese natural language requirements. Then, we present a rule-based translation augmented with BERT, which translates restricted requirements into LTL and CTL. In addition, SCADE model verification is achieved by transforming it into nuXmv which supports both SMT-based and SAT-based verification. Finally, we illustrate a successful application of our methodology with an ejection seat control system, and convince our industrial partners of the usefulness of formal methods for industrial systems.

Opacity is an important security notion for discrete event systems (DESs) to measure the secret behaviors leaked to an intruder. The intruder is usually modeled as a malicious observer who always attempts to infer secret behaviors based on his dynamical observations of the system. In our earlier research, we proposed several opacity measures for DESs from the perspective of fuzzy logic, in which the intruder is assumed to only infer the current secret behaviors. Considering that modern computers usually have a powerful computation ability and rich memory resources, this article presents a new opacity measure of DESs, called as fuzzy infinite-step opacity (FIO) measure, where the intruder is assumed to have the ability of inferring all the secret behaviors that occurred in the past. In addition, the properties and the calculation of the FIO measure are also investigated. The FIO measure can be used to assess the secret-leakage situations of fuzzy DESs attacked by powerful intruders. For the purpose of illustration, we present a practical application of the FIO measure in evaluating the privacy protection mechanisms in location-based services.

Opacity, as an important security property, has been well investigated in crisp discrete event systems. However, in some practical systems, the general behaviors, secret and nonsecret behaviors obtained by the intruder need to be expressed as fuzzy sets rather than crisp sets. Under this situation, the intruder makes inferences by fuzzy logic rather than classic logic, thus the notions of the fuzzy opacity measures are desired to be established. First, by means of the basic laws of fuzzy logic, a general fuzzy opacity measure, as a template, is presented, in this article, for the given generalized characterizations of secret and nonsecret behaviors. Moreover, a specific measure, called as fuzzy initial-final opacity (FIFO) measure, is investigated under the assumption that the secrets and nonsecrets can be coded into the initial-final state-pairs. In addition, two variants of FIFO measure are also proposed under the assumptions that the secrets and nonsecrets are only related to the initial-states or final-states. With these fuzzy opacity measures, the system designers can evaluate the opacity degree of the systems to be designed. To show the applicability of the fuzzy opacity measures to practical systems, we finally present an illustrative example of evaluating the location privacy protection systems in location-based services by means of the fuzzy opacity measures.

In our earlier paper (i.e., Deng and Qiu, 2017), we have investigated the safe-diagnosis problem for discrete-event systems (DESs) with assumptions that events completely cannot be obtained and states can be measured by sensors under the so-called state-based decentralized architecture (SDA). In this paper, we continue to consider this problem under an economical decentralized architecture (EDA). The corresponding safe-diagnosability, as well as a polynomial-time verification algorithm is presented.

Recently, we have introduced bi-fuzzy discrete event systems (BFDESs) and established their supervisory control theory under full observations and partial observations, respectively. Compared with the models of discrete event systems and fuzzy discrete event systems, BFDESs are more satisfactory models to characterize some high-uncertainty systems. In this paper, we study the fault diagnosis problems of BFDESs. First, the framework of state-based decentralized diagnosis is introduced. Then, the notion of state-based codiagnosability is defined and a necessary and sufficient condition for state-based codiagnosability is provided. In particular, a polynomial-time algorithm for state-based codiagnosability verification and an online decentralized diagnosis method are presented. In addition, a compact state-based decentralized diagnosis framework is introduced, and the notion of state-based jointly diagnosability and its verification algorithm are proposed. Finally, the implication relationships between the two diagnosabilities are investigated.

The supervisory control theory of fuzzy discrete-event systems (FDESs) for fuzzy language equivalence has been developed. However, in a way, language equivalence has limited expressiveness. Therefore, if the given specification can not be expressed by language equivalence, then the control for language equivalence does not work. In this paper, we further establish the supervisory control theory of FDESs for fuzzy simulation equivalence whose expressiveness is stronger than that of fuzzy language equivalence. First, we formalize the notions of fuzzy simulation and fuzzy simulation equivalence between two FDESs. Then, we present a method for deciding whether there is a fuzzy simulation or not. In addition, we also show several basic properties of fuzzy simulation relations. Afterward, we put forward the notion of fuzzy simulation-based controllability and, in particular, show that it serves as a necessary and sufficient condition for the existence of the fuzzy supervisors of FDESs. Moreover, we study the “range” control problem of FDESs. Some examples are given to illustrate the main results obtained.

It is well known that type-1 fuzzy sets (T1 FSs) have limited capabilities to handle some data uncertainties directly, and type-2 fuzzy sets (T2 FSs) can cover the shortcoming of T1 FSs to a certain extent. Fuzzy discrete event systems (FDESs) were proposed based on T1 FSs theory. Hence, FDES may not be a satisfactory model to characterize some high-uncertainty systems. In this paper, we propose a new model, called as bifuzzy discrete event systems (BFDESs), by combining classical DESs theory and T2 FSs theory. Then, we consider the supervisory control problem of BFDESs. The bifuzzy controllability theorem and nonblocking bifuzzy controllability theorem are demonstrated. In addition, an algorithm for checking the bifuzzy controllability condition is presented. In addition, two controllable approximations to an uncontrollable language are investigated in detail. An illustrative example is provided to show the applicability and the advantages of the BFDES model.