Runtime verification is aimed at analyzing execution traces stemming from a running program or system. The traditional purpose is to detect the lack of conformance with respect to a formal specification. Numerous efforts in the field have focused on monitoring so-called parametric specifications, where events carry data, and formulas can refer to such. Since a monitor for such specifications has to store observed data, the challenge is to have an efficient representation and manipulation of Boolean operators, quantification, and lookup of data. The fundamental problem is that the actual values of the data are not necessarily bounded or provided in advance. In this work we explore the use of Binary Decision Diagrams (BDDs) for representing observed data. Our experiments show a substantial improvement in performance compared to related work.

Safety-critical systems need to maintain their functionality in the presence of multiple errors caused by component failures or disastrous environment events. We propose a game-theoretic foundation for synthesizing control strategies that maximize the resilience of a software system in defense against a realistic error model. The new control objective of such a game is called $k$ -resilience. In order to be $k$ -resilient, a system needs to rapidly recover from infinitely many waves of a small number of up to $k$ close errors provided that the blocks of up to $k$ errors are separated by short time intervals, which can be used by the system to recover. We first argue why we believe this to be the right level of abstraction for safety critical systems when local faults are few and far between. We then show how the analysis of $k$ -resilience problems can be formulated as a model-checking problem of a mild extension to the alternating-time $\mu$ -calculus (AMC). The witness for $k$ resilience, which can be provided by the model checker, can be used for providing control strategies that are optimal with respect to resilience. We show that the computational complexity of constructing such optimal control strategies is low and demonstrate the feasibility of our approach through an implementation and experimental results.

Concurrency theory suggests the use of fairness as a criterion for a reasonable execution: a transition or a process should not wait an unbounded amount of time to execute if it is enabled continuously (under weak fairness) or infinitely often (under strong fairness). Unlike multiprocessing, in actual concurrent systems one may rely on the physical nature of the system to act in a “fair” manner. However, in many realistic concurrent systems, performing the next transition may involve several smaller steps that can include negotiation and communication, and fairness can be hard to achieve. It is useful to be able to control the global fairness guaranteed by enforcing local constraints on processes. We define local fairness conditions and study their relationship with common notions of global fairness constraints.

Concurrent systems are prone to deadlocks that arise from competing access to shared resources and synchronization between the components. At the same time, concurrency leads to a dramatic increase of the possible state space due to interleavings of computations, which makes standard verification techniques often infeasible. Previous work has shown that approximating the state space of component based systems by computing invariants allows to verify much larger systems then standard methods that compute the exact state space. The approach comes with the drawback, though, that not all of the reported specification violations may be reachable in the system. This paper deals with that problem by combining the information from the invariant with model checking techniques and strategies for reducing the memory footprint. The approach is implemented as post processing step for generating the exact set of reachable specification violations along with traces to demonstrate the error.

Abstract We present a symbolic model checking approach that allows verifying a unit of code, e.g., a single procedure or a collection of procedures that interact with each other. We allow temporal specifications that assert over both theprogram countersand theprogram variables. We decompose the verification into two parts: (1) a search that is based on the temporal behavior of theprogram counters, and (2) the formulation and refutation of a path condition, which inherits conditions constraining theprogram variablesfrom the temporal specification. This verification approach is modular, as we do not require that all the involved procedures are provided. Furthermore, we do not request that the code is based on a finite domain. The presented approach can also be used for automating the generation of test cases for unit testing.

We extend the standard model checking paradigm of linear temporal logic, LTL, to a “model measuring” paradigm where one can obtain more quantitative information beyond a “Yes/No” answer. For this purpose, we define a parametric temporal logic , PLTL, which allows statements such as “a request p is followed in at most x steps by a response q ,” where x is a free variable. We show how one can, given a formula ***( x 1 ...,x k ) of PLTL and a system model K satisfies the property ***, but if so find valuations which satisfy various optimality criteria. In particular, we present algorithms for finding valuations which minimize (or maximize) the maximum (or minimum) of all parameters. Theses algorithms exhibit the same PSPACE complexity as LTL model checking. We show that our choice of syntax for PLTL lies at the threshold of decidability for parametric temporal logics, in that several natural extensions have undecidable “model measuring” problems.

The notions of serializability, linearizability, and sequential consistency are used in the specification of concurrent systems. We show that the model checking problem for each of these properties can be cast in terms of the containment of one regular language in another regular language shuffled using a semicommutative alphabet. The three model checking problems are shown to be, respectively, in P space , in E xpspace , and undecidable.

Modeling execution as partial orders increases the flexibility in reasoning about concurrent programs by allowing the use of alternative, equivalent execution sequences. This is a desirable feature in specifying concurrent systems which allows formalizing frequently used arguments such as ‘in an equivalent execution sequence’, or ‘in a consistent global state, not necessarily on the execution sequence’ to be formalized. However, due to the addition of structure to the model, verification of partial order properties is non-trivial and sparse. We present here a new approach which allows expressing and verifying partial order properties. It is based on modeling an execution as a linear sequence of global states, where each state is equipped with its past partial-order history. The temporal logic BPLTL (for Branching Past Linear Temporal Logic) is introduced. We provide a sound and relatively complete proof system for the logic BPLTL over transitions programs. Our proof system augments an existing proof system for LTL.

We have developed a formal validation tool that has been used on several projects that are developing software for AT&T's 5ESS™ telephone switching system. The tool uses Holzmann's supertrace algorithm to check for errors such as deadlock and livelock in networks of communicating processes. The validator invariably finds subtle errors that were missed during thorough simulation and testing; however, the brute-force search it performs can result in extremely long running times, which can be frustrating to users. Recently, a number of researchers have been investigating techniques known as partial-order methods that can significantly reduce the running time of formal validation by avoiding redundant exploration of execution scenarios. In this paper, we describe the design of a partial-order algorithm for our validation tool and discuss its effectiveness. We show that a careful compile-time static analysis of process communication behavior yields information that can be used during validation to dramatically improve its performance. We demonstrate the effectiveness of our partial-order algorithm by presenting the results of experiments with actual industrial examples drawn from a variety of 5ESS™ application domains, including call processing, signalling, and switch maintenance.

The notions of serializability, linearizability and sequential consistency are used in the specification of concurrent systems. We show that the model checking problem for each of these properties can be cast in terms of the containment of one regular language in another regular language shuffled using a semi-commutative alphabet. The three model checking problems are shown to be, respectively, in PSPACE, in EXPSPACE, and undecidable.

Formal validation is a powerful technique for automatically checking that a collection of communicating processes is free from concurrency-related errors. Although validation tools invariably find subtle errors that were missed during thorough simulation and testing, the brute-force search they perform can result in excessive memory usage and extremely long running times. Recently, a number of researchers have been investigating techniques known as partial-order methods that can significantly reduce the computational resources needed for formal validation by avoiding redundant exploration of execution scenarios. This paper investigates the behavior of partial-order methods in an industrial setting. We describe the design of a partial-order algorithm or a formal validation tool that has been used on several projects that are developing software for the Lucent Technologies 5ESS/sup (R/) telephone switching system. We demonstrate the effectiveness of the algorithm by presenting the results of experiments with actual industrial examples drawn from a variety of 5ESS application domains.

A temporal logic for causality (T/sub LC/) is introduced. The logic is interpreted over causal structures corresponding to partial order executions of programs. For causal structures describing the behavior of a finite fixed set of processes, a T/sub LC/-formula can, equivalently, be interpreted over their linearizations. The main result of the paper is a tableau construction that gives a singly-exponential translation from a T/sub LC/ formula /spl psi/ to a Streett automaton that accepts the set of linearizations satisfying /spl psi/. This allows both checking the validity of T/sub LC/ formulas and model-checking of program properties. As the logic T/sub LC/ does not distinguish among different linearizations of the same partial order execution, partial order reduction techniques can be applied to alleviate the state-space explosion problem of model-checking.

Serializability of database transactions is first defined within the framework of linear temporal logic. For commutativity-based serializability, an alternative specification is given in a temporal logic whose semantic interpretation is especially tailored for reasoning about equivalence sequences of histories. The alternative specification method is given in ISTL* and is limited to the specification of concurrency control algorithms based on commutativity. A formal verification system for serializability that uses classical logic reasoning is provided. Within it, proving serializability of transactions executing a concurrency control algorithm is done along the same lines as proving properties of concurrent programs. Serializability for the multiversion-timestamp algorithm is verified.>

A new temporal logic and interpretation are suggested which have features from linear temporal logic, branching time temporal logic, and partial order temporal logic.The new logic can describe properties essential to the specification and correctness proofs of distributed algorithms such as those for global snapshots.It is also appropriate for the justification of proof rules and giving temporal semantics to properties such as layering of a program.These properties cannot be described with existing temporal logics.The semantic model of the logic is based on a set of sets of interleaving sequences which reflect partial orders from the underlying semantics of the computational model.For the common partial order derived from sequential&y in execution of each process, the logic will distinguish between nondeterminism due to the parallel execution and nondeterminism due to local nondeterministic choices.The difference in expressive power is thus qualitative, and not merely due to the presence or absence of a particular temporal operator.In the logic, theorems are proven which clarify when it is possible to establish a property P for SGWZ~ of the interleaving computations, and yet conclude the truth of P for every interleaving.