1,721,117 research outputs found
Abstract Model Checking without Computing the Abstraction
No full textAbstraction is a fundamental technique that enables the verification of large systems. In symbolic model checking, abstractions are defined by formulas that relate concrete and abstract variables. In predicate abstraction, the abstract variables are equivalent to some predicates over the concrete variables. In order to apply model checking on the abstract state space, it is usually necessary to compute a quantifier-free formula that is equivalent to the abstract transition relation. In predicate abstraction, the quantifier elimination can be obtained by solving an ALLSAT problem. In many practical cases, this computation results into a bottleneck. In this paper, we propose a new algorithm that combines abstraction with bounded model checking and k-induction. The algorithm does not rely on quantifier elimination, but encodes the model checking problem over the abstract state space into SAT problems. The algorithm is a novelty in the state-of-the-art of abstract model checking because it avoids computing the abstraction. An experimental evaluation with case studies taken from an industrial project shows that the new algorithm is more efficient and reaches in some cases a time improvement that is exponential in the number of predicates
SMT-based scenario verification for hybrid systems
No full textHybrid automata are a widely used framework to model complex critical systems, where continuous physical dynamics are combined with discrete transitions. The expressive power of Satisfiability Modulo Theories (SMT) solvers can be used to symbolically model networks of hybrid automata, using formulas in the theory of reals, and SAT-based verification algorithms, such as bounded model checking and k-induction, can be naturally lifted to the SMT case.
In this paper, we tackle the important problem of scenario-based verification, i.e. checking if a network of hybrid automata accepts some desired interactions among the components, expressed as Message Sequence Charts (MSCs). We propose a novel approach, that exploits the structure of the scenario to partition and drive the search, both for bounded model checking and k-induction. We also show how to obtain information explaining the reasons for infeasibility in the case of invalid scenarios.
The expressive power of the SMT framework allows us to exploit a local time semantics, where the timescales of the automata in the network are synchronized upon shared events. The approach fully leverages the advanced features of modern SMT solvers, such as incrementality, unsatisfiable core extraction, and interpolation. An experimental evaluation demonstrates the effectiveness of the approach in proving both feasibility and unfeasibility, and the adequacy of the automatically generated explanations
Quantifier-free encoding of invariants for hybrid systems
No full textHybrid systems are a clean modeling framework for embedded systems,
which feature integrated discrete and continuous dynamics. A well-known source
of complexity comes from the time invariants, which represent an implicit quan-
tication of a constraint over all time points of a continuous transition.
Emerging techniques based on Satisability Modulo Theory (SMT) have been
found promising for the verication and validation of hybrid systems because they
combine discrete reasoning with solvers for rst-order theories. However, these
techniques are ecient for quantier-free theories and the current approaches have
so far either ignored time invariants or have been limited to hybrid systems with
linear constraints.
In this paper, we propose a new method that encodes a class of hybrid systems
into transition systems with quantier-free formulas. The method does not rely
on expensive quantier elimination procedures. Rather, it exploits the sequential
nature of the transition system to split the continuous evolution enforcing the
invariants on the discrete time points. This way, we can encode all hybrid systems
whose invariants can be expressed in terms of polynomial constraints. This pushes
the application of SMT-based techniques beyond the standard linear case
HRELTL: A temporal logic for hybrid systems
No full textHybrid traces are useful to describe behaviors of dynamic systems where continuous and discrete evolutions are combined. The ability to represent sets of traces by means of formulas in temporal logic has recently found important applications in various fields, such as requirements analysis, compositional verification, and contract-based design. In this paper we present HRELTL, a temporal logic to characterize hybrid traces. The logic is highly expressive: it allows the description of continuous behaviors, by expressing mathematical constraints over derivatives, and discrete behaviors, by constraining values of variables across instantaneous transitions. HRELTL combines the power of temporal operators and regular expressions, and enjoys important properties such as sampling invariance.
We demonstrate that the satisfiability problem for a fragment of HRELTL allows for a satisfiability-preserving reduction to RELTL(RA), a logic over discrete traces with atoms in non-linear Real Arithmetic for which automated reasoning procedures are being developed
A Property-Based Proof System for Contract-Based Design
No full textContract-based design is an emerging paradigm for the design of complex systems, where each component is associated with a contract, i.e., a clear description of the expected behaviour. Contracts specify the input-output behaviour of a component by defining what the component guarantees, provided that the its environment obeys some given assumptions. The ultimate goal of contract-based design is to allow for compositional reasoning, stepwise refinement, and a principled reuse of components that are already pre-designed, or designed independently. In this paper, we present a novel, fully formal contract framework. The decomposition of the system architecture is complemented with the corresponding decomposition of component contracts. The framework exploits such decomposition to automatically generate a set of proof obligations, which, once verified, allow concluding the correctness of the top-level system properties. The framework relies on an expressive property specification language, conceived for the formalization of embedded system requirements. The proof system reduces the correctness of contracts refinement to entailment of temporal logic formulas, and is supported by a verification engine based on automated SMT techniques
Generalizing Platform-Aware Mission Planning for Infinite-State Timed Transition Systems
No full textThe Platform-Aware Mission Planning (PAMP) problem, formalizes the relationship between an automated temporal planning problem and an execution platform modeled as a Timed Automaton. The PAMP problem consists in finding a valid plan that guarantees the plan executability and the satisfaction of a safety property on the platform, regardless of non-determinism. In this paper, we significantly generalize the PAMP problem along three directions. First, we consider platforms represented as infinite state timed transition systems (TTSs), allowing a more natural and expressive modeling of realistic systems. Second, we introduce a new feature to model relations between the fluents of the planning problem and the platform variables. Finally, we generalize the semantics to cope with unbounded traces. We define a solution method for the resulting generalized PAMP, combining an automated temporal planner and an infinite-state model-checker. Our method is largely more efficient than the existing approach for bounded PAMP problems, despite being strictly more expressive
- …
