Formally specified monitoring of temporal properties
- 20 January 2003
- conference paper
- Published by Institute of Electrical and Electronics Engineers (IEEE)
- No. 10683070,p. 114-122
- https://doi.org/10.1109/emrts.1999.777457
Abstract
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.Keywords
This publication has 13 references indexed in Scilit:
- Efficient Run-time Monitoring Of Timing ConstraintsPublished by Institute of Electrical and Electronics Engineers (IEEE) ,2005
- The sentry systemPublished by Institute of Electrical and Electronics Engineers (IEEE) ,2003
- An approach to automatic detection of software failures in real-time systemsPublished by Institute of Electrical and Electronics Engineers (IEEE) ,2002
- Test automation for safety-critical systems: Industrial application and future developmentsPublished by Springer Nature ,1996
- On-line monitoring: a tutorialComputer, 1995
- Designing programs that check their workJournal of the ACM, 1995
- Concurrent runtime monitoring of formally specified programsComputer, 1993
- A specificational approach to high level program monitoring and measuringIEEE Transactions on Software Engineering, 1992
- The Temporal Logic of Reactive and Concurrent SystemsPublished by Springer Nature ,1992
- High-level debugging of distributed systems: The behavioral abstraction approachJournal of Systems and Software, 1983