Testing-based formal verification (TBFV) is proposed to reduce test cost and guarantee software reliability by ensuring the correctness of all traversed program paths. An ideal target is to generate adequate test cases to traverse all of its execution paths. However, it is a rather ambitious criterion that can hardly be satisfied due to the potentially great amount of test cases required. To address this problem, we propose a new criterion called Condition Sequence Coverage (CSC) to maintain a good balance between program correctness and the number of test cases. In this paper, we refine the TBFV method and introduce the theoretical foundations of CSC. We also integrate CSC with functional scenario form (FSF) to automatically generate test cases for the TBFV method. In addition, we develop the tool support for Java and validate its effectiveness and accuracy through experimental comparisons.

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.

Autonomous spacecraft rendezvous is very challenging in increasingly complex space missions. In this article, we present our approach model-based reinforcement learning for spacecraft rendezvous guidance (MBRL4SRG). We build a Markov decision process model based on the Clohessy-Wiltshire equation of spacecraft dynamics and use dynamic programming to solve it and generate the decision table as the optimal agent policy. Since the onboard computing system of spacecraft is resource constrained in terms of both memory size and processing speed, we train a neural network (NN) as a compact and efficient function approximation to the tabular representation of the decision table. The NN outputs are formally verified using the verification tool ReluVal, and the verification results show that the robustness of the NN is maintained. Experimental results indicate that MBRL4SRG achieves lower computational overhead than the conventional proportional–integral–derivative algorithm and has higher trustworthiness and better computational efficiency during training than the model-free reinforcement learning algorithms.

Safety-critical cyber-physical systems (SC-CPS) have the characteristics of distributed, heterogeneous, strong coupling of computing resources and physical resources. With the increased acceptance of Model-Driven Development (MDD) in the safety-critical domain, the SysML language has been broadly used. Increasing complexity results in the formal verification of the SysML models of SC-CPS often faces the so-called state-explosion problem. Moreover, safety analysis is also an important step to ensure the quality of SC-CPS. Thus, this article proposes an integrated SysML modelling and verification approach to cover specification of nominal behaviour and safety. First, an extension of SysML is presented, in which the contract information (i.e. Assume and Guarantee) is extended for SysML block diagrams and a Safety Profile is proposed to describe safety-related concepts. Second, the transformation from SysML to the compositional verification tool OCRA is given. Third, the safety analysis is achieved by translating the Safety Profile model into FTA (Fault Tree Analysis). Finally, the prototype tools including SysML2OCRA and SafetyProfile2FTA are represented, and the effectiveness of the method proposed in this paper is verified through actual industrial cases.

Abstract Machine learning (ML) is used increasingly in safety-critical systems to provide more complex autonomy to make the system to do decisions by itself in uncertain environments. Using ML to learn system features is fundamentally different from manually implementing them in conventional components written in source code. In this paper, we make a first step towards exploring the architecture modeling of safety-critical autonomous systems which are composed of conventional components and ML components, based on natural language requirements. Firstly, augmented intelligence for restricted natural language requirement modeling is proposed. In that, several AI technologies such as natural language processing and clustering are used to recommend candidate terms to the glossary, as well as machine learning is used to predict the category of requirements. The glossary including data dictionary and domain glossary and the category of requirements will be used in the restricted natural language requirement specification method RNLReq, which is equipped with a set of restriction rules and templates to structure and restrict the way how users document requirements. Secondly, automatic generation of SysML architecture models from the RNLReq requirement specifications is presented. Thirdly, the prototype tool is implemented based on Papyrus. Finally, it presents the evaluation of the proposed approach using an industrial autonomous guidance, navigation and control case study.

Requirements traceability is broadly recognized as a critical element of any rigorous software development process, especially for building safety-critical software (SCS) systems. Model-driven development (MDD) is increasingly used to develop SCS in many domains, such as automotive and aerospace. MDD provides new opportunities for establishing traceability links through modeling and model transformations. Architecture Analysis and Design Language (AADL) is a standardized architecture description language for embedded systems, which is widely used in avionics and aerospace industries to model safety-critical applications. However, there is a big challenge to automatically establish the traceability links between requirements and AADL models in the context of MDD, because requirements are mostly written as free natural language texts, which are often ambiguous and difficult to be processed automatically. To bridge the gap between natural language requirements (NLRs) and AADL models, we propose an approach to generate the traceability links between NLRs and AADL models. First, we propose a requirement modeling method based on the restricted natural language, which is named as RM-RNL. The RM-RNL can eliminate the ambiguity of NLRs and barely change engineers' habits of requirement specification. Second, we present a method to automatically generate the initial AADL models from the RM-RNLs and to automatically establish traceability links between the elements of the RM-RNL and the generated AADL models. Third, we refine the initial AADL models through patterns to achieve the change of requirements and traceability links. Finally, we demonstrate the effectiveness of our approach with industrial case studies and evaluation experiments.

AADL is a modeling language to design and analyze embedded real-time systems and is widely used to model safety-critical systems. AADL describes the system models hierarchically through components such as systems, processes, and threads, etc. The Behavioral Annex is a supplement of AADL in terms of functional behavior. It enables modeling component and component interaction behavior in a state-machine-based annex sublanguage. At present, there is no mechanism to represent hierarchical automata in the behavioral annex. However, this is a very important feature because industrial complex systems are always described with concurrent and composite states. Although we can model a system with AADL's own hierarchical description capabilities, it will result in a large amount of threads. In actual development, a refinement process is always needed before system synthesis, in which several threads may be combined into one thread that has concurrent and composite states. This paper proposes a hierarchical extension of the AADL behavioral annex which is named HBA (Hierarchical Behavior Annex). First, the formal syntax of HBA is given, and then we formally define the semantics of HBA. We propose a meta-model of HBA and implement its textual and graphical editor in the OSATE environment. Finally, an industrial case study is given to validate the approach.

Many runtime verification tools are built based on Aspect-Oriented Programming (AOP) tools, most often AspectJ, a mature implementation of AOP for Java. Although already popular in the Java domain, there is few work on runtime verification of C programs via AOP, due to the lack of a solid language and tool support. In this paper, we propose a new general purpose and expressive language for defining monitors as an extension to the C language, and present our tool implementation of the weaver, the Movec compiler, which brings fully-fledged parametric runtime verification support into the C domain. These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.

Standards play the key role in safety-critical systems. Errors in standards could mislead system developer's understanding and introduce bugs into system implementations. In this paper, we present an Event-B formalization and verification for the ARINC 653 standard, which provides a standardized interface between safety-critical real-time operating systems and application software, as well as a set of functionalities aimed to improve the safety and certification process of such safety-critical systems. The formalization is a complete model of ARINC 653, and provides a necessary foundation for the formal development and verification of ARINC 653 compliant operating systems and applications. Three hidden errors and three cases of incomplete specification were discovered from the verification using the Event-B formal reasoning approach.

SIGNAL belongs to the synchronous languages family. Such languages are widely used in the design of safety-critical real-time systems such as avionics, space systems, and nuclear power plants. This paper reports a key step of a verified SIGNAL compiler prototype, that is the transformation from a subset of SIGNAL to S-CGA (a variant of clocked guarded actions) and the proof of semantics preservation. Compared with the existing SIGNAL compiler, we use clocked guarded actions as the intermediate representation, to integrate more synchronous programs into our verified compiler prototype in the future. However, in contrast to the SIGNAL language, clocked guarded actions can evaluate a variable even if its clock does not hold. Thus, we propose a variant of clocked guarded actions, namely S-CGA, which constrains variable accesses as done by SIGNAL. To conform with the revised semantics of clocked guarded actions, we also do some adjustments on the existing translation rules from SIGNAL to clocked guarded actions. Finally, the verified transformation is mechanized in the theorem prover Coq.

The analysis and verification of an AADL model usually requires its transformation into the meta-model of this model-checker or that schedulability analysis tool. However, one challenging problem is to prove that the transformation into the target model of computation (MoC) preserves the semantics of the original AADL model or at least some of its properties. Moreover, the AADL standard lacks a formal semantics to make the validation of this translation possible. Albeit some of the related works give informal explanations on the model transformations they apply to interpret or compile AADL, the formal proof of semantics preservation remains in most cases altogether impossible. Our contribution is to bridge this gap by providing two formal semantics for a synchronous subset of AADL, which includes periodic threads and data port communications. Its operational semantics is formalized as a TTS (Timed Transition System). This formalization is one prerequisite to the formal proof of semantics preservation for our model transformation from AADL sources to our target verification formalism: TASM (Timed Abstract State Machine). In this paper, an abstract syntax of (our subset of) AADL is given, together with the abstract syntax of TASM. The translation is formalized by a family of semantics functions, which associates each AADL construct to a TASM fragment. Then, the proof of simulation equivalence between the TTSs of the AADL and the TASM models is formalized and mechanized using the proof assistant Coq.

AADL is an Architecture Description Language which describes embedded real-time systems. Behavior annex is an extension of the dispatch mechanism of AADL execution model. This paper proposes a formal semantics for the AADL behavior annex using Timed Abstract State Machine (TASM). Firstly, the semantics of AADL default execution model is given, and then we formally define some aspects semantics of behavior annex. A prototype of real-time behavior modeling and verification is proposed, and finally, a case study will be given to validate the feasibility.

This paper presents some real-time concepts as they are found in the AADL language and proposes their expression in two formalisms suitable for formal analysis: FIACRE which is based on timed transition systems and TASM which extends abstract state machines with resource consumption mechanisms.