| 1. |
- Ahrendt, Wolfgang, 1967, et al.
(author)
-
Specification language for static and runtime verification of data and control properties
- 2015
-
In: Lecture Notes in Computer Science. FM 2015: FORMAL METHODS. 20th International Symposium on Formal Methods (FM), Oslo, Norway, June 24-26, 2015. - Cham : Springer International Publishing. - 0302-9743 .- 1611-3349. - 9783319192482 ; 9109, s. 108-125
-
Conference paper (peer-reviewed)abstract
- Static verification techniques can verify properties across all executions of a program, but powerful judgements are hard to achieve automatically. In contrast, runtime verification enjoys full automation, but cannot judge future and alternative runs. In this paper we present a novel approach in which data-centric and control-oriented properties may be stated in a single formalism, amenable to both static and dynamic verification techniques. We develop and formalise a specification notation, ppDATE, extending the control-flow property language used in the runtime verification tool Larva with pre/post-conditions and show how specifications written in this notation can be analysed both using the deductive theorem prover KeY and the runtime verification tool Larva. Verification is performed in two steps: KeY first partially proves the dataoriented 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-centric aspects. We apply the approach to Mondex, an electronic purse application.
|
|
| 2. |
- Ahrendt, Wolfgang, 1967, et al.
(author)
-
Verifying data- and control-oriented properties combining static and runtime verification: theory and tools
- 2017
-
In: Formal Methods in System Design. - : Springer Science and Business Media LLC. - 0925-9856 .- 1572-8102. ; 51:1, s. 200-265
-
Journal article (peer-reviewed)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. |
- Chimento, Mauricio, 1985
(author)
-
Combined Static and Dynamic Verification of Object Oriented Software Through Partial Proofs
- 2019
-
Doctoral thesis (other academic/artistic)abstract
- When verifying software one can make use of several verification techniques. These techniques mostly fall in one of two categories: Static Verification and Dynamic Verification. Static verification deals with the analysis of either concrete source code, or a model of it. These kinds of techniques can verify properties over all possible runs of a program. Dynamic verification is concerned with the monitoring of software, providing guarantees that observed runs comply with specified properties. It is strong in analysing systems of a complexity that is difficult to address by static verification, e.g., systems with numerous interacting sub-units, concrete (as opposed to abstract) data, etc. On the other hand, its major drawbacks are the impossibility to extrapolate correct observations to all possible runs, and that the monitoring of a property introduces runtime overheads. It is quite clear that static and dynamic verification have largely disjoint strengths. Therefore, their combination can allow the verification process to deal with richer properties, with greater ease. The work presented in this thesis addresses this issue by introducing some manners to combine static and dynamic verification, where partial proofs are used as a means to accomplish the combination. The main novelty in these combinations consists in the fact that all of them consider the use of the partial proofs in the verification process, whereas, in general, other verification approaches discard them right away. The main contributions of this thesis are: (i) ppDATE, an automata-based formalism to specify both data- and control-oriented properties; (ii) structural operational semantics for ppDATE; (iii) a translation of ppDATE to DATE together with a proof of correctness; (iv) StaRVOOrS, a tool for combining (static) deductive verification and runtime verification of object oriented software; (v) a testing focused development methodology which integrates deductive and runtime verification in its workflow; and (vi) a methodology to infer global trace conditions for a system, from partial proofs local to the transitions of a model, obtained by performing low effort verification attempts to properties.
|
|
| 4. |
- Chimento, Mauricio, 1985, et al.
(author)
-
STARVOORS: A Tool for Combined Static and Runtime Verification of Java
- 2015
-
In: Lecture Notes in Computer Science - 6th International Conference on Runtime Verification (RV). - Cham : Springer International Publishing. - 0302-9743 .- 1611-3349. - 9783319238203 ; 9333, s. 297-305
-
Conference paper (peer-reviewed)abstract
- We present the tool StaRVOOrS (Static and Runtime Verification of Object-Oriented Software), which combines static and runtime verification (RV) of Java programs. The tool automates a framework which uses partial results extracted from static verification to optimise the runtime monitoring process. StaRVOOrs combines the deductive theorem prover KeY and the RV tool LARVA, and uses properties written using the ppDATE specification language which combines the control-flow property language DATE used in LARVA with Hoare triples assigned to states. We demonstrate the effectiveness of the tool by applying it to the electronic purse application Mondex.
|
|
| 5. |
- Chimento, Mauricio, 1985, et al.
(author)
-
Testing Meets Static and Runtime Verification
- 2018
-
In: Proceedings - 2018 ACM/IEEE Conference on Formal Methods in Software Engineering, FormaliSE 2018. - New York, NY, USA : ACM. ; , s. 30-39
-
Conference paper (peer-reviewed)abstract
- Test driven development (TDD) is a technique where test cases are used to guide the development of a system. This technique introduces several advantages at the time of developing a system, e.g. writing clean code, good coverage for the features of the system, and evolutionary development. In this paper we show how the capabilities of a testing focused development methodology based on TDD and model-based testing, can be enhanced by integrating static and runtime verification into its workflow. Considering that the desired system properties capture data- As well as control-oriented aspects, we integrate TDD with (static) deductive verification as an aid in the development of the data-oriented aspects, and we integrate model-based testing with runtime verification as an aid in the development of the control-oriented aspects. As a result of this integration, the proposed development methodology features the benefits of TDD and model-based testing, enhanced with, for instance, early detection of bugs which may be missed by TDD, regarding data aspects, and the validation of the overall system with respect to the model, regarding the control aspects.
|
|
| 6. |
- Chimento, Mauricio, 1985
(author)
-
Unified Static and Runtime Verification of Object-Oriented Software
- 2017
-
Licentiate thesis (other academic/artistic)abstract
- At the time of verifying software one can make use of several verification techniques. These techniques mostly fall in one of two categories: Static Verification and Dynamic Verification. Runtime Verification is a dynamic verification technique which is concerned with the monitoring of software, providing guarantees that observed runs comply with specified properties. It is strong in analysing systems of a complexity that is difficult to address by static verification, e.g., systems with numerous interacting sub-units, real (as opposed to abstract) data, etc. On the other hand, the major drawbacks of runtime verification are the impossibility to extrapolate correct observations to all possible executions, and that the monitoring of a program introduces runtime overheads. The work presented in this thesis addresses these issues by introducing a novel approach which combines the use of runtime verification with static verification, in such a way that:(i) static verification attempts to `resolve' the parts of the properties which can be confirmed statically; (ii) the static results, even if only partial, are used to improve the specified properties such that generated monitors will not check at runtime what was already verified statically.In addition, this thesis introduces the specification language ppDATE (and its semantics), which allows to describe properties suitable for static and runtime verification within a single formalism; the verification tool StaRVOOrS, which embodies the previously mentioned approach; and presents some case studies to demonstrate the effectiveness of using this new approach.
|
|
