Technical Reports


Click here for full text: PDF

Demos2k as a Bridge to Formal Methods

Taylor, Richard; Tofts, Chris
HP Laboratories


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]

Back to Index