Integrating Model-Checking with UML-based SoC Development

In order to address the complexities of SoC design, rigorous development methods and automated tools are required. This paper presents an approach to formal verification using model-checking, designed for use in the context of a UML-based SoC design flow. Different UML models can be automatically translated into CSP by the UML2CSP tool that has been developed in this work. The translated models can be checked for consistency with the model-checker FDR. Checks can also be carried out to determine whether models exhibit specified properties. The overall objective of the work is to ensure that only correct models are carried into the later stages of development where they are partitioned, and implementations are synthesised.

• Type: Conference
• Year: 2005
• Where: FDL
• Authors: Peter Green, Kinika Tasie-Amadi
• Keywords: FDL 2005, Rigorous Development Methods, SoC Design, UML-based SoC Design