Modeling and Verifying Abstract Multithreaded Systems.
Winfried Grünewald, Klaus Schneider · 1998
Abstract. Multithreaded systems consist of programs (threads), an operating system and one or more processors. We describe abstraction techniques from programs, the operating system and processors to extract a finite state machine that reflects the thread manager in its system context. To assure the correctness and fairness of the concurrent execution, we apply common verification techniques, in particular CTL model checking and theorem proving in higher order logic. Additionally, requirements for interrupt service routines are derived. We illustrate the application of the method by verifying the thread management of the multithreaded Rhamma system. 1