Catálogo de publicaciones - libros

When monitoring a system wrt a property defined in some temporal logic, e.g., LTL, a major concern is to settle with an adequate interpretation of observable system events; that is, models of temporal logic formulae are usually infinite streams of events, whereas at runtime only prefixes are available.

This work defines a four-valued semantics for LTL over finite traces, which extends the classical semantics, and allows to infer whether a system behaves (1) according to the monitored property, (2) violates the property, (3) will possibly violate the property in the future, or (4) will possibly conform to the property in the future, once the system has stabilised. Notably, (1) and (2) correspond to the classical semantics of LTL, whereas (3) and (4) are chosen whenever an observed system behaviour has not yet lead to a violation or acceptance of the monitored property.

Moreover, we present a monitor construction for RV-LTL properties in terms of a Moore machine signalising the semantics of the so far obtained execution trace.

Abstraction is intensively used in the verification of large, complex or infinite-state systems. With abstractions getting more complex it is often difficult to see whether they are valid. However, for using abstraction in model checking it has to be ensured that properties are preserved. In this paper, we use a translation validation approach to verify property preservation of system abstractions. We formulate a correctness criterion based on simulation between concrete and abstract system for a property to be verified. For each distinct run of the abstraction procedure the correctness is verified in the theorem prover Isabelle/HOL. This technique is applied in the verification of adaptive embedded systems.

A significant number of cyber assaults and intrusion attempts are made against open source software written in C, C++, or Java. Detecting all flaws in a large system is still a daunting, unrealistic task. The information assurance area known as ”intrusion detection” (ID) senses unauthorized access attempts by monitoring key pieces of system data. There is a desire to at least detect intrusion attempts in order to stop them while in progress, or repair the damage at a later date. Most ID systems examine system log files, or monitor network traffic. This research presents a new approach to generating records for intrusion detection by means of instrumentation. Open source code such as a web server can be compiled and the execution path of the server can be observed externally in near real-time. This method thus creates a new data source for ID which can be incorporated into a discovery system.

Probabilistic correctness is an important aspect of reliable systems. A soft real-time system, for instance, may be designed to tolerate some degree of deadline misses under a threshold. Since probabilistic systems may behave differently from their probabilistic models depending on their current environments, checking the systems at runtime can provide another level of assurance for their probabilistic correctness. This paper presents a statistical runtime verification for probabilistic properties using statistical analysis. However, while this statistical analysis collects a number of execution paths as samples to check probabilistic properties within some certain error bounds, runtime verification can only produce one single sample. This paper provides a technique to produce such a number of samples and applies this methodology to check probabilistic properties in wireless sensor network applications.

We extend our previous approach to runtime verification of a single finite path against a formula in Next-free Linear-Time Logic (LTL) . The existing approach is extended from event-based to set-based states, and the design-space of quantification is discussed. By introducing a binary operator that values based on the current state, we can dispense with the static analysis of a formula. The binding semantics of propositions containing quantified variables is simplified by a pure top-down evaluation. The corresponding to a formula is evaluated in a breadth-first manner, allowing us to instantly detect refuted formulae during execution.

We introduce a new non-interference criterion for concurrent programs: rollback atomicity. Similarly to other definitions of atomicity, rollback atomicity of a given concurrent execution requires that there be a matching serial execution. Rollback atomicity differs from other definitions of atomicity in two key regards. First, it is formulated as a special case of view refinement. As such, it requires a correspondence between the states of a concurrent and a serial execution for each atomic block rather than only at quiescent states. Second, it designates a subset of shared variables as peripheral and has more relaxed requirements for peripheral variables than previous non-interference criteria.

In this paper, we provide the motivation for rollback atomicity. We formally define it and compare it with other notions of atomicity and non-interference criteria. We built a runtime checker for rollback atomicity integrated into the refinement checking tool, VYRD. This implementation was able to verify that concurrent executions of our motivating example are rollback atomic.

The process of verifying that a program conforms to its specification is often hampered by errors in both the program and the specification. A runtime checker that can evaluate formal specifications can be useful for quickly identifying such errors. This paper describes our preliminary experience with incorporating run-time checking into the Jahob verification system and discusses some lessons we learned in this process. One of the challenges in building a runtime checker for a program verification system is that the language of invariants and assertions is designed for simplicity of semantics and tractability of proofs, and not for run-time checking. Some of the more challenging constructs include existential and universal quantification, set comprehension, specification variables, and formulas that refer to past program states. In this paper, we describe how we handle these constructs in our runtime checker, and describe directions for future work.