An algorithm to generate the context-sensitive synchronized control flow graph

The verification of industrial systems specified with CSP often implies the analysis of many concurrent and synchronized components. The cost associated to these analyses is usually very high, and sometimes prohibitive, due to the complexity imposed by the non-deterministic execution order of processes and to the restrictions imposed on this order by synchronizations. To overcome this problem, there has been a recent proposal that allows to statically simplify a specification before the analyses. This simplification allows to drastically reduce the time needed by the analyses because it reduces the state explosion. Unfortunately, the approach has been implemented but it has not been formalized neither proved correct. In this paper, we formally define the data structures needed to automatically simplify a CSP specification and we define an algorithm able to automatically generate these data structures. Categories and Subject Descriptors D.3.3 [Software]: Programming Languages—...

• Type: Conference
• Year: 2010
• Where: SAC
• Authors: Marisa Llorens, Javier Oliver, Josep Silva, Salvador Tamarit
• Keywords: Applied Computing, Concurrent Programming Structures, Data Structures, Non-deterministic Execution Order, SAC 2010