Abstract:Preface to the Topic of Formal Methods and Their Applications

Abstract:In GitHub platform, many project contributors often ignore the descriptions of Pull Requests (PRs) when submitting PRs, making their PRs easily neglected or rejected by reviewers. Therefore, it is necessary to generate PR descriptions automatically to help increase the PR pass rate. The performances of existing PR description generation methods are usually affected by PR granularity, so it is difficult to generate descriptions for large-granularity PRs effectively. For such reasons, this work focuses on generating descriptions for large-granularity PRs. The text information is first preprocessed in PRs and word-sentence heterogeneous graphs are constructed where the words are taken as secondary nodes, so as to establish the connections between PR sentences. Subsequently, feature extraction is performed on the heterogeneous graphs, and then the features are input to a graph neural network for further graph representation learning, from which the sentence nodes can learn more abundant content information through message delivery between nodes. Finally, the sentences with key information are selected to form a PR description. In addition, the supervised learning method cannot be used for training due to the lack of manually labeled tags in the dataset; therefore, reinforcement learning is adopted to guide the generation of PR descriptions. The goal of model training is minimizing the negative expectation of rewards, which does not require the ground truth and directly improves the performance of the results. The experiments are conducted on real dataset and the experimental results show that the proposed method is superior to existing methods in $F1$ and readability.

Abstract:The unfolding technique can partially alleviate the state explosion in Petri nets through branching processes. However, all states of a system are still contained in its unfolding net. To deal with some practical problems, only the coverability determination of a specific state is needed. In view of this, reducing the scale of the unfolding net is feasible. This study proposes a target-oriented reverse unfolding algorithm for the coverability determination of 1-safe Petri nets, which combines a heuristic technique to reduce the scale of unfolding nets, thereby improving the efficiency of coverability determination. Furthermore, the reverse unfolding is applied to the formal verification of concurrent programs, and their data race detection is converted into the coverability determination of a specific state in 1-safe Petri nets. The experiment compares the efficiency between forward nfolding and reverse unfolding in the coverability determination of a Petri net. The results show that when the Petri net has more forward branches than backward branches, reverse unfolding is more efficient than forward unfolding. Finally, the key factors influencing the efficiency of reverse unfolding are analyzed.

Abstract:Embedded systems have been widely applied in real-time automatic control systems, and most of these systems are safety-critical, for example, the engine control systems in an automobile and the avionics in an airplane. It is very important to verify the schedulability of such a real-time embedded system in its early design stages, so as to avoid unexpected loss for the debugging of architecture design problems. However, it has been proved to be a tough challenge to evaluate the schedulability of a Preemptive-Scheduling Real-Time (PSRT) system, especially when the constraints of system resources are taken into consideration. The cache memory built inside the processor is an exclusive-accessing resource shared by all the tasks deployed on the processor. In addition, the Cache-Related Preemption Delay (CRPD) caused by preemptive task scheduling will bring extra time to the execution time for all the tasks. Thus, the CRPD should be taken into consideration when the Worst-Case Execution Time (WCET) of tasks is estimated in a real-time system. A model-based evaluation and verification method of architecture schedulability, which is designed for priority-based PSRT systems, is proposed in this study to make cache resource constrained and CRPD related schedulability evaluation based on the AADL system architecture model. In the first step, the study enhances the property set of AADL storage elements to make it compatible with cache memory properties in a system architecture model. Secondly, the study proposes a set of algorithms to estimate the CRPDs of a task before it is completed; run system schedule simulation and construct the schedule sequence with the constraint of cache resources and CRPDs involved; and make WCET estimation of the tasks in such a CRPD considered, preemptive-scheduling execution sequence. Finally, the methods mentioned above are implemented within a prototype software toolkit, which is designed to make evaluation and verification of system schedulability within CRPD constraints. The toolkit is tested with a use case of aircraft airborne open-architecture intelligent information system. The result shows that, compared with the schedule sequence constructed without cache memory resource constraints, the WCET estimated for most tasks is extended, and the sequence order is changed. In some extreme cases, when CRPD is taken into consideration, some tasks are evaluated to be incompletable. The test shows that the method and algorithms proposed in this study are feasible.

Abstract:User feature extraction and identity authentication methods based on interactive behavior are an important method of identity recognition. However, for high-frequency users, the interactive behavior patterns and operating habits are relatively stable, which are easily imitated by fraudsters and make the existing models have a higher misjudgment. The key to solving the above problems is to make the users' behavior change smoothly and distinguishably. This study proposes a smooth intervention model based on an individual interactive behavior system to handle it. Firstly, according to the users' historical web behavior log, the change trend of users' interactive behavior is obtained from multiple dimensions. Then, combined with the stability and deviation of the behavior, the Time-Domain Drift Algorithm (TDDA) is proposed to determine the behavior guidance time of each user. Finally, an intervention model for interactive behavior reconstruction systems is proposed, which superimposes behavior trigger factors on non-critical paths in the system to guide users to generate new interactive behavior habits. Experiments prove that the method proposed in this study could guide the user behavior to change smoothly and produce sufficient distinction to significantly advance the model accuracy in the scenario of behavior camouflage anomaly detection.

Abstract:PolarFS is a distributed file system developed by Alibaba with ultra-low latency and high availability. It implements a variant of the Raft consensus protocol, called ParallelRaft. ParallelRaft breaks Raft's strict serialization restrictions in the commitment and execution of log entries and enables state machines to commit and execute log entries in an out-of-order way. However, ParallelRaft is not open-sourced. It has only a brief description, lacking formal specification. Moreover, the correctness of ParallelRaft has not been manually proven or formally checked. The purpose of the study is to provide a precise formal specification for ParallelRaft and to prove its correctness. Specifically, the following main contributions are accomplished. First, to clarify the relationship between Raft and ParallelRaft, ParallelRaft-SE (Sequential Execution) is proposed, which allows out-of-order commitment but prohibits out-of-order executions. Also, a refinement mapping from ParallelRaft-SE to Multi-Paxos is established. Second, it is discovered that ParallelRaft, according to its brief description in the literature, neglects the so-called "ghost log entries" phenomenon, which may violate the consistency among state machines. Therefore, based on ParallelRaft-SE, ParallelRaft-CE (Concurrent Execution) is proposed. ParallelRaft-CE avoids the "ghost log entries" phenomenon and ensures the consistency among state machines when executing concurrently by limiting parallelism in the commitment of log entries. The correctness of ParallelRaft-CE is proved manually. Finally, the formal specifications of ParallelRaft-SE and ParallelRaft-CE are provided by TLA+ (TLA stands for temporal logic of actions), and the refinement mapping from ParallelRaft-SE to Multi-Paxos and the correctness of ParallelRaft-CE are verified using the TLC model checker when the number of participants of the protocols is small.

Abstract:Robot Operating System (ROS) is an open-source, meta-operating system, which can provide a structured communication layer based on the message mechanism on heterogeneous computing clusters. To improve the unsatisfactory real-time performance and reliability of data distribution in ROS1, ROS2 is proposed with a data flow-oriented data distribution service mechanism. This study validates the real-time performance and reliability of the ROS2 data distribution mechanism by means of probabilistic model checking. Firstly, a formal validation framework is put forward for the data flow-oriented ROS2 data distribution service system, and the probabilistic timed automata model is set up for the communication system module. Secondly, the probabilistic model checker PRISM is used to verify the real-time performance and reliability of data flow-oriented ROS2 data distribution service through the analysis of data loss rate and system response time. Finally, depending on the retransmission mechanism and Quality of Service (QoS) policy analysis, different data requirements and quantitative performance analysis of the transmission mode are achieved through the setting and adjustment of QoS parameters. This study can provide references for ROS2 application designers and the formal modeling, validation, and quantitative performance analysis of the distributed data distribution service based on the data flow.