Relating and Visualising CSP, VCR and Structural Traces

Brown, Neil C.C. and Smith, Marc L. (2009) Relating and Visualising CSP, VCR and Structural Traces. In: Welch, Peter H. and Roebbers, Herman W. and Broenink, Jan F. and Barnes, Frederick R.M. and Ritson, Carl G. and Sampson, Adam T. and Stiles, Gardiner S. and Vinter, Brian, eds. Communicating Process Architectures 2009. Concurrent Systems Engineering . IOS Press, Amsterdam, Netherlands, pp. 182-196. ISBN 978-1-60750-065-0. E-ISBN 978-1-60750-513-6. (doi:10.3233/978-1-60750-065-0-89)

Abstract

As well as being a useful tool for formal reasoning, a trace can provide insight into a concurrent program's behaviour, especially for the purposes of run-time analysis and debugging. Long-running programs tend to produce large traces which can be difficult to comprehend and visualise. We examine the relationship between three types of traces (CSP, VCR and Structural), establish an ordering and describe methods for conversion between the trace types. Structural traces preserve the structure of composition and reveal the repetition of individual processes, and are thus well-suited to visualisation. We introduce the Starving Philosophers to motivate the value of structural traces for reasoning about behaviour not easily predicted from a program's specification. A remaining challenge is to integrate structural traces into a more formal setting, such as the Unifying Theories of Programming – however, structural traces do provide a useful framework for analysing large systems.

Item Type:	Book section
DOI/Identification number:	10.3233/978-1-60750-065-0-89
Uncontrolled keywords:	determinacy analysis, Craig interpolants
Subjects:	Q Science > QA Mathematics (inc Computing science) > QA 76 Software, computer programming,
Divisions:	Faculties > Sciences > School of Computing > Programming Languages and Systems Group
Depositing User:	Neil Brown
Date Deposited:	21 Sep 2012 09:49 UTC
Last Modified:	03 Jun 2019 09:09 UTC
Resource URI:	https://kar.kent.ac.uk/id/eprint/30580 (The current URI for this page, for reference purposes)