| 1. |
- Aarts, Fides, et al.
(författare)
-
Generating models of infinite-state communication protocols using regular inference with abstraction
- 2015
-
Ingår i: Formal methods in system design. - : Springer Science and Business Media LLC. - 0925-9856 .- 1572-8102. ; 46:1, s. 1-41
-
Tidskriftsartikel (refereegranskat)abstract
- In order to facilitate model-based verification and validation, effort is underway to develop techniques for generating models of communication system components from observations of their external behavior. Most previous such work has employed regular inference techniques which generate modest-size finite-state models. They typically suppress parameters of messages, although these have a significant impact on control flow in many communication protocols. We present a framework, which adapts regular inference to include data parameters in messages and states for generating components with large or infinite message alphabets. A main idea is to adapt the framework of predicate abstraction, successfully used in formal verification. Since we are in a black-box setting, the abstraction must be supplied externally, using information about how the component manages data parameters. We have implemented our techniques by connecting the LearnLib tool for regular inference with an implementation of session initiation protocol (SIP) in ns-2 and an implementation of transmission control protocol (TCP) in Windows 8, and generated models of SIP and TCP components.
|
|
| 2. |
- Ahrendt, Wolfgang, 1967, et al.
(författare)
-
Verifying data- and control-oriented properties combining static and runtime verification: theory and tools
- 2017
-
Ingår i: Formal Methods in System Design. - : Springer Science and Business Media LLC. - 0925-9856 .- 1572-8102. ; 51:1, s. 200-265
-
Tidskriftsartikel (refereegranskat)abstract
- Static verification techniques are used to analyse and prove properties about programs before they are executed. Many of these techniques work directly on the source code and are used to verify data-oriented properties over all possible executions. The analysis is necessarily an over-approximation as the real executions of the program are not available at analysis time. In contrast, runtime verification techniques have been extensively used for control-oriented properties, analysing the current execution path of the program in a fully automatic manner. In this article, we present a novel approach in which data-oriented and control-oriented properties may be stated in a single formalism amenable to both static and dynamic verification techniques. The specification language we present to achieve this that of ppDATEs, which enhances the control-oriented property language of DATEs, with data-oriented pre/postconditions. For runtime verification of ppDATE specifications, the language is translated into a DATE. We give a formal semantics to ppDATEs, which we use to prove the correctness of our translation from ppDATEs to DATEs. We show how ppDATE specifications can be analysed using a combination of the deductive theorem prover KeY and the runtime verification tool LARVA. Verification is performed in two steps: KeY first partially proves the data-oriented part of the specification, simplifying the specification which is then passed on to LARVA to check at runtime for the remaining parts of the specification including the control-oriented aspects. We show the applicability of our approach on two case studies.
|
|
| 3. |
- Chakraborty, S., et al.
(författare)
-
Symbolic trajectory evaluation for word-level verification: theory and implementation
- 2017
-
Ingår i: Formal Methods in System Design. - : Springer Science and Business Media LLC. - 1572-8102 .- 0925-9856. ; 50:2-3, s. 317-352
-
Tidskriftsartikel (refereegranskat)abstract
- Symbolic trajectory evaluation (STE) is a model checking technique that has been successfully used to verify many industrial designs. Existing implementations of STE reason at the level of bits, allowing signals in a circuit to take values from a lattice comprised of three elements: 0, 1, and X. This limits the amount of abstraction that can be achieved, and presents limitations to scaling STE to even larger designs. The main contribution of this paper is to show how much more abstract lattices can be derived automatically from register-transfer level descriptions, and how a model checker for the general theory of STE instantiated with such abstract lattices can be implemented in practice. We discuss several implementation issues, including how word-level circuits can be symbolically simulated using a new encoding for words that allows representing X values of sub-words succinctly. This gives us the first practical word-level STE engine, called STEWord. Experiments on a set of designs similar to those used in industry show that STEWord scales better than bit-level STE, as well as word-level bounded model checking.
|
|
| 4. |
|
|
| 5. |
- Klebanov, Vladimir, et al.
(författare)
-
Automating regression verification of pointer programs by predicate abstraction
- 2018
-
Ingår i: Formal methods in system design. - : Springer Science and Business Media LLC. - 0925-9856 .- 1572-8102. ; 52:3, s. 229-259
-
Tidskriftsartikel (refereegranskat)abstract
- Regression verification is an approach complementing regression testing with formal verification. The goal is to formally prove that two versions of a program behave either equally or differently in a precisely specified way. In this paper, we present a novel automated approach for regression verification that reduces the equivalence of two related imperative pointer programs to constrained Horn clauses over uninterpreted predicates. Subsequently, state-of-the-art SMT solvers are used to solve the clauses. We have implemented the approach, and our experiments show that non-trivial programs with integer and pointer arithmetic can now be proved equivalent without further user input.
|
|
| 6. |
|
|
| 7. |
- Sanchez Perez, Cesar, 1981, et al.
(författare)
-
A survey of challenges for runtime verification from advanced application domains (beyond software)
- 2019
-
Ingår i: Formal Methods in System Design. - : Springer Science and Business Media LLC. - 1572-8102 .- 0925-9856. ; 54:3, s. 279-335
-
Tidskriftsartikel (refereegranskat)abstract
- Runtime verification is an area of formal methods that studies the dynamic analysis of execution traces against formal specifications. Typically, the two main activities in runtime verification efforts are the process of creating monitors from specifications, and the algorithms for the evaluation of traces against the generated monitors. Other activities involve the instrumentation of the system to generate the trace and the communication between the system under analysis and the monitor. Most of the applications in runtime verification have been focused on the dynamic analysis of software, even though there are many more potential applications to other computational devices and target systems. In this paper we present a collection of challenges for runtime verification extracted from concrete application domains, focusing on the difficulties that must be overcome to tackle these specific challenges. The computational models that characterize these domains require to devise new techniques beyond the current state of the art in runtime verification.
|
|
| 8. |
- Westman, Jonas, 1986-, et al.
(författare)
-
Conditions of Contracts for Separating Responsibilities in Heterogeneous Systems
- 2018
-
Ingår i: Formal methods in system design. - : Springer Nature. - 0925-9856 .- 1572-8102. ; 52:2, s. 147-192
-
Tidskriftsartikel (refereegranskat)abstract
- A general, compositional, and component-based contract theory is proposed for modeling and specifying heterogeneous systems, characterized by consisting of parts from different domains, e.g. software, electrical and mechanical. Given a contract consisting of assumptions and a guarantee, clearly separated conditions on a component and its environment are presented where the conditions ensure that the guarantee is fulfilled - a responsibility assigned to the component, given that the environment fulfills the assumptions. The conditions are applicable whenever it cannot be ensured that the sets of ports of components are partitioned into inputs and outputs, and hence fully support scenarios where components, characterized by both causal and acausal models, are to be integrated by solely relying on the information of a contract. An example of such a scenario of industrial relevance is explicitly considered, namely a scenario in a supply chain where the development of a component is outsourced. To facilitate the application of the theory in practice, necessary properties of contracts are also derived to serve as sanity checks of the conditions. Furthermore, based on a graph that represents a structuring of a hierarchy of contracts, sufficient conditions to achieve compositionality are presented.
|
|
