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

Fingerprint

Model checking
Real time systems
Semantics
Specifications

ASJC Scopus subject areas

  • Engineering(all)

Cite this

@article{fadc5728a7394651b691964eb559f839,
title = "Automated verification of the dependability of object-oriented real-time systems",
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.",
author = "Hui Ding and Can Zheng and Agha, {Gul A} and Sha, {Lui Raymond}",
year = "2003",
month = "12",
day = "1",
doi = "10.1109/WORDS.2003.1267505",
language = "English (US)",
pages = "171--178",
journal = "Proceedings - International Workshop on Object-Oriented Real-Time Dependable Systems, WORDS",
issn = "1530-1443",

}

TY - JOUR

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

AU - Ding, Hui

AU - Zheng, Can

AU - Agha, Gul A

AU - Sha, Lui Raymond

PY - 2003/12/1

Y1 - 2003/12/1

N2 - 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.

AB - 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.

UR - http://www.scopus.com/inward/record.url?scp=84883131864&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=84883131864&partnerID=8YFLogxK

U2 - 10.1109/WORDS.2003.1267505

DO - 10.1109/WORDS.2003.1267505

M3 - Conference article

AN - SCOPUS:84883131864

SP - 171

EP - 178

JO - Proceedings - International Workshop on Object-Oriented Real-Time Dependable Systems, WORDS

JF - Proceedings - International Workshop on Object-Oriented Real-Time Dependable Systems, WORDS

SN - 1530-1443

M1 - 1410960

ER -