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

Hui Ding, Can Zheng, Gul A Agha, Lui Raymond Sha

Research output: Contribution to journalConference article

Abstract

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.

Original languageEnglish (US)
Article number1410960
Pages (from-to)171-178
Number of pages8
JournalProceedings - International Workshop on Object-Oriented Real-Time Dependable Systems, WORDS
DOIs
StatePublished - Dec 1 2003
Event2003 9th IEEE International Workshop on Object-Oriented Real-Time Dependable Systems, WORDS 2003F - Anacapri, Italy
Duration: Oct 1 2003Oct 3 2003

ASJC Scopus subject areas

  • Engineering(all)

Fingerprint Dive into the research topics of 'Automated verification of the dependability of object-oriented real-time systems'. Together they form a unique fingerprint.

  • Cite this