In this paper, we report on the formal, machine-verified operating system - ORIENTAIS. ORIENTAIS is an OSEK/VDX standard based real-time operating system for automotive applications. About 8000 lines of C and 60 lines of assembler are comprised in the ORIENTAIS. The operating system is of vital importance to embedded systems, especially for some time sensitive and accurate controlling applications just like automotive applications. We prove that the implementation of ORIENTAIS application programming interfaces strictly follow the OSEK/VDX specification which we formalized from natural language expressed OSEK/VDX specification. Meanwhile, we model the high level interaction behaviors with CSP and verify the properties just like deadlock-free. To guarantee the safety of memory access and bounded response time with interrupt program involved, binary code level verification is developed based on xBIL which is a binary intermediate language we proposed. We introduce a series of techniques and approaches for verifying the ORIENTAIS. Our approach is an efficient work for the verification of ORIENTAIS, with whose help several bugs are detected. Now, ORIENTAIS has been certificated by OSEK certification group and installed on more than 1.38 million cars in China.

The POSIX threads (Pthreads) library is a thread API for C/C++ to control parallel threads and spawn concurrent process flows. Programming in Pthreads usually suffers from undesirable deadlock, data race, and race condition problems due to the potential nondeterministic execution behaviors between parallel threads. Dthreads, as another multithreading model that re‐implements Pthreads, was proposed by Liu et al for efficient deterministic multithreading. They found out that, under specific test cases, Dthreads can effectively prevent data races. However, no comparison test has been made with Pthreads.To perform a formal comparison between Pthreads and Dthreads over deadlocks, data races, and race conditions, in this paper, we adopt CSP (communicating sequential processes) as a formal model for specifying part of API functions in Pthreads and Dthreads and illustrate the model construction using 4 classical example programs. By feeding the models into the model checker PAT (process analysis toolkit), we have verified that deadlocks and data races exist in Pthreads, but do not exist in Dthreads, for the considered programs. We have also found that neither of them can prevent race conditions. Our comparative modelling and verification of Pthreads and Dthreads show that though Dthreads cannot prevent all the deadlock situations, shown by verification results of another 2 example programs, Dthreads is better than Pthreads on eliminating data races and preventing deadlocks. Considering limited scalability of Dthreads, we have introduced a new programming model to support coarse granularity in bank transfer. Our modelling is also extended by covering the synchronization operations in Liu et al work.

The POSIX threads (Pthreads) library is a thread API for C/C++ to control parallel threads and spawn concurrent process flows. Programming in Pthreads usually suffers from undesirable deadlock and data race problems due to the potential non-deterministic execution behaviors between parallel threads. Dthreads is another multithreading model re-implementing Pthreads, which was proposed by Liu et al. for efficient deterministic multithreading. Under specific test cases, they found out that Dthreads can effectively prevent data races. But they have not made comparison test with Pthreads. In order to formally compare Pthreads with Dthreads over deadlocks and data races, in this paper, we apply CSP (Communicating Sequential Processes) to model part of APIs in Pthreads and Dthreads, as well as two classical example programs. By using the model checker PAT (Process Analysis Toolkit), for our considered examples, we verify that deadlocks and data races exist in Pthreads, but do not exist in Dthreads. Our comparative modeling and verification of Pthreads and Dthreads show that Dthreads is better than Pthreads on eliminating data races and preventing deadlocks.

For hybrid systems, hybrid automata based tools are capable of verification while Matlab Simulink/Stateflow is proficient in simulation. In this paper, a methodology is developed in which the formal verification tool PHAVer and simulation tool Matlab are integrated to analyze and verify hybrid systems. For application of this methodology, a Platform Screen Doors System (abbreviated as PSDS), a subsystem of the subway, is modeled with formal verification techniques based on hybrid automata and Matlab Simulink/Stateflow charts, respectively. The models of PSDS are simulated by Matlab and verified by PHAVer. It is verified that the sandwich situation can be avoided under time interval conditions. We conclude that this integration methodology is competent in verifying Platform Screen Doors System.