Process Algebra as a Common Framework for Hardware/Software Co-Verification

Matthias Raffelsieper, MohammadReza Mousavi, and Jack Sleuters. IEEE Embedded Systems Letters, 3(1):9--12, 2011.

Abstract

This paper presents the practical issues concerning late and insufficient verification of low-level software on hardware platforms developed by our industrial partner. To overcome these issues we propose a co-verification platform based on process algebra. The descriptions of hardware and software and their interface are translated into a common process-algebraic platform, and formal verification techniques are used to check the conformance of the two descriptions. We present the results of our first attempt towards this goal, discuss the lessons learned, and present the road-map for future research.

Pre-print (in .pdf format)

@article{MousaviESL2010,
    author      = "Raffelsieper, Matthias and Mousavi, MohammadReza and Sleuters, Jack",
    title       = "Process Algebra as a Common Framework for Hardware/Software Co-Verification",
    journal     = "IEEE Embedded Systems Letters",
    year        = "2010"
}