Title :
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
fDate :
31 Aug.-3 Sept. 2004
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;
Conference_Titel :
Euromicro Conference, 2004. Proceedings. 30th
Print_ISBN :
0-7695-2199-1
DOI :
10.1109/EURMIC.2004.1333361
