Online, library-based visual formal specification monitoring system for monitoring log-files with visible and hidden data
Abstract
Runtime Monitoring (RM), also known as Runtime
Verification (RV), is the process of monitoring and
verifying the sequencing and temporal behavior of an underlying
application and comparing it to the correct behavior as
specified by a formal specification pattern. Hidden Markov
Model (HMM)-based RM enables the monitoring of systems
with both visible and hidden data, using the same
formal specifications used by deterministic RM. This paper
describes an online library of formal specification oracles and
an accompanying toolset for the runtime monitoring log-files
that contain hidden and visible data.
Description
The article of record as published may be found at http://link.springer.com/article/10.1007/s11334-016-0286-6
Rights
This publication is a work of the U.S. Government as defined in Title 17, United States Code, Section 101. Copyright protection is not available for this work in the United States.Collections
Related items
Showing items related by title, author, creator and subject.
-
Detecting malicious tweets in twitter using runtime monitoring with hidden information
Yilmaz, Abdullah (Monterey, California: Naval Postgraduate School, 2016-06);Although there is voluminous data flow in social media, it is still possible to create an effective system that can detect malicious activities within a shorter time and provide situational awareness. This thesis developed ... -
A Hidden Markov Model based Runtime Monitoring tool
Drusinsky, Doron (Monterey, California. Naval Postgraduate School, 2016-01); NPS-CS-16-001Runtime Monitoring (RM), also known as Runtime Verification (RV), is the process of monitoring and verifying the sequencing and temporal behavior of an underlying application and comparing it to the correct behavior as ... -
Formal specifications for an electrical power grid system stability and reliability
Galinski, Jonathan J. (Monterey, California: Naval Postgraduate School, 2015-09);This thesis provides natural language requirements and associated formal specifications for an electric power grid. These specifications are the first step in using bounded constraint solving to detect early bleak states ...