| 1. |
- Alshnakat, Anoud, et al.
(författare)
-
Constraint-Based Contract Inference for Deductive Verification
- 2020
-
Ingår i: Deductive Software Verification. - Cham : Springer Nature. ; , s. 149-176
-
Bokkapitel (refereegranskat)abstract
- Assertion-based software model checking refers to techniques that take a program annotated with logical assertions and statically verify that the assertions hold whenever program execution is at the corresponding control point. While the associated annotation overhead is relatively low, these techniques are typically monolithic in that they explore the state space of the whole program at once, and may therefore scale poorly to large programs. Deductive software verification, on the other hand, refers to techniques that prove the correctness of a piece of software against a detailed specification of what it is supposed to accomplish or compute. The associated verification techniques are modular and scale well to large code bases, but incur an annotation overhead that is often very high, which is a real obstacle for deductive verification to be adopted in industry on a wider scale. In this paper we explore synergies between the two mentioned paradigms, and in particular, investigate how interpolation-based Horn solvers used for software model checking can be instrumented to infer missing procedure contracts for use in deductive verification, thus aiding the programmer in the code annotation process. We summarise the main developments in the area of automated contract inference, and present our own experiments with contract inference for C programs, based on solving Horn clauses. To drive the inference process, we put program assertions in the main function, and adapt our TriCera tool, a model checker based on the Horn solver Eldarica, to infer candidate contracts for all other functions. The contracts are output in the ANSI C Specification Language (ACSL) format, and are then validated with the Frama-C deductive verification tool for C programs.
|
|
| 2. |
- Gurov, Dilian, 1964-, et al.
(författare)
-
Automated Verification of Embedded Control Software : Track Introduction
- 2020
-
Ingår i: Leveraging Applications of Formal Methods, Verification and Validation. - Cham : Springer Nature. ; , s. 235-239
-
Konferensbidrag (refereegranskat)abstract
- Embedded control software is used in a variety of industries, such as in the automotive and railway domains, or in industrial automation and robotization. The development of such software is subject to tight time-to-market requirements, but at the same time also to very high safety requirements posed by various safety standards. To assure the latter, formal methods such as model-based testing and formal verification are increasingly used. However, the main obstacle to a more wide-scale adoption of these methods, and especially of formal verification, is the currently relative low level of automation of the verification process and integration in the general software development cycle. At present, writing formal specifications and annotating the embedded code is still a highly labour intensive activity requiring special competence and skills. In this track we address this challenge from various angles. We start by introducing the topic and then give a summary of the contributions.
|
|
| 3. |
- Gurov, Dilian, 1964-, et al.
(författare)
-
Who Carries the Burden of Modularity? : Introduction to ISoLA 2020 Track on Modularity and (De-)composition in Verification
- 2020
-
Ingår i: Leveraging Applications of Formal Methods, Verification and Validation. - Cham : Springer Nature. ; , s. 3-21
-
Konferensbidrag (refereegranskat)abstract
- Modularity and compositionality in verification frameworks occur within different contexts: the model that is the verification target, the specification of the stipulated properties, and the employed verification principle. We give a representative overview of mechanisms to achieve modularity and compositionality along the three mentioned contexts and analyze how mechanisms in different contexts are related. In many verification frameworks one of the contexts carries the main burden. It is important to clarify these relations to understand the potential and limits of the different modularity mechanisms.
|
|
| 4. |
- Nyberg, Mattias, et al.
(författare)
-
Formally Proving Compositionality in Industrial Systems with Informal Specifications
- 2020
-
Ingår i: ISoLA 2020: Leveraging Applications of Formal Methods, Verification and Validation: Applications. - Cham : Springer Science and Business Media Deutschland GmbH. ; , s. 348-365
-
Konferensbidrag (refereegranskat)abstract
- Based upon first-order logic, the paper presents a methodology and a deductive system for proving compositionality. Typical specifications found in industry are not expressed in any formal notation; rather most often in natural language. Therefore, the methodology does not assume specifications to be formal logical sentences. Instead, the methodology takes as input, properties of specifications and in particular, refinement relations. To cover general industrial heterogeneous systems, the semantics chosen is behavior based, originating in previous work on contract-based design for cyber-physical systems. In contrast to the previous work, implementation of specifications is non-monotonic with respect to composition. That is, even though a specification is implemented by one component, a composition with a second component may not implement the same specification. This kind of non-monotonicity is fundamentally important to support architectural specifications and so-called freedom-of-interference used in design of safety critical systems.
|
|
| 5. |
- Oortwijn, Wytse, et al.
(författare)
-
An Abstraction Technique for Verifying Shared-Memory Concurrency
- 2020
-
Ingår i: Applied Sciences. - : MDPI AG. - 2076-3417. ; 10:11
-
Tidskriftsartikel (refereegranskat)abstract
- Modern concurrent and distributed software is highly complex. Techniques to reason about the correct behaviour of such software are essential to ensure its reliability. To be able to reason about realistic programs, these techniques must be modular and compositional as well as practical by being supported by automated tools. However, many existing approaches for concurrency verification are theoretical and focus primarily on expressivity and generality. This paper contributes a technique for verifying behavioural properties of concurrent and distributed programs that balances expressivity and usability. The key idea of the approach is that program behaviour is abstractly modelled using process algebra, and analysed separately. The main difficulty is presented by the typical abstraction gap between program implementations and their models. Our approach bridges this gap by providing a deductive technique for formally linking programs with their process-algebraic models. Our verification technique is modular and compositional, is proven sound with Coq, and has been implemented in the automated concurrency verifier VerCors. Moreover, our technique is demonstrated on multiple case studies, including the verification of a leader election protocol.
|
|
| 6. |
- Oortwijn, Wytse, et al.
(författare)
-
Practical Abstractions for Automated Verification of Shared-Memory Concurrency
- 2020
-
Ingår i: Lect. Notes Comput. Sci.. - Cham : Springer. ; , s. 401-425
-
Konferensbidrag (refereegranskat)abstract
- Modern concurrent and distributed software is highly complex. Techniques to reason about the correct behaviour of such software are essential to ensure its reliability. To be able to reason about realistic programs, these techniques must be modular and compositional as well as practical by being supported by automated tools. However, many existing approaches for concurrency verification are theoretical and focus on expressivity and generality. This paper contributes a technique for verifying behavioural properties of concurrent and distributed programs that makes a trade-off between expressivity and usability. The key idea of the approach is that program behaviour is abstractly modelled using process algebra, and analysed separately. The main difficulty is presented by the typical abstraction gap between program implementations and their models. Our approach bridges this gap by providing a deductive technique for formally linking programs with their process-algebraic models. Our verification technique is modular and compositional, is proven sound with Coq, and has been implemented in the automated concurrency verifier VerCors. Moreover, our technique is demonstrated on multiple case studies, including the verification of a leader election protocol.
|
|
