tla-ci

TLA+ specifications accompanying paper: Automated Validation of State-Based Client-Centric Isolation with TLA+. (https://doi.org/10.1007/978-3-030-67220-1_4) Based on Crooks' Isolation (https://dl.acm.org/doi/10.1145/3087801.3087802).

https://github.com/cwi-swat/tla-ci

Science Score: 41.0%

This score indicates how likely this project is to be science-related based on various indicators:

✓
CITATION.cff file
Found CITATION.cff file
○
codemeta.json file
○
.zenodo.json file
✓
DOI references
Found 3 DOI reference(s) in README
✓
Academic publication links
Links to: acm.org
○
Academic email domains
○
Institutional organization owner
○
JOSS paper metadata
○
Scientific vocabulary similarity
Low similarity (4.6%) to scientific vocabulary

Keywords

pluscal tlaplus

Last synced: 6 months ago · JSON representation ·

Repository

Basic Info

Host: GitHub
Owner: cwi-swat
License: bsd-2-clause
Language: TLA
Default Branch: master
Homepage:
Size: 1.57 MB

Statistics

Stars: 20
Watchers: 5
Forks: 2
Open Issues: 1
Releases: 1

Topics

pluscal tlaplus

Created over 5 years ago · Last pushed almost 2 years ago

Metadata Files

Readme License Citation

README.md

TLA-CI

TLA+ specifications accompanying paper: Automated Validation of State-Based Client-Centric Isolation with TLA+ (ASYDE'20) (https://doi.org/10.1007/978-3-030-67220-1_4). Based on Crooks' Isolation.

The code can be run with both:

Contents - ClientCentric.tla contains the definitions of Crooks' Isolation model. - ClientCentricPaperExamples.tla contains some examples from the paper. For example ASSUME test(Serializability(as1, bankTransactions), TRUE) shows that the banking example is serializable, but the other ordering isn't (Serializability(as1, bBankTransactions = FALSE), but is Snapshot Isolatable: ASSUME test(executionSatisfiesCT(bExecution, CT_SI), TRUE). - The 2PL related files show how a specification bug in a 2PL/2PC protocol can result in not serializable behavior.

Please contact me for more details.

Owner

Name: CWI - Software Analysis and Transformation
Login: cwi-swat
Kind: organization
Location: Amsterdam

Website: https://www.cwi.nl/research/groups/software-analysis-and-transformation
Repositories: 186
Profile: https://github.com/cwi-swat

Citation (CITATION.bib)

@inproceedings{DBLP:conf/sefm/SoethoutSV20,
  author    = {Tim Soethout and
               Tijs van der Storm and
               Jurgen J. Vinju},
  editor    = {Loek Cleophas and
               Mieke Massink},
  title     = {Automated Validation of State-Based Client-Centric Isolation with
               TLA\textsuperscript{\smaller+}},
  booktitle = {Software Engineering and Formal Methods. {SEFM} 2020 Collocated Workshops
               - ASYDE, CIFMA, and CoSim-CPS, Amsterdam, The Netherlands, September
               14-15, 2020, Revised Selected Papers},
  series    = {Lecture Notes in Computer Science},
  volume    = {12524},
  pages     = {43--57},
  publisher = {Springer},
  year      = {2020},
  doi       = {10.1007/978-3-030-67220-1_4},
  timestamp = {Mon, 25 Jan 2021 17:33:07 +0100}}

GitHub Events

Total

Issues event: 2
Watch event: 2
Issue comment event: 4

Last Year

Issues event: 2
Watch event: 2
Issue comment event: 4

Issues and Pull Requests

Last synced: 6 months ago

All Time

Total issues: 1
Total pull requests: 0
Average time to close issues: N/A
Average time to close pull requests: N/A
Total issue authors: 1
Total pull request authors: 0
Average comments per issue: 0.0
Average comments per pull request: 0
Merged pull requests: 0
Bot issues: 0
Bot pull requests: 0

Past Year

Issues: 1
Pull requests: 0
Average time to close issues: N/A
Average time to close pull requests: N/A
Issue authors: 1
Pull request authors: 0
Average comments per issue: 0.0
Average comments per pull request: 0
Merged pull requests: 0
Bot issues: 0
Bot pull requests: 0

ecosyste.ms

Data

Tools

Indexes

Applications

Experiments

Open Source Science