CSP is a powerful language for specifying complex concurrent systems. Due to the non-deterministic execution order of processes and to synchronizations, many analyses such as deadlock analysis, reliability analysis, and program slicing try to predict properties of the specification which can guarantee the quality of the final system. These analyses often rely on the use of CSP's traces. In this work, we introduce the theoretical basis for tracking concurrent and explicitly synchronized computations in process algebras such as CSP. Tracking computations is a difficult task due to the subtleties of the underlying operational semantics which combines concurrency, non-determinism and non-termination. We define an instrumented operational semantics that generates as a side-effect an appropriate data structure (a track) which can be used to track computations. Formal definition of a tracking semantics improves the understanding of the tracking process, but also, it allows to formally prove the correctness of the computed tracks. © 2010 Springer-Verlag Berlin Heidelberg.
CITATION STYLE
Llorens, M., Oliver, J., Silva, J., & Tamarit, S. (2010). A tracking semantics for CSP. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 6120 LNCS, pp. 248–270). https://doi.org/10.1007/978-3-642-13321-3_15
Mendeley helps you to discover research relevant for your work.