Runtime verification of timing and probabilistic properties using WMI and .NET

Author

Jayaputera, Jane ; Poernomo, Iman ; Schmidt, Heinz

Author_Institution

CSSE, Monash Univ., Clayton, Vic., Australia

fYear

2004

fDate

31 Aug.-3 Sept. 2004

Firstpage

100

Lastpage

106

Abstract

Reliability and availability are key issues to distributed service-oriented systems. We present a methodology for run-time verification of reliability and availability properties for distributed architectures. Our approach generalizes the concept of design-by-contract to contracts involving time and probabilities. We define a language for contracts based on probabilistic real time computational tree logic (PCTL). We provide a formal semantics for this language based on possible execution traces of a system. Then we describe a .NET-based system for monitoring contracts, built upon the Windows Management Instrumentation (WMI) framework.

Keywords

application program interfaces; formal logic; formal specification; formal verification; network operating systems; probability; software architecture; software reliability; trees (mathematics); .NET-based system; WMI framework; Windows Management Instrumentation; design-by-contract; distributed architectures; distributed service-oriented systems; execution traces; probabilistic real time computational tree logic; run-time verification; Availability; Banking; Computer architecture; Contracts; Instruments; Monitoring; Probabilistic logic; Runtime; Technology management; Timing;

fLanguage

English

Publisher

ieee

Conference_Titel

Euromicro Conference, 2004. Proceedings. 30th

ISSN

1089-6503

Print_ISBN

0-7695-2199-1

Type

conf

DOI

10.1109/EURMIC.2004.1333361

Filename

1333361