Unified Static and Runtime Verification of Object-Oriented Software

(STARVOORS)

About



The overall purpose of StaRVOOrS (`Unified Static and Runtime Verification of Object-Oriented Software') is to provide a unified, lightweight to use but powerful in result, method for specifying and verifying, with a variety of confidence levels, properties of parallel object-oriented software systems.


Specific goals of StaRVOOrSs


  • To combine the strengths of static and runtime verification into a verification method that is easier to use than static methods, while providing a higher level of confidence and a lower application slow down than runtime verification.

  • To let both of the underlying verification techniques (static and runtime) profit to a great extent from the analysis performed by the respective other.

  • To develop techniques which also allow exploiting partial results, like unfinished proofs, to strengthen the result of the unified verification method.

  • To provide a unified framework for specifying desired properties of the system to be verified. The user will not have to separate sub-properties that are subject to static vs. runtime verification during the process.

  • To support the combination of data centric and control centric properties, including real time constraints.

  • To provide a verification solution for sequential, concurrent, and distributed object-oriented applications.

  • To implement a powerful, integrated tool that achieves the aforementioned goals for Java applications
    in particular.

Chalmers University of Technology

Partners



Jesus Mauricio Chimento

Wolfgang Ahrendt

Gerardo Schneider

External Collaborator(s)

Gordon Pace

Publications



Verifying data- and control-oriented properties combining static and runtime verification: theory and tools

W. Ahrendt, J. M. Chimento, G. Pace, and G. Schneider.
Formal Methods in System Design.
04 April 2017. Springer.
PDF Bibtex Pre-printed version

StaRVOOrS --- Episode II. Strengthen and Distribute the Force

W. Ahrendt, G. Pace, and G. Schneider.
Leveraging Applications of Formal Methods, Verification and Validation.
7th International Symposium, ISoLA 2016.
Volume 9952 of LNCS, pages 402-415.
Heraklion, Crete, Greece, 05 October 2016. Springer.
PDF Bibtex Pre-printed version

StaRVOORS: A Tool for Combined Static and Runtime Verification of Java

J. M. Chimento, W. Ahrendt, G. Pace, and G. Schneider.
Runtime Verification 2015 (RV'15).
Volume 9333 of LNCS, pages 297-305.
Vienna, Austria, September 23-25 2015. Springer.
PDF Bibtex Pre-printed version

A Specification Language for Static and Runtime Verification of Data and Control Properties

W. Ahrendt, J. M. Chimento, G. Pace, and G. Schneider.
Formal Methods 2015 (FM'15), 20th International Symposium on Formal Methods.
Volume 9109 of LNCS, pages 108-125.
Oslo, Norway, June 24-26 2015. Springer.
PDF Bibtex Pre-print PDF

A Unified Approach for Static and Runtime Verification: Framework and Applications

Wolfgang Ahrendt, Gordon J. Pace, Gerardo Schneider.
Leveraging Applications of Formal Methods, Verification and Validation.
5th International Symposium, ISoLA 2012, Heraklion, Crete, Greece.
Proceedings, Part I, Springer-Verlag, LNCS 7609.
PDF Bibtex

Downloads



StaRVOOrS tool

The StaRVOOrS tool can be found on Github. This repository contains the source code of the tool, its user manual, and ppDATE syntax hilighting.

Ready-to-try examples for StaRVOOrS

Login example files
Coffee Machine example
Mondex Case Study
SoftSlate Case Study

Tutorials



StaRVOOrS tool Video Tutorial

Video tutorial on how to use the StaRVOOrS tool. See on youtube.

Demonstration Script

Demonstration script on how to use the StaRVOOrS tool. Download.