Abstract:Preface

Abstract:Time-point-interval prioritized time Petri nets were defined in our prior work to model and analyze real-time embedded multi-core systems, but they have the following flaws: (1) they only consider the case that the execution time of each task is a fixed value, but in many practical applications, the execution time of a task is generally within a range, and thus this kind of model cannot be used to analyze these applications; (2) there is no automatic transformation from the task dependency graph to this kind of model and thus it is inconvenient for engineering designers to use them; (3) the case of mutually exclusive access to shared variables is not considered in them. To make up the above flaws, we define Prioritized Time Petri Nets (Pri-TPNs), define Task Dependency Graph with Resource Allocation and Priority (TDG-RAP), propose the rules from a TDG-RAP to a Pri-TPN, and develop a related tool to analyze Worst-Case Execution Time (WCET) and deadlock automatically.

Abstract:Linearizability is universally accepted as a correctness criterion for concurrent objects. However, it has been shown that linearizability cannot be adopted as a correctness criterion for concurrent objects with random sentences. Thus, Golab et al. proposed the concept of strong linearizability, which adds prefix preservation properties based on the linearizability definition and has more constraints for concurrent objects. The research on strong linearizability focuses on the feasibility of generating strongly linearizable objects with certain basic objects, while only a few studies are about checking and verification of strong linearizability. We investigate strong linearizability from two aspects including the verification algorithm and the approach for proving non-strong linearizability of concurrent objects. First, we divide strong linearizability into fixed effective points and pure help and prove that the notion of fixed effective points is an extension of that of fixed linearizability points. Then, two verification algorithms for strong linearizability are put forward. One algorithm is based on checking the fixed linearizability points, and the other is based on the fixed effective points. Finally, an approach is provided for proving that the concurrent objects violate strong linearizability, and it helps verify that the Herlihy & Wing queue, a single-reader single-write register, and a snapshot object violate strong linearizability.

Abstract:Operating systems are the key foundational components of the software stacks employed in many safety-critical scenarios. A tiny error or loophole in the operating system may cause major failures of the overall software system, resulting in huge economic losses or endangering human lives. Thus, the correctness of the operating system should be verified to reduce the number of such accidents. Traditional testing methods cannot guarantee the exhaustive detection of potential errors in the target system. Therefore, it is necessary to adopt formal methods based on strict mathematical theories for verifying operating systems. In an operating system, mutexes are utilized to coordinate the access to shared resources by tasks and they are a typical means of task synchronization. The functional correctness of mutexes is the key to the correct functioning of multi-task applications. Based on the theorem proof method, we conduct formal verification on the code of the mutex module of a preemptive microkernel in the interactive theorem prover Coq, give the formal specifications of the interface functions of this module, and formally prove the functional correctness of these interface functions.

Abstract:As a recursive method for finding the optimal solution to a problem, dynamic programming mainly solves the original problem by first solving the subproblems and then combining their solutions. Due to a large number of dependencies and constraints among its subproblems, the validation procedure is laborious, and especially the correctness verification of imperative dynamic programming algorithms is a challenge. Based on the Isabelle/HOL functional modeling and verification of dynamic programming algorithms, we avoid dealing with complex dependencies and constraints in proving correctness by verifying the equivalence of imperative dynamic programming algorithms and their programs. Meanwhile, a framework for the design of imperative dynamic programming algorithmic programs and their mechanized verification are proposed. First, according to the optimization method (memo method) and properties (optimal substructure property and subproblems overlapping property) of dynamic programming algorithms, the problem specification is described, the recursive relations are inductively derived, and the loop invariants are formally constructed. Then, the IMP (minimalistic imperative programming language) code is generated based on the recursive relations. Second, the problem specification, loop invariants, and generated IMP code are fed into VCG (verification condition generator) to generate the verification conditions for correctness automatically. Additionally, the verification conditions are then mechanically verified in the Isabelle/HOL theorem prover. The algorithm is initially designed in the general form of an imperative dynamic programming algorithm and further instantiated to obtain specific algorithms. Finally, the effectiveness of the proposed framework is validated by case studies to provide references for automated derivation and verification of dynamic programming algorithms.

Abstract:Many complex embedded systems are Mixed-Criticality Systems (MCSs). MCSs are often required to operate with the specified criticality level, but they may be subject to hazards that can induce random errors and burst errors, which may result in the abortion of an executing thread or even system failures. Current research only concentrates on schedulability analysis for MCSs and fails to further analyze system safety and consider the dependency relationship among threads. Taking random errors and burst errors as the research objects, we propose an architecture-based MCS safety analysis method with the integration of fault propagation analysis. Meanwhile, Architecture Analysis and Design Language (AADL) is employed to characterize the dependency relations among components. To compensate for the shortcomings of AADL, we create new AADL properties (AADL burst error properties) and propose new thread state machine (burst error-based thread state machine) semantics to describe the thread execution process with burst errors. Additionally, model transformation rules and assembly methods are proposed to apply probabilistic model checking for safety analysis, and PRISM models are derived from AADL models. Two formulae are also formulated to obtain quantitative safety properties for verifying occurrence probabilities of failures, and qualitative safety properties for generating corresponding witnesses to figure out propagation paths for fault propagation analysis respectively. Finally, the effectiveness of the proposed method is verified by adopting a Power Boat Autopilot (PBA) system.