Difference between revisions of "Publications/pommellet.20.isse"
From LRDE
(5 intermediate revisions by 2 users not shown) | |||
Line 5: | Line 5: | ||
| title = LTL Model Checking for Communicating Concurrent Programs |
| title = LTL Model Checking for Communicating Concurrent Programs |
||
| journal = Innovations in Systems and Software Engineering: a NASA journal (ISSE) |
| journal = Innovations in Systems and Software Engineering: a NASA journal (ISSE) |
||
− | | volume = |
+ | | volume = 16 |
− | | number = |
+ | | number = 2 |
− | | pages = |
+ | | pages = 161 to 179 |
| publisher = Springer |
| publisher = Springer |
||
+ | | lrdepaper = http://www.lrde.epita.fr/dload/papers/pommellet.20.isse.pdf |
||
| lrdeprojects = Spot |
| lrdeprojects = Spot |
||
| lrdenewsdate = 2020-05-15 |
| lrdenewsdate = 2020-05-15 |
||
− | | abstract = We present in this paper a new approach to the static analysis of concurrent programs with procedures. To this end, we model multi-threaded programs featuring recursive procedure calls and synchronisation by rendez-vous between parallel threads with communicating pushdown systems (from now on CPDSs). The reachability problem for this particular class of automata is unfortunately undecidable. However, it has been shown that an efficient abstraction of the execution traces language can nonetheless be computed. To this end, an algebraic framework to over-approximate context-free languages has been introduced by Bouajjani et al. In this paper, we combine this framework with an automata-theoretic approach in order to approximate an answer to the model checking problem of the linear-time temporal logic (from now on LTL) on CPDSs. We then present an algorithm that, given a single-indexed or |
+ | | abstract = We present in this paper a new approach to the static analysis of concurrent programs with procedures. To this end, we model multi-threaded programs featuring recursive procedure calls and synchronisation by rendez-vous between parallel threads with communicating pushdown systems (from now on CPDSs). The reachability problem for this particular class of automata is unfortunately undecidable. However, it has been shown that an efficient abstraction of the execution traces language can nonetheless be computed. To this end, an algebraic framework to over-approximate context-free languages has been introduced by Bouajjani et al. In this paper, we combine this framework with an automata-theoretic approach in order to approximate an answer to the model checking problem of the linear-time temporal logic (from now on LTL) on CPDSs. We then present an algorithm that, given a single-indexed or stutter-invariant LTL formula, allows us to prove that no run of a CPDS verifies this formula if the procedure ends. |
| type = article |
| type = article |
||
| id = pommellet.20.isse |
| id = pommellet.20.isse |
||
Line 18: | Line 19: | ||
@Article<nowiki>{</nowiki> pommellet.20.isse, |
@Article<nowiki>{</nowiki> pommellet.20.isse, |
||
author = <nowiki>{</nowiki>Adrien Pommellet and Tayssir Touili<nowiki>}</nowiki>, |
author = <nowiki>{</nowiki>Adrien Pommellet and Tayssir Touili<nowiki>}</nowiki>, |
||
− | title = <nowiki>{</nowiki>LTL Model Checking for Communicating Concurrent |
+ | title = <nowiki>{</nowiki><nowiki>{</nowiki>LTL<nowiki>}</nowiki> Model Checking for Communicating Concurrent |
+ | Programs<nowiki>}</nowiki>, |
||
journal = <nowiki>{</nowiki>Innovations in Systems and Software Engineering: a NASA |
journal = <nowiki>{</nowiki>Innovations in Systems and Software Engineering: a NASA |
||
journal (ISSE)<nowiki>}</nowiki>, |
journal (ISSE)<nowiki>}</nowiki>, |
||
year = 2020, |
year = 2020, |
||
− | volume = <nowiki>{</nowiki> |
+ | volume = <nowiki>{</nowiki>16<nowiki>}</nowiki>, |
− | number = <nowiki>{</nowiki> |
+ | number = <nowiki>{</nowiki>2<nowiki>}</nowiki>, |
− | pages = <nowiki>{</nowiki> |
+ | pages = <nowiki>{</nowiki>161--179<nowiki>}</nowiki>, |
month = jun, |
month = jun, |
||
publisher = <nowiki>{</nowiki>Springer<nowiki>}</nowiki>, |
publisher = <nowiki>{</nowiki>Springer<nowiki>}</nowiki>, |
||
Line 31: | Line 33: | ||
end, we model multi-threaded programs featuring recursive |
end, we model multi-threaded programs featuring recursive |
||
procedure calls and synchronisation by rendez-vous between |
procedure calls and synchronisation by rendez-vous between |
||
− | parallel threads with |
+ | parallel threads with communicating pushdown systems (from |
− | + | now on CPDSs). |
|
The reachability problem for this particular class of |
The reachability problem for this particular class of |
||
Line 43: | Line 45: | ||
In this paper, we combine this framework with an |
In this paper, we combine this framework with an |
||
automata-theoretic approach in order to approximate an |
automata-theoretic approach in order to approximate an |
||
− | answer to the model checking problem of the |
+ | answer to the model checking problem of the linear-time |
− | + | temporal logic (from now on LTL) on CPDSs. We then present |
|
− | + | an algorithm that, given a single-indexed or |
|
⚫ | |||
− | \emph<nowiki>{</nowiki>single-indexed<nowiki>}</nowiki> or \emph<nowiki>{</nowiki>stutter-invariant<nowiki>}</nowiki> LTL |
||
+ | run of a CPDS verifies this formula if the procedure |
||
⚫ | |||
− | + | ends.<nowiki>}</nowiki>, |
|
doi = <nowiki>{</nowiki>10.1007/s11334-020-00363-6<nowiki>}</nowiki> |
doi = <nowiki>{</nowiki>10.1007/s11334-020-00363-6<nowiki>}</nowiki> |
||
<nowiki>}</nowiki> |
<nowiki>}</nowiki> |
Latest revision as of 08:57, 5 November 2020
- Authors
- Adrien Pommellet, Tayssir Touili
- Journal
- Innovations in Systems and Software Engineering: a NASA journal (ISSE)
- Type
- article
- Publisher
- Springer
- Projects
- Spot
- Date
- 2020-05-15
Abstract
We present in this paper a new approach to the static analysis of concurrent programs with procedures. To this end, we model multi-threaded programs featuring recursive procedure calls and synchronisation by rendez-vous between parallel threads with communicating pushdown systems (from now on CPDSs). The reachability problem for this particular class of automata is unfortunately undecidable. However, it has been shown that an efficient abstraction of the execution traces language can nonetheless be computed. To this end, an algebraic framework to over-approximate context-free languages has been introduced by Bouajjani et al. In this paper, we combine this framework with an automata-theoretic approach in order to approximate an answer to the model checking problem of the linear-time temporal logic (from now on LTL) on CPDSs. We then present an algorithm that, given a single-indexed or stutter-invariant LTL formula, allows us to prove that no run of a CPDS verifies this formula if the procedure ends.
Documents
Bibtex (lrde.bib)
@Article{ pommellet.20.isse, author = {Adrien Pommellet and Tayssir Touili}, title = {{LTL} Model Checking for Communicating Concurrent Programs}, journal = {Innovations in Systems and Software Engineering: a NASA journal (ISSE)}, year = 2020, volume = {16}, number = {2}, pages = {161--179}, month = jun, publisher = {Springer}, abstract = {We present in this paper a new approach to the static analysis of concurrent programs with procedures. To this end, we model multi-threaded programs featuring recursive procedure calls and synchronisation by rendez-vous between parallel threads with communicating pushdown systems (from now on CPDSs). The reachability problem for this particular class of automata is unfortunately undecidable. However, it has been shown that an efficient abstraction of the execution traces language can nonetheless be computed. To this end, an algebraic framework to over-approximate context-free languages has been introduced by Bouajjani et al. In this paper, we combine this framework with an automata-theoretic approach in order to approximate an answer to the model checking problem of the linear-time temporal logic (from now on LTL) on CPDSs. We then present an algorithm that, given a single-indexed or stutter-invariant LTL formula, allows us to prove that no run of a CPDS verifies this formula if the procedure ends.}, doi = {10.1007/s11334-020-00363-6} }