Automated verification of the dependability of object-oriented real-time systems

We develop an effective approach to formally specify and automatically verify the dependability of object-oriented real-time systems based on the Actor model and Real-Time Maude. Our approach decomposes an application into functional components represented as concurrent objects or actors, and separately specifies the timing constraints using RTSynchronizer. It achieves the goal of automatically verifying the dependability and timing properties of the target system by implementing the operational semantics of Actor and RTSynchronizer in Real-Time Maude, which supports executable specification and various temporal model checking analysis. We demonstrate the effectiveness of our approach by an annotated case study of the Simplex architecture.