Formally specified monitoring of temporal properties

Moonjoo Kim, M. Viswanathan, H. Ben-Abdallah, S. Kannan, I. Lee, O. Sokolsky

Research output: Chapter in Book/Report/Conference proceedingConference contribution


We describe the Monitoring and Checking (MaC) framework which provides assurance on the correctness of an execution of a real-time system at runtime. Monitoring is performed based on a formal specification of system requirements. MaC bridges the gap between formal specification, which analyzes designs rather than implementations, and testing, which validates implementations but lacks formality. An important aspect of the framework is a clear separation between implementation-dependent description of monitored objects and high-level requirements specification. Another salient feature is automatic instrumentation of executable code. The paper presents an overview of the framework, languages to express monitoring scripts and requirements, and a prototype implementation of MaC targeted at systems implemented in Java.

Original languageEnglish (US)
Title of host publicationProceedings of the 11th Euromicro Conference on Real-Time Systems, ECRTS 1999
Number of pages9
StatePublished - 1999
Externally publishedYes
Event11th Euromicro Conference on Real-Time Systems, ECRTS 1999 - York, United Kingdom
Duration: Jun 9 1999Jun 11 1999

Publication series

NameProceedings - Euromicro Conference on Real-Time Systems
ISSN (Print)1068-3070


Other11th Euromicro Conference on Real-Time Systems, ECRTS 1999
Country/TerritoryUnited Kingdom

ASJC Scopus subject areas

  • Software
  • Hardware and Architecture


Dive into the research topics of 'Formally specified monitoring of temporal properties'. Together they form a unique fingerprint.

Cite this