|
Formal Methods in System Design
Journal Prestige (SJR): 0.445  Citation Impact (citeScore): 2 Number of Followers: 6  Hybrid journal (It can contain Open Access articles)ISSN (Print) 1572-8102 - ISSN (Online) 0925-9856 Published by Springer-Verlag  [2469 journals]
|
- Cut-off theorems for the PV-model
-
Free pre-print version: Loading...
Abstract: Abstract For a PV thread T which accesses a set \(\mathcal {R}\) of resources, each with a maximal capacity \(\kappa :\mathcal {R}\rightarrow {\mathbb {N}}\) , the PV-program \(T^n\) , where n copies of T are run in parallel, is deadlock free for all n if and only if \(T^M\) is deadlock free where M is the sum of the capacities of the shared resources \(M=\Sigma _{r\in \mathcal {R}}\kappa (r)\) . This is a sharp bound: For all \(\kappa :\mathcal {R}\rightarrow {\mathbb {N}}\) and finite \(\mathcal {R}\) there is a thread T using these resources such that \(T^M\) has a deadlock, but \(T^n\) does not for \(n<M\) . Moreover, we prove a more general theorem for a set of different threads sharing resources \(\mathcal {R}\) : There are no deadlocks in \(p=T1 T2 \cdots Tn\) if and only if there are no deadlocks in \(T_{i_1} T_{i_2} \cdots T_{i_M}\) for any M-element subset \(\{i_1,\ldots ,i_M\}\subset [1:n]\) . For \(\kappa (r)\equiv 1\) , \(T^n\) is serializable, i.e., all executions are equivalent to serial executions, for all n if and only if \(T^2\) is serializable. For general capacities, we define local obstructions to serializability—if no such obstruction exists, the program is serializable. There is no local obstruction to serializability in \(T^n\) for all n if and only if there is no local obstruction to serializability in \(T^M\) for \(M=\Sigma _{r\in \mathcal {R}}\kappa (r)+1\) . The obstructions may be found using a deadlock algorithm in \(T^{M+1}\) . There is a generalization to \(p=T1 T2 \cdots Tn\) : If there are no local obstructions to serializability in any of the sub programs, \(T_{i_1} T_{i_2} \cdots T_{i_M}\) , then p is serializable.
PubDate: 2022-06-15
-
- The complexity gap in the static analysis of cache accesses grows if
procedure calls are added-
Free pre-print version: Loading...
Abstract: Abstract The static analysis of cache accesses consists in correctly predicting which accesses are hits or misses. While there exist good exact and approximate analyses for caches implementing the least recently used (LRU) replacement policy, such analyses were harder to find for other replacement policies. A theoretical explanation was found: for an appropriate setting of analysis over control-flow graphs, cache analysis is PSPACE-complete for all common replacement policies (FIFO, PLRU, NMRU) except for LRU, for which it is only NP-complete. In this paper, we show that if procedure calls are added to the control flow, then the gap widens: analysis remains NP-complete for LRU, but becomes EXPTIME-complete for the three other policies. For this, we improve on earlier results on the complexity of reachability problems on Boolean programs with procedure calls. In addition, for the LRU policy we derive a backtracking algorithm as well as an approach for using it as a last resort after other analyses have failed to conclude.
PubDate: 2022-05-13
-
- Practical algebraic calculus and Nullstellensatz with the checkers Pacheck
and Pastèque and Nuss-Checker-
Free pre-print version: Loading...
Abstract: Abstract Automated reasoning techniques based on computer algebra have seen renewed interest in recent years and are for example heavily used in formal verification of arithmetic circuits. However, the verification process might contain errors. Generating and checking proof certificates is important to increase the trust in automated reasoning tools. For algebraic reasoning, two proof systems, Nullstellensatz and polynomial calculus, are available and are well-known in proof complexity. A Nullstellensatz proof captures whether a polynomial can be represented as a linear combination of a given set of polynomials by providing the co-factors of the linear combination. Proofs in polynomial calculus dynamically capture that a polynomial can be derived from a given set of polynomials using algebraic ideal theory. In this article we present the practical algebraic calculus as an instantiation of the polynomial calculus that can be checked efficiently. We further modify the practical algebraic calculus and gain LPAC (practical algebraic calculus + linear combinations) that includes linear combinations. In this way we are not only able to represent both Nullstellensatz and polynomial calculus proofs, but we are also able to blend both proof formats. Furthermore, we introduce extension rules to simulate essential rewriting techniques required in practice. For efficiency we also make use of indices for existing polynomials and include deletion rules too. We demonstrate the different proof formats on the use case of arithmetic circuit verification and discuss how these proofs can be produced as a by-product in formal verification. We present the proof checkers Pacheck, Pastèque, and Nuss-Checker. Pacheck checks proofs in practical algebraic calculus more efficiently than Pastèque, but the latter is formally verified using the proof assistant Isabelle/HOL. The tool Nuss-Checker is used to check proofs in the Nullstellensatz format.
PubDate: 2022-04-11
DOI: 10.1007/s10703-022-00391-x
-
- Parameterized verification of leader/follower systems via first-order
temporal logic-
Free pre-print version: Loading...
Abstract: We introduce a framework for the verification of protocols involving a distinguished machine (referred to as a leader) orchestrating the operation of an arbitrary number of identical machines (referred to as followers) in a network. At the core of our framework is a high-level formalism capturing the operation of these types of machines together with their network interactions. We show that this formalism automatically translates to a tractable form of first-order temporal logic. Checking whether a protocol specified in our formalism satisfies a desired property (expressible in temporal logic) then amounts to checking whether the protocol’s translation in first-order temporal logic entails that property. Many different types of protocols used in practice, such as cache coherence, atomic commitment, consensus, and synchronization protocols, fit within our framework. First-order temporal logic also facilitates parameterized verification by enabling us to model such protocols abstractly without referring to individual machines.
PubDate: 2022-03-15
DOI: 10.1007/s10703-022-00390-y
-
- Special Issue on Syntax-Guided Synthesis Preface
-
Free pre-print version: Loading...
PubDate: 2022-02-28
DOI: 10.1007/s10703-021-00386-0
-
- Debug-localize-repair: a symbiotic construction for heap manipulations
-
Free pre-print version: Loading...
Abstract: We present Wolverine2, an integrated Debug-Localize-Repair environment for heap manipulating programs. Wolverine2 provides an interactive debugging environment: while concretely executing a program via on an interactive shell supporting common debugging facilities, Wolverine2 displays the abstract program states (as box-and-arrow diagrams) as a visual aid to the programmer, packages a novel, proof-directed repair algorithm to quickly synthesize the repair patches and a new bug localization algorithm to reduce the search space of repairs. Wolverine2 supports “hot-patching” of the generated patches to provide a seamless debugging environment, and also facilitates new debug-localize-repair possibilities: specification refinement and checkpoint-based hopping. We evaluate Wolverine2 on 6400 buggy programs (generated using automated fault injection) on a variety of data-structures like singly, doubly, and circular linked lists, AVL trees, Red-Black trees, Splay Trees and Binary Search Trees; Wolverine2 could repair all the buggy instances within realistic programmer wait-time (less than 5 s in most cases). Wolverine2 could also repair more than 80% of the 247 (buggy) student submissions where a reasonable attempt was made.
PubDate: 2022-02-08
DOI: 10.1007/s10703-021-00387-z
-
- Incremental design-space model checking via reusable reachable state
approximations-
Free pre-print version: Loading...
Abstract: Abstract The design of safety-critical systems often requires design space exploration: comparing several system models that differ in terms of design choices, capabilities, and implementations. Model checking can compare different models in such a set, however, it is continuously challenged by the state space explosion problem. Therefore, learning and reusing information from solving related models becomes very important for future checking efforts. For example, reusing variable ordering in BDD-based model checking leads to substantial performance improvement. In this paper, we present a SAT-based algorithm for checking a set of models. Our algorithm, FuseIC3, extends IC3 to minimize time spent in exploring the common state space between related models. Specifically, FuseIC3 accumulates artifacts from the sequence of over-approximated reachable states, called frames, from earlier runs when checking new models, albeit, after careful repair. It uses bidirectional reachability; forward reachability to repair frames, and IC3-type backward reachability to block predecessors to bad states. We extensively evaluate FuseIC3 over a large collection of challenging benchmarks. FuseIC3 is on-average up to 5.48 \(\times \) (median 1.75 \(\times \) ) faster than checking each model individually, and up to 3.67 \(\times \) (median 1.72 \(\times \) ) faster than the state-of-the-art incremental IC3 algorithm. Moreover, we evaluate the performance improvement of FuseIC3 by smarter ordering of models and property grouping using a linear-time hashing approach.
PubDate: 2022-02-05
DOI: 10.1007/s10703-022-00389-5
-
- Colored nested words
-
Free pre-print version: Loading...
Abstract: Abstract Nested words allow modeling of linear and hierarchical structure in data, and nested word automata are special kinds of pushdown automata whose push/pop actions are directed by the hierarchical structure in the input nested word. The resulting class of regular languages of nested words has many appealing theoretical properties, and has found many applications, including model checking of procedural programs. In the nested word model, the hierarchical matching of open- and close- tags must be properly nested, and this is not the case, for instance, in program executions in presence of exceptions. This limitation of nested words narrows its model checking applications to programs with no exceptions. We introduce the model of colored nested words which allows such hierarchical structures with mismatches. We say that a language of colored nested words is regular if the language obtained by inserting the missing closing tags is a well-colored regular language of nested words. We define an automata model that accepts regular languages of colored nested words. These automata can execute restricted forms of \(\varepsilon \) -pop/push transitions. We provide an equivalent grammar characterization and show that the class of regular languages of colored nested words has the same appealing closure and decidability properties as nested words, thus removing the restriction of programs to be exception-free in order to be amenable for model checking, via the nested words paradigm.
PubDate: 2022-01-20
DOI: 10.1007/s10703-021-00384-2
-
- Distributed bounded model checking
-
Free pre-print version: Loading...
Abstract: Abstract Program verification is a resource-hungry task. This paper looks at the problem of parallelizing SMT-based automated program verification, specifically bounded model-checking, so that it can be distributed and executed on a cluster of machines. We present an algorithm that dynamically unfolds the call graph of the program and frequently splits it to create sub-tasks that can be solved in parallel. The algorithm is adaptive, controlling the splitting rate according to available resources, and also leverages information from the SMT solver to split where most complexity lies in the search. We implemented our algorithm by modifying Corral, the verifier used by Microsoft’s Static Driver Verifier (SDV), and evaluate it on a series of hard SDV benchmarks.
PubDate: 2022-01-05
DOI: 10.1007/s10703-021-00385-1
-
- From LTL to unambiguous Büchi automata via disambiguation of
alternating automata-
Free pre-print version: Loading...
Abstract: Abstract Due to the high complexity of translating linear temporal logic (LTL) to deterministic automata, several forms of “restricted” nondeterminism have been considered with the aim of maintaining some of the benefits of deterministic automata, while at the same time allowing more efficient translations from LTL. One of them is the notion of unambiguity. This paper proposes a new algorithm for the generation of unambiguous Büchi automata (UBA) from LTL formulas. Unlike other approaches it is based on a known translation from very weak alternating automata (VWAA) to NBA. A notion of unambiguity for alternating automata is introduced and it is shown that the VWAA-to-NBA translation preserves unambiguity. Checking unambiguity of VWAA is determined to be PSPACE-complete, both for the explicit and symbolic encodings of alternating automata. The core of the LTL-to-UBA translation is an iterative disambiguation procedure for VWAA. Several heuristics are introduced for different stages of the procedure. We report on an implementation of our approach in the tool Duggi and compare it to an existing LTL-to-UBA implementation in the SPOT tool set. Our experiments cover model checking of Markov chains, which is an important application of UBA.
PubDate: 2021-12-15
DOI: 10.1007/s10703-021-00379-z
-
- Extended bounded response LTL: a new safety fragment for efficient
reactive synthesis-
Free pre-print version: Loading...
Abstract: Abstract Reactive synthesis is a key technique for the design of correct-by-construction systems, which has been thoroughly investigated in the last decades. It consists of the synthesis of a controller that reacts to environment’s inputs satisfying a given temporal logic specification. Common approaches are based on the explicit construction of automata and on their determinization, which limits their scalability. In this paper, we introduce a new safety fragment of Linear Temporal Logic (LTL), called Extended Bounded Response LTL ( \({\textsf {LTL}}_{{\textsf {EBR}}}\) ), which allows one to combine bounded and universal unbounded temporal operators (thus covering a large set of practical cases). We show that reactive synthesis from \({\textsf {LTL}}_{{\textsf {EBR}}}\) specifications can be reduced to solving a safety game over a deterministic symbolic automaton built directly from the specification. We prove the correctness of the approach and study the complexity of the fragment showing that the proposed solution is optimal. Finally, we evaluate it on various benchmarks showing better performance of other approaches for general LTL or larger safety fragments.
PubDate: 2021-11-04
DOI: 10.1007/s10703-021-00383-3
-
- Formal methods: practical applications and foundations
-
Free pre-print version: Loading...
PubDate: 2021-10-01
DOI: 10.1007/s10703-021-00380-6
-
- Static analysis for detecting high-level races in RTOS kernels
-
Free pre-print version: Loading...
Abstract: Abstract We propose a static analysis based approach for detecting high-level races in RTOS kernels popularly used in safety-critical embedded software. High-Level races are indicators of atomicity violations and can lead to erroneous software behaviour with serious consequences. Hitherto techniques for detecting high-level races have relied on model-checking approaches, which are inefficient and apriori unsound. In contrast we propose a technique based on static analysis that is both efficient and sound. The technique is based on the notion of disjoint blocks recently introduced in Chopra et al. (In: Proceedings of 28th European symposium on programming (ESOP), Prague, Czech Republic. LNCS, vol 11423, pp 1–27. Springer, 2019). We evaluate our technique on four popular RTOS kernels and show that it is effective in detecting races, many of them harmful, with a high rate of precision.
PubDate: 2021-10-01
DOI: 10.1007/s10703-020-00354-0
-
- Information-flow control on ARM and POWER multicore processors
-
Free pre-print version: Loading...
Abstract: Abstract Weak memory models implemented on modern multicore processors are known to affect the correctness of concurrent code. They can also affect whether or not the concurrent code is secure. This is particularly the case in programs where the security levels of variables are value-dependent, i.e., depend on the values of other variables. In this paper, we illustrate how instruction reordering allowed by ARM and POWER multicore processors leads to vulnerabilities in such programs, and present a compositional, flow-sensitive information-flow logic which can be used to detect such vulnerabilities. The logic allows step-local reasoning (one instruction at a time) about a thread’s security by tracking information about dependencies between instructions which guarantee their order of occurrence. Program security can then be established from individual thread security using rely/guarantee reasoning. The logic has been proved sound with respect to existing operational semantics using Isabelle/HOL, and implemented in an automatic symbolic execution tool.
PubDate: 2021-10-01
DOI: 10.1007/s10703-021-00376-2
-
- Compositional verification of concurrent systems by combining
bisimulations-
Free pre-print version: Loading...
Abstract: Abstract One approach to verify a property expressed as a modal \(\mu \) -calculus formula on a system with several concurrent processes is to build the underlying state space compositionally (i.e., by minimizing and recomposing the state spaces of individual processes in a hierarchical way, keeping visible only the relevant actions occurring in the formula), and check the formula on the resulting state space. It was shown previously that, when checking the formulas of the \(L_{\mu }^{ dbr }\) fragment of the \(\mu \) -calculus (consisting of weak modalities only), individual processes can be minimized modulo divergence-preserving branching (divbranching for short) bisimulation. In this paper, we refine this approach to handle formulas containing both strong and weak modalities, so as to enable a combined use of strong or divbranching bisimulation minimization on concurrent processes depending whether they contain or not the actions occurring in the strong modalities of the formula. We extend \(L_{\mu }^{ dbr }\) with strong modalities and show that the combined minimization approach preserves the truth value of formulas of the extended fragment. We implemented this approach on top of the CADP verification toolbox and demonstrated how it improves the capabilities of compositional verification on realistic examples of concurrent systems. In particular, we applied our approach to the verification problems of the RERS 2019 challenge and observed drastic reductions of the state space compared to the approach in which only strong bisimulation minimization is used, on formulas not preserved by divbranching bisimulation.
PubDate: 2021-10-01
DOI: 10.1007/s10703-021-00360-w
-
- Pegasus: sound continuous invariant generation
-
Free pre-print version: Loading...
Abstract: Abstract Continuous invariants are an important component in deductive verification of hybrid and continuous systems. Just like discrete invariants are used to reason about correctness in discrete systems without having to unroll their loops, continuous invariants are used to reason about differential equations without having to solve them. Automatic generation of continuous invariants remains one of the biggest practical challenges to the automation of formal proofs of safety for hybrid systems. There are at present many disparate methods available for generating continuous invariants; however, this wealth of diverse techniques presents a number of challenges, with different methods having different strengths and weaknesses. To address some of these challenges, we develop Pegasus: an automatic continuous invariant generator which allows for combinations of various methods, and integrate it with the KeYmaera X theorem prover for hybrid systems. We describe some of the architectural aspects of this integration, comment on its methods and challenges, and present an experimental evaluation on a suite of benchmarks.
PubDate: 2021-10-01
DOI: 10.1007/s10703-020-00355-z
-
- Abstraction and subsumption in modular verification of C programs
-
Free pre-print version: Loading...
Abstract: The type-theoretic notions of existential abstraction, subtyping, subsumption, and intersection have useful analogues in separation-logic proofs of imperative programs. We have implemented these as an enhancement of the verified software toolchain (VST). VST is an impredicative concurrent separation logic for the C language, implemented in the Coq proof assistant, and proved sound in Coq. For machine-checked functional-correctness verification of software at scale, VST embeds its expressive program logic in dependently typed higher-order logic (CiC). Specifications and proofs in the program logic can leverage the expressiveness of CiC—so users can overcome the abstraction gaps that stand in the way of top-to-bottom verification: gaps between source code verification, compilation, and domain-specific reasoning, and between different analysis techniques or formalisms. Until now, VST has supported the specification of a program as a flat collection of function specifications (in higher-order separation logic)—one proves that each function correctly implements its specification, assuming the specifications of the functions it calls. But what if a function has more than one specification? In this work, we exploit type-theoretic concepts to structure specification interfaces for C code. This brings modularity principles of modern software engineering to concrete program verification. Previous work used representation predicates to enable data abstraction in separation logic. We go further, introducing function-specification subsumption and intersection specifications to organize the multiple specifications that a function is typically associated with. As in type theory, if \(\phi \) is a
of \(\psi \) , that is \(\phi <:\psi \) , then \(x:\phi \) implies \(x:\psi \) , meaning that any function satisfying specification \(\phi \) can be used wherever a function satisfying \(\psi \) is demanded. Subsumption incorporates separation-logic framing and parameter adaptation, as well as step-indexing and specifications constructed via mixed-variance functors (needed for C’s function pointers).
PubDate: 2021-10-01
DOI: 10.1007/s10703-020-00353-1
-
- Gray-box monitoring of hyperproperties with an application to privacy
-
Free pre-print version: Loading...
Abstract: Abstract Runtime verification is a complementary approach to testing, model checking and other static verification techniques to verify software properties. Monitorability characterizes what can be verified (monitored) at run time. Different definitions of monitorability have been given both for trace properties and for hyperproperties (properties defined over sets of traces), but these definitions usually cover only some aspects of what is important when characterizing the notion of monitorability. The first contribution of this paper is a refinement of classic notions of monitorability both for trace properties and hyperproperties, taking into account, among other things, the computability of the monitor. A second contribution of our work is to show that black-box monitoring of HyperLTL (a logic for hyperproperties) is in general unfeasible, and to suggest a gray-box approach in which we combine static and runtime verification. The main idea is to call a static verifier as an oracle at run time allowing, in some cases, to give a final verdict for properties that are considered to be non-monitorable under a black-box approach. Our third contribution is the instantiation of this solution to a privacy property called distributed data minimization which cannot be verified using black-box runtime verification. We use an SMT-based static verifier as an oracle at run time. We have implemented our gray-box approach for monitoring data minimization into the proof-of-concept tool Minion. We describe the tool and apply it to a few case studies to show its feasibility.
PubDate: 2021-10-01
DOI: 10.1007/s10703-020-00358-w
-
- Integrating formal specifications into applications: the ProB Java API
-
Free pre-print version: Loading...
Abstract: Abstract The common formal methods workflow consists of formalising a model followed by applying model checking and proof techniques. Once an appropriate level of certainty is reached, code generators are used in order to gain executable code. In this paper, we propose a different approach: instead of generating code from formal models, it is also possible to embed a model checker or animator into applications in order to use the formal models themselves at runtime. We present a Java API to the ProB animator and model checker. We describe several case studies that use this API as enabling technology to interact with a formal specification at runtime.
PubDate: 2021-10-01
DOI: 10.1007/s10703-020-00351-3
-
- Automatic verification of concurrent stochastic systems
-
Free pre-print version: Loading...
Abstract: Abstract Automated verification techniques for stochastic games allow formal reasoning about systems that feature competitive or collaborative behaviour among rational agents in uncertain or probabilistic settings. Existing tools and techniques focus on turn-based games, where each state of the game is controlled by a single player, and on zero-sum properties, where two players or coalitions have directly opposing objectives. In this paper, we present automated verification techniques for concurrent stochastic games (CSGs), which provide a more natural model of concurrent decision making and interaction. We also consider (social welfare) Nash equilibria, to formally identify scenarios where two players or coalitions with distinct goals can collaborate to optimise their joint performance. We propose an extension of the temporal logic rPATL for specifying quantitative properties in this setting and present corresponding algorithms for verification and strategy synthesis for a variant of stopping games. For finite-horizon properties the computation is exact, while for infinite-horizon it is approximate using value iteration. For zero-sum properties it requires solving matrix games via linear programming, and for equilibria-based properties we find social welfare or social cost Nash equilibria of bimatrix games via the method of labelled polytopes through an SMT encoding. We implement this approach in PRISM-games, which required extending the tool’s modelling language for CSGs, and apply it to case studies from domains including robotics, computer security and computer networks, explicitly demonstrating the benefits of both CSGs and equilibria-based properties.
PubDate: 2021-10-01
DOI: 10.1007/s10703-020-00356-y
-
