JavaBIP meets VerCors: Towards the Safety of Concurrent Software Systems in Java

Bliudze, Simon; van den Bos, Petra; Huisman, Marieke; Rubbens, Robert; Safina, Larisa

Document type :

Communication dans un congrès avec actes

DOI :

10.1007/978-3-031-30826-0_8

Title :

JavaBIP meets VerCors: Towards the Safety of Concurrent Software Systems in Java

Author(s) :

Bliudze, Simon [Auteur]

Centre de Recherche en Informatique, Signal et Automatique de Lille - UMR 9189 [CRIStAL]
Self-adaptation for distributed services and large software systems [SPIRALS]
van den Bos, Petra [Auteur]
Formal Methods and Tools [FMT group]
Huisman, Marieke [Auteur]
Formal Methods and Tools [FMT group]
Rubbens, Robert [Auteur]
Formal Methods and Tools [FMT group]
Safina, Larisa [Auteur]
Reflective Evolution of Ever-running Software Systems [EVREF]
Centre de Recherche en Informatique, Signal et Automatique de Lille - UMR 9189 [CRIStAL]

Conference title :

FASE 2023 - 26th International Conference on Fundamental Approaches to Software Engineering

City :

Paris

Country :

France

Start date of the conference :

2023-04-20

Journal title :

Lecture Notes in Computer Science

Publisher :

Springer Nature Switzerland

Publication place :

Cham

Publication date :

2023-04-20

HAL domain(s) :

Informatique [cs]/Génie logiciel [cs.SE]
Informatique [cs]/Langage de programmation [cs.PL]

English abstract : [en]

We present "Verified JavaBIP", a tool set for the verification of JavaBIP models. A JavaBIP model is a Java program where classes are considered as components, their behaviour described by finite state machine and ...
Show more >We present "Verified JavaBIP", a tool set for the verification of JavaBIP models. A JavaBIP model is a Java program where classes are considered as components, their behaviour described by finite state machine and synchronization annotations. While JavaBIP guarantees execution progresses according to the indicated state machine, it does not guarantee properties of the data exchanged between components. It also does not provide verification support to check whether the behaviour of the resulting concurrent program is as (safe as) expected. This paper addresses this by extending the JavaBIP engine with run-time verification support, and by extending the program verifier VerCors to verify JavaBIP models deductively. These two techniques complement each other: feedback from run-time verification allows quicker prototyping of contracts, and deductive verification can reduce the overhead of run-time verification. We demonstrate our approach on the "Solidity Casino" case study, known from the VerifyThis Collaborative Long Term Challenge.Show less >

Language :

Anglais

Peer reviewed article :

Oui

Audience :

Internationale

Popular science :

Non

ANR Project :

ULNE
Compositions Non-agrégatives de Resources

Collections :

Centre de Recherche en Informatique, Signal et Automatique de Lille (CRIStAL) - UMR 9189

Source :

Harvested from HAL

Files

document
Open access
Access the document

javabip-meets-vercors-submitted-draft-2022-10-21.pdf
Open access
Access the document

document
Open access
Access the document

javabip-meets-vercors-submitted-draft-2022-10-21.pdf
Open access
Access the document

JavaBIP meets VerCors: Towards the Safety ... BibTeX CSV Excel RIS

Files

JavaBIP meets VerCors: Towards the Safety ...

BibTeX

CSV

Excel

RIS