Technical Reports
HPL-2008-184
Click here for full text:
Demos2k as a Bridge to Formal Methods
Taylor, Richard; Tofts, Chris
HP Laboratories
HPL-2008-184
Keyword(s): Concurrency, Multi Core, Parallelism, Formal, Analysis, Simulation, Visualisation
Abstract: With multi core computing systems becoming commonplace it has been recognised that their full potential can only be exploited by using explicitly parallel programming solutions. It has long been known that this class of programs is difficult to constrcut correctly, difficult to demonstrate efficient and a major problem to maintain. Although formal approaches to these programming situations have demonstrated many point successes, their widespread adoption has been limited by the (reasonable) belief that they are too technically challenging and time consuming to deliver value to a project. In this paper we illustrate, via an extended example, how a formally based process based simulation language (DEMOS2k) provides a mid point between concept, implementation and formal analysis. Furthermore, regarded as a rapid software prototyping system it gives a rapid visualisation of how the algorithm concept will execute in a concurrent setting.
15 Pages
External Posting Date: October 21, 2008 [Fulltext]. Approved for External Publication
Internal Posting Date: October 21, 2008 [Fulltext]