TLA+ model checking made symbolic
| Autor: | Igor Konnov, Thanh-Hai Tran, Jure Kukovec |
|---|---|
| Přispěvatelé: | Modeling and Verification of Distributed Algorithms and Systems (VERIDIS), Max-Planck-Institut für Informatik (MPII), Max-Planck-Gesellschaft-Max-Planck-Gesellschaft-Inria Nancy - Grand Est, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-Department of Formal Methods (LORIA - FM), Laboratoire Lorrain de Recherche en Informatique et ses Applications (LORIA), Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Laboratoire Lorrain de Recherche en Informatique et ses Applications (LORIA), Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS), Proof-oriented development of computer-based systems (MOSEL), Department of Formal Methods (LORIA - FM), Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS), Vienna University of Technology (TU Wien), Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Inria Nancy - Grand Est, Institut National de Recherche en Informatique et en Automatique (Inria)-Max-Planck-Institut für Informatik (MPII), Max-Planck-Gesellschaft-Max-Planck-Gesellschaft |
| Rok vydání: | 2019 |
| Předmět: |
Model checking
Exploit Relation (database) Computer science Programming language [INFO.INFO-LO]Computer Science [cs]/Logic in Computer Science [cs.LO] 020207 software engineering [INFO.INFO-SE]Computer Science [cs]/Software Engineering [cs.SE] 02 engineering and technology computer.software_genre Language primitive TLA+ SMT 020204 information systems Formal specification 0202 electrical engineering electronic engineering information engineering State (computer science) Tuple Safety Risk Reliability and Quality Boolean data type computer Software |
| Zdroj: | Proceedings of the ACM on Programming Languages Proceedings of the ACM on Programming Languages, 2019, 3 (OOPSLA), pp.123:1--123:30. ⟨10.1145/3360549⟩ Proceedings of the ACM on Programming Languages, ACM, 2019, 3 (OOPSLA), pp.123:1--123:30. ⟨10.1145/3360549⟩ |
| ISSN: | 2475-1421 |
| Popis: | TLA+ is a language for formal specification of all kinds of computer systems. System designers use this language to specify concurrent, distributed, and fault-tolerant protocols, which are traditionally presented in pseudo-code. TLA+ is extremely concise yet expressive: The language primitives include Booleans, integers, functions, tuples, records, sequences, and sets thereof, which can be also nested. This is probably why the only model checker for TLA+ (called TLC) relies on explicit enumeration of values and states. In this paper, we present APALACHE -- a first symbolic model checker for TLA+. Like TLC, it assumes that all specification parameters are fixed and all states are finite structures. Unlike TLC, APALACHE translates the underlying transition relation into quantifier-free SMT constraints, which allows us to exploit the power of SMT solvers. Designing this translation is the central challenge that we address in this paper. Our experiments show that APALACHE outperforms TLC on examples with large state spaces. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|