Model-checking middleware-based event-driven real-time embedded software

Xianghua Deng; Matthew B. Dwyer; John Hatcliff; Georg Jung; Robby; Gurdip Singh

doi:10.1007/978-3-540-39656-7_6

Model-checking middleware-based event-driven real-time embedded software

Xianghua Deng, Matthew B. Dwyer, John Hatcliff, Georg Jung, Robby, Gurdip Singh

Research output: Chapter in Book/Entry/Poem › Chapter

12 Scopus citations

Abstract

Component frameworks such as the CORBA Component Model (CCM) and middleware services such as the CORBA Event Service are increasingly being used to build safety / mission-critical distributed real-time embedded (DRE) systems. In this paper, we present a novel model-checking infrastructure for checking global temporal properties of DRE systems built on top of a Real-Time CORBA Event Service using CCM architectures. We describe how (a) building support for OO structures and communication layers directly in an extensible model-checker and (b) leveraging domain properties related to priorities, scheduling, and timing can dramatically reduce the costs of checking realistic systems.

Original language	English (US)
Title of host publication	Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Editors	Frank S. de Boer, Marcello M. Bonsangue, Susanne Graf, Willem-Paul de Roever
Publisher	Springer Verlag
Pages	154-181
Number of pages	28
ISBN (Print)	3540203036, 9783540203032
DOIs	https://doi.org/10.1007/978-3-540-39656-7_6
State	Published - 2003
Externally published	Yes

Publication series

Name	Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume	2852
ISSN (Print)	0302-9743
ISSN (Electronic)	1611-3349

ASJC Scopus subject areas

Theoretical Computer Science
General Computer Science

Access to Document

10.1007/978-3-540-39656-7_6

Cite this

Deng, X., Dwyer, M. B., Hatcliff, J., Jung, G., Robby, & Singh, G. (2003). Model-checking middleware-based event-driven real-time embedded software. In F. S. de Boer, M. M. Bonsangue, S. Graf, & W.-P. de Roever (Eds.), Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (pp. 154-181). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 2852). Springer Verlag. https://doi.org/10.1007/978-3-540-39656-7_6

Model-checking middleware-based event-driven real-time embedded software. / Deng, Xianghua; Dwyer, Matthew B.; Hatcliff, John et al.
Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). ed. / Frank S. de Boer; Marcello M. Bonsangue; Susanne Graf; Willem-Paul de Roever. Springer Verlag, 2003. p. 154-181 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 2852).

Research output: Chapter in Book/Entry/Poem › Chapter

Deng, X, Dwyer, MB, Hatcliff, J, Jung, G, Robby & Singh, G 2003, Model-checking middleware-based event-driven real-time embedded software. in FS de Boer, MM Bonsangue, S Graf & W-P de Roever (eds), Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 2852, Springer Verlag, pp. 154-181. https://doi.org/10.1007/978-3-540-39656-7_6

Deng X, Dwyer MB, Hatcliff J, Jung G, Robby, Singh G. Model-checking middleware-based event-driven real-time embedded software. In de Boer FS, Bonsangue MM, Graf S, de Roever WP, editors, Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). Springer Verlag. 2003. p. 154-181. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)). doi: 10.1007/978-3-540-39656-7_6

Deng, Xianghua ; Dwyer, Matthew B. ; Hatcliff, John et al. / Model-checking middleware-based event-driven real-time embedded software. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). editor / Frank S. de Boer ; Marcello M. Bonsangue ; Susanne Graf ; Willem-Paul de Roever. Springer Verlag, 2003. pp. 154-181 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).

@inbook{dea1cf4138ca4411845fd8fe66622a25,

title = "Model-checking middleware-based event-driven real-time embedded software",

abstract = "Component frameworks such as the CORBA Component Model (CCM) and middleware services such as the CORBA Event Service are increasingly being used to build safety / mission-critical distributed real-time embedded (DRE) systems. In this paper, we present a novel model-checking infrastructure for checking global temporal properties of DRE systems built on top of a Real-Time CORBA Event Service using CCM architectures. We describe how (a) building support for OO structures and communication layers directly in an extensible model-checker and (b) leveraging domain properties related to priorities, scheduling, and timing can dramatically reduce the costs of checking realistic systems.",

author = "Xianghua Deng and Dwyer, {Matthew B.} and John Hatcliff and Georg Jung and Robby and Gurdip Singh",

year = "2003",

doi = "10.1007/978-3-540-39656-7_6",

language = "English (US)",

isbn = "3540203036",

series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",

publisher = "Springer Verlag",

pages = "154--181",

editor = "{de Boer}, {Frank S.} and Bonsangue, {Marcello M.} and Susanne Graf and {de Roever}, Willem-Paul",

booktitle = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",

}

TY - CHAP

T1 - Model-checking middleware-based event-driven real-time embedded software

AU - Deng, Xianghua

AU - Dwyer, Matthew B.

AU - Hatcliff, John

AU - Jung, Georg

AU - Robby,

AU - Singh, Gurdip

PY - 2003

Y1 - 2003

N2 - Component frameworks such as the CORBA Component Model (CCM) and middleware services such as the CORBA Event Service are increasingly being used to build safety / mission-critical distributed real-time embedded (DRE) systems. In this paper, we present a novel model-checking infrastructure for checking global temporal properties of DRE systems built on top of a Real-Time CORBA Event Service using CCM architectures. We describe how (a) building support for OO structures and communication layers directly in an extensible model-checker and (b) leveraging domain properties related to priorities, scheduling, and timing can dramatically reduce the costs of checking realistic systems.

AB - Component frameworks such as the CORBA Component Model (CCM) and middleware services such as the CORBA Event Service are increasingly being used to build safety / mission-critical distributed real-time embedded (DRE) systems. In this paper, we present a novel model-checking infrastructure for checking global temporal properties of DRE systems built on top of a Real-Time CORBA Event Service using CCM architectures. We describe how (a) building support for OO structures and communication layers directly in an extensible model-checker and (b) leveraging domain properties related to priorities, scheduling, and timing can dramatically reduce the costs of checking realistic systems.

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

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

U2 - 10.1007/978-3-540-39656-7_6

DO - 10.1007/978-3-540-39656-7_6

M3 - Chapter

AN - SCOPUS:0142183392

SN - 3540203036

SN - 9783540203032

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 154

EP - 181

BT - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

A2 - de Boer, Frank S.

A2 - Bonsangue, Marcello M.

A2 - Graf, Susanne

A2 - de Roever, Willem-Paul

PB - Springer Verlag

ER -

Model-checking middleware-based event-driven real-time embedded software

Abstract

Publication series

ASJC Scopus subject areas

Access to Document

Other files and links

Fingerprint

Cite this