Difference between revisions of "Publications/pommellet.20.isse"
From LRDE
Line 11: | Line 11: | ||
| 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 31: | Line 31: | ||
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 43: | ||
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> |
Revision as of 14:36, 3 July 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.
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 = {??}, number = {??}, pages = {??--??}, 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} }