# Extracting Symbolic Transitions from $TLA+$ Specifications

2 VERIDIS - Modeling and Verification of Distributed Algorithms and Systems
Inria Nancy - Grand Est, LORIA - FM - Department of Formal Methods
Abstract : In TLA+, a system specification is written as a logical formula that restricts the system behavior. As a logic, TLA+ does not have assignments and other imperative statements that are used by model checkers to compute the successor states of a system state. Model checkers compute successors either explicitly-by evaluating program statements-or symbolically-by translating program statements to an SMT formula and checking its satisfiability. To efficiently enumerate the successors, TLA's model checker TLC introduces side effects. For instance, an equality x = e is interpreted as an assignment of e to the yet unbound variable x. Inspired by TLC, we introduce an automatic technique for discovering expressions in TLA+ formulas such as x = e and x ∈ {e1,. .. , e k } that can be provably used as assignments. In contrast to TLC, our technique does not explicitly evaluate expressions, but it reduces the problem of finding assignments to the satisfiability of an SMT formula. Hence, we give a way to slice a TLA+ formula in symbolic transitions, which can be used as an input to a symbolic model checker. Our prototype implementation successfully extracts symbolic transitions from a few TLA+ benchmarks.
Keywords :
Type de document :
Communication dans un congrès
Michael Butler; Alexander Raschke; Thai Son Hoang; Klaus Reichl. Abstract State Machines, Alloy, B, TLA, VDM, and Z. ABZ 2018, Jun 2018, Southampton, United Kingdom. 10817, pp.89-104, Lecture Notes in Computer Science. 〈https://www.southampton.ac.uk/abz2018/index.page〉. 〈10.1007/978-3-319-91271-4_7〉
Domaine :

https://hal.inria.fr/hal-01871131
Contributeur : Igor Konnov <>
Soumis le : lundi 10 septembre 2018 - 13:53:01
Dernière modification le : mardi 18 décembre 2018 - 16:38:25
Document(s) archivé(s) le : mardi 11 décembre 2018 - 14:41:54

### Fichier

camera.pdf
Fichiers produits par l'(les) auteur(s)

### Citation

Jure Kukovec, Thanh-Hai Tran, Igor Konnov. Extracting Symbolic Transitions from $TLA+$ Specifications. Michael Butler; Alexander Raschke; Thai Son Hoang; Klaus Reichl. Abstract State Machines, Alloy, B, TLA, VDM, and Z. ABZ 2018, Jun 2018, Southampton, United Kingdom. 10817, pp.89-104, Lecture Notes in Computer Science. 〈https://www.southampton.ac.uk/abz2018/index.page〉. 〈10.1007/978-3-319-91271-4_7〉. 〈hal-01871131〉

### Métriques

Consultations de la notice

## 102

Téléchargements de fichiers