Abstract
| Language | Undefined |
|---|---|
| Title of host publication | 10th International Conference on Formal Modeling and Analysis of Timed Systems, FORMATS 2012 |
| Editors | M. Jurdzinski, D. Nickovic |
| Place of Publication | London |
| Publisher | Springer Verlag |
| Pages | 91-106 |
| Number of pages | 16 |
| ISBN (Print) | 978-3-642-33365-1 |
| DOIs | |
| State | Published - 18 Sep 2012 |
| Event | 10th International Conference on Formal Modeling and Analysis of Timed Systems, FORMATS 2012 - Imperial College London, London, United Kingdom Duration: 18 Sep 2012 → 20 Sep 2012 Conference number: 10 http://www2.warwick.ac.uk/fac/cross_fac/dimap/events/formats2012/ |
Publication series
| Name | Lecture Notes in Computer Science |
|---|---|
| Publisher | Springer Verlag |
| Volume | 7595 |
| ISSN (Print) | 0302-9743 |
| ISSN (Electronic) | 1611-3349 |
Conference
| Conference | 10th International Conference on Formal Modeling and Analysis of Timed Systems, FORMATS 2012 |
|---|---|
| Abbreviated title | FORMATS |
| Country | United Kingdom |
| City | London |
| Period | 18/09/12 → 20/09/12 |
| Internet address |
Keywords
- METIS-287893
- Abstraction
- IR-80819
- Multi-Core
- Model Checking
- well-quasi-ordering
- EWI-21972
- lockless
- lattice-based model checking
- Timed Automata
- Symbolic reachability
- Parallel
- FMT-MC: MODEL CHECKING
- hash table
Cite this
}
Multi-Core Reachability for Timed Automata. / Dalsgaard, Andreas; Laarman, Alfons; Larsen, K.G.; Olesen, Mads Chr.; van de Pol, Jan Cornelis.
10th International Conference on Formal Modeling and Analysis of Timed Systems, FORMATS 2012. ed. / M. Jurdzinski; D. Nickovic. London : Springer Verlag, 2012. p. 91-106 (Lecture Notes in Computer Science; Vol. 7595).Research output: Chapter in Book/Report/Conference proceeding › Conference contribution
TY - GEN
T1 - Multi-Core Reachability for Timed Automata
AU - Dalsgaard,Andreas
AU - Laarman,Alfons
AU - Larsen,K.G.
AU - Olesen,Mads Chr.
AU - van de Pol,Jan Cornelis
PY - 2012/9/18
Y1 - 2012/9/18
N2 - Model checking of timed automata is a widely used technique. But in order to take advantage of modern hardware, the algorithms need to be parallelized. We present a multi-core reachability algorithm for the more general class of well-structured transition systems, and an implementation for timed automata. Our implementation extends the opaal tool to generate a timed automaton successor generator in c++, that is efficient enough to compete with the UPPAAL model checker, and can be used by the discrete model checker LTSmin, whose parallel reachability algorithms are now extended to handle subsumption of semi-symbolic states. The reuse of efficient lockless data structures guarantees high scalability and efficient memory use. With experiments we show that opaal+LTSmin can outperform the current state-of-the-art, UPPAAL. The added parallelism is shown to reduce verification times from minutes to mere seconds with speedups of up to 40 on a 48-core machine. Finally, strict BFS and (surprisingly) parallel DFS search order are shown to reduce the state count, and improve speedups.
AB - Model checking of timed automata is a widely used technique. But in order to take advantage of modern hardware, the algorithms need to be parallelized. We present a multi-core reachability algorithm for the more general class of well-structured transition systems, and an implementation for timed automata. Our implementation extends the opaal tool to generate a timed automaton successor generator in c++, that is efficient enough to compete with the UPPAAL model checker, and can be used by the discrete model checker LTSmin, whose parallel reachability algorithms are now extended to handle subsumption of semi-symbolic states. The reuse of efficient lockless data structures guarantees high scalability and efficient memory use. With experiments we show that opaal+LTSmin can outperform the current state-of-the-art, UPPAAL. The added parallelism is shown to reduce verification times from minutes to mere seconds with speedups of up to 40 on a 48-core machine. Finally, strict BFS and (surprisingly) parallel DFS search order are shown to reduce the state count, and improve speedups.
KW - METIS-287893
KW - Abstraction
KW - IR-80819
KW - Multi-Core
KW - Model Checking
KW - well-quasi-ordering
KW - EWI-21972
KW - lockless
KW - lattice-based model checking
KW - Timed Automata
KW - Symbolic reachability
KW - Parallel
KW - FMT-MC: MODEL CHECKING
KW - hash table
U2 - 10.1007/978-3-642-33365-1_8
DO - 10.1007/978-3-642-33365-1_8
M3 - Conference contribution
SN - 978-3-642-33365-1
T3 - Lecture Notes in Computer Science
SP - 91
EP - 106
BT - 10th International Conference on Formal Modeling and Analysis of Timed Systems, FORMATS 2012
PB - Springer Verlag
CY - London
ER -