Abstract
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 machines, 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.
Original language | English |
---|---|
Title of host publication | Fundamental Approaches to Software Engineering |
Subtitle of host publication | 26th International Conference, FASE 2023, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2023, Paris, France, April 22–27, 2023, Proceedings |
Editors | Leen Lambers, Sebastián Uchitel |
Pages | 143-150 |
Number of pages | 8 |
ISBN (Electronic) | 978-3-031-30826-0 |
DOIs | |
Publication status | Published - 20 Apr 2023 |
Event | International Conference on Fundamental Approaches to Software Engineering, FASE 2023 - Paris, France Duration: 22 Apr 2023 → 27 Apr 2023 |
Conference
Conference | International Conference on Fundamental Approaches to Software Engineering, FASE 2023 |
---|---|
Abbreviated title | FASE 2023 |
Country/Territory | France |
City | Paris |
Period | 22/04/23 → 27/04/23 |
Fingerprint
Dive into the research topics of 'JavaBIP meets VerCors: Towards the Safety of Concurrent Software Systems in Java'. Together they form a unique fingerprint.Datasets
-
Artefact of: JavaBIP meets VerCors: Towards the Safety of Concurrent Software Systems in Java
Rubbens, R. (Creator), Safina, L. (Creator), Huisman, M. (Creator), Bliudze, S. (Creator) & van den Bos, P. (Creator), 4TU.Centre for Research Data, 13 Mar 2024
DOI: 10.4121/21763274, https://data.4tu.nl/datasets/c24f1f76-19f3-456b-b6cd-087eef905e5d and one more link, https://data.4tu.nl/datasets/c24f1f76-19f3-456b-b6cd-087eef905e5d/1 (show fewer)
Dataset