|
 
|
[PP06] Static Reductions for Promela Specifications
Conférence Internationale avec comité de lecture : FORTE 2008 28th IFIP WG 6.1 Int. Conf.rence. Tokyo, Japan, January 2006, pp.84-98, Series LNCS 5048,
motcle:
Résumé:
The interleaving of concurrent processes actions leads to a combinatory explosion. There exists in Petri nets theory some structural reductions that combat the state explosion by agglomerating sequences of transitions into a single atomic transition. These reductions are easily checkable and preserve deadlocks, Petri nets liveness and any LTL formula that do not observe the modified transitions. Furthermore, they can be combined with others kinds of reductions such like partial-order techniques to obtain very effective reductions. We propose in this paper to adapt these reductions to Promela specifications by proposing some simple rules which give the possibility to automatically infer atomic steps in the Promela model while preserving the checked property. We demonstrate on typical example the efficiency of this approach and we propose some perspectives of this work.
BibTeX
| @inproceedings { | |||
| PP06, | |||
| title | = | "{Static Reductions for Promela Specifications}", | |
| author | = | " C. Pajault and J. Pradat-Peyre ", | |
| booktitle | = | "{FORTE 2008 28th IFIP WG 6.1 Int. Conf.rence. Tokyo, Japan}", | |
| year | = | 2006, | |
| month | = | "January", | |
| series | = | "LNCS 5048", | |
| pages | = | "84-98", | |
| } | |||
