Formal methods are promising for modeling and analyzing system requirements. However, applying formal methods to large-scale industrial projects is a remaining challenge. The industrial engineers are suffering from the lack of automated engineering methodologies to effectively conduct precise requirement models, and rigorously validate and verify (V&V) the generated models. To tackle this challenge, in this paper, we present a systematic engineering approach, named Formal Requirement Engineering Platform in Aircraft (FREPA), for formal requirement modeling and V&V in the aerospace and aviation control domains. FREPA is an outcome of the seamless collaboration between the academy and industry over the last eight years. The main contributions of this paper include 1) an automated and systematic engineering approach FREPA to construct requirement models, validate and verify systems in the aerospace and aviation control domain, 2) a domain-specific modeling language AASRDL to describe the formal specification, and 3) a practical FREPA-based tool AeroReq which has been used by our industry partners. We have successfully adopted FREPA to seven real aerospace gesture control and two aviation engine control systems. The experimental results show that FREPA and the corresponding tool AeroReq significantly facilitate formal modeling and V&V in the industry. Moreover, we also discuss the experiences and lessons gained from using FREPA in aerospace and aviation projects.

Runtime verification is a dynamic verification technique widely used in practice. In this paper we revisit the runtime verification technique with formula progression, which verifies the execution trace step by step by progressing the desired property written in temporal logic. The previous work did not discuss explicitly the bound for the sizes of expanded formulas, while the successive invoking of formula progression is likely to cause divergence. In this paper, we present the convergent formula progression by introducing a novel fix-point reduction technique, and prove it guarantees the sizes of expanded formulas be always convergent. To the best of our knowledge, this is the first work discussing the convergence of formula progression. Furthermore, we implement the new runtime verification framework, and experiments show the efficiency of our proposed strategy.

The AUTOSAR (AUTomotive Open System ARchitecture) is an open standard in automotive industry, aiming at unifying the methodology of the automotive software development. It is drawing increasing attention because of its great concern about the safety of automotive electronics. The safety of automotive electronics greatly depends on the Operating System (OS) components, which fully implement the functionality part of automotive applications. However, taking the complex timing protection mechanism of AUTOSAR OS and random occurrences of interrupt requests (IRs) into consideration, it is hard for the developers to design and configure the OS components correctly or even reconcilably. In this paper, we focus on the timing properties and propose an automatic verification framework, in which developers could analyze the timing behaviors and devise the OS components configuration. Furthermore, three important timing properties are expressed and can be verified in our framework, namely, schedulability, non-fault-propagation, and consistency. As a reduced version of AUTOSAR OS and auxiliary analysis modules have been implemented based on Real-Time Maude, developers could easily employ the tool to experiment with different configurations of OS components.

This paper proposes a requirement analysis approach to periodic control systems that are widely used as one of the real time systems. By regulating the initial requirement documents with key words in natural language, we compile the regulated requirement documents into an intermediate model specified by SPARDL language with formal syntax and semantics. To make the requirement executable, a prototype generation technique is proposed to simulate the system behaviors. To analyze the dataflow relations among modules among the same mode or different modes, we introduce module-level and mode-level dataflow analysis techniques to help system engineers to uncover the potential affections on any two modules. The dataflow analysis techniques are useful especially for module reuse when a new version of the system is developed. We have applied the developed tool based on our approach to the Moon-Exploration Spacecraft Project from Beijing Institute of Control Engineering, and the preliminary experiments are encouraging. We have found both the ambiguity and the inconsistency cases in the requirement documents from the project.

SPARDL is a domain-specific modeling language for periodic control systems, which are widely used in embedded systems. Periodic control systems are usually driven by the given period. A periodic control system can be decomposed into different modes or sub-modes, and each mode represents a system state observed from outside. We believe that introducing static checking will extend the power of SPARDL. In this paper, we develop a type system for SPARDL. To make the contributions of this paper convincible and easy to understand, we apply the traditional approaches to construct the type system for SPARDL. An operational semantics is proposed as the basic explanation of SPARDL. And then some type safety theorems are proved under such semantics. We apply the type system to an industrial case from China Academy of Space Technology(CAST) to evaluate the effectiveness of our approach in practice, and then eight type errors are revealed.

The service choreography gives a global view on the collaboration among a collection of services involving multiple different organizations or independent processes. In this paper, a formal model for service choreography based on WS-CDL language is proposed. This model explores the key concepts related to choreography, such as passing channel, fault handling and finalization mechanisms. This study brings us the insights for the analysis, synthesis and verification of service choreography. For instance, the choreography synthesis is discussed based on our trace semantics achieved.

Test data generation is one of the important tasks during software testing. This paper proposes an approach to generating test cases automatically for the unit test of C programs with derived types including pointers, structures and arrays. Our approach combines symbolic execution and concrete execution. The approach captures operations on variables precisely by concrete execution, and thus it is capable of handling derived types. Benefited from symbolic execution, accessing variables as array index can be solved by a substitution strategy. The substitution strategy also translates a path constraint involving variables of derived type to the one containing only primitive variables. An implementation of this approach is integrated into our test case generation tool called CAUT. Experimental results show that our approach is effective to generate test data for derived types.

rCOS, the abbreviation of Refinement Calculus for Object Systems, is designed to present mathematical characterization of essential object-oriented concepts for an object-based language with a rich variety of features including subtypes, inheritance, type casting, dynamic binding and polymorphism. This paper represents an operational semantics for the rCOS language based on labeled transition systems. The result semantics shows the process of how the effects of an rCOS program are produced. It can be a secure guide for the implementation of the rCOS language, which is being carried out by our group. For the purpose of extending verifiability and functionality, a set of auxiliary language features is introduced to the rCOS language. Concurrent execution structure is designed to specify multi-threaded programs. Also the simulation is introduced to specify the observable behaviors of objects, and it can be regarded as the refinement relation defined in denotational domain to some extent.

This paper presents an approach to validation and verification of the WSCDL specification. In order to validate whether the CDL document is well defined or not, we introduce OCL to precisely describe the constraints which was expressed by natural language, and design a simple validator to check the static properties of the CDL document. The validator is created based on a Java model and the Java model is generated according to the UML diagrams with OCL constraints which is used to describe CDL specification. To verify the dynamic properties of CDL document, we model the behavior of CDL document with Java, so that Java Pathfinder model checker can be applied to check the desired properties. The assert activity is introduced to the CDL specification for describing the logic properties, to facilitate the verification process. A case study is given and it shows that our approach is both effective and practical. Moreover, this approach can check almost every kinds of CDL document, even the documents including exception block or finalize block.