Notice
This item was automatically migrated from a legacy system. It's data has not been checked and might not meet the quality criteria of the present system.
E192-04 - Forschungsbereich Formal Methods in Systems Engineering E192 - Institut für Logic and Computation E191-02 - Forschungsbereich Embedded Computing Systems
-
ISSN:
0163-5700
-
Date (published):
2016
-
Number of Pages:
12
-
Peer reviewed:
No
-
Keywords:
General Medicine
-
Abstract:
Parameterized model checking is an active research field that considers automated verification of distributed or concurrent systems, for all numbers of participating processes. In our
recent book [11] we surveyed literature on decidability of parameterized verification. The system
models, as well as the proof methods, that are studied in this field are similar to those from
distributed computin...
Parameterized model checking is an active research field that considers automated verification of distributed or concurrent systems, for all numbers of participating processes. In our
recent book [11] we surveyed literature on decidability of parameterized verification. The system
models, as well as the proof methods, that are studied in this field are similar to those from
distributed computing. For instance, we survey results for token passing systems and ad hoc
networks. The proof methods for undecidability include simulation of two-counter machines.
For decidability, we survey cut-off results that provide conditions to reduce parameterized verification to model checking of fixed-size systems. We believe that the results are of interest to
the readers of the Distributed Computing Column, and in this short note we want to give a
taste of parameterized model checking.
en
Project title:
Parametrized Verification of Fault-tolerant Distributed Algorithms Abstraction-based Parameterized TLA Checker
-
Research Areas:
Logic and Computation: 70% Computer Engineering and Software-Intensive Systems: 20% Distributed and Parallel Systems: 10%
