Loading...
Linking a "state-rich" process algebra to a "state-free" process algebra to verify software / hardware implementations
Date
2010
Abstract
Following the development of formalisms based on data and behavioural aspects of the system, there are number of attempts in which these two formalisms are mixed together to get benefit of both paradigms. 'Circus' being a living specification language with continuous collaboration from both academia and industry, is a combination of Z, CSP and the refinement calculus. To make use of the available and industry-proven tools for a particular programming paradigm, there is a need to develop a formally verified link between the one world and the other. The aim of this work is to develop a formally verified link between a state-rich process algebra i.e. 'Circus' to a state-free process algebra i.e. CSP. To achieve the research goal, the most suitable available tools are to identify. For developing link between targeted formal languages, we will identify the key translations required between the two languages. For ensuring correctness of the translation, we will formalise the key translation / refinement steps. These will form the theoretical core of the work and support the soundness of the link. In the end, we will select and verify a case study from the collection of software / hardware protocols.
Supervisor
Description
peer-reviewed
Publisher
Citation
International Conference on Frontiers of Information Technology 2010;
Files
Loading...
Beg-Linking.pdf
Adobe PDF, 311.58 KB
Keywords
Funding code
Funding Information
Science Foundation Ireland (SFI), Higher Education Authority (HEA), PARTLI4
Sustainable Development Goals
External Link
Type
Meetings and Proceedings
Rights
https://creativecommons.org/licenses/by-nc-sa/1.0/