Skip to main content

Formal Complexity-Oriented Performance-Critical Design and Verification Framework

Suleiman Abu Kharmeh, Formal Complexity-Oriented Performance-Critical Design and Verification Framework. PhD thesis. University of Bristol. August 2012. PDF, 2704 Kbytes.

Abstract

This thesis develops a formal framework for the specification, complexity analysis and verification of functional and performance requirements of configurable communica- tion systems and protocols. The main objective is demonstrating the applicability of the proposed framework for the modelling and verification of a realistic system. Design-for-Verification principles are demonstrated, such as the semantic analysis and decomposition of complex and intertwined requirements, and the subsequent composition of orthogonal functional units with manageable complexities. Tock-CSP was used to model those functional units and their interfaces. Analysis of the underlying state machines of the mod- elled system resulted in the identification of complexity and scalability issues. Then, through the development and application of formal complexity analysis techniques for state machines, modelling optimisations were possible. Complexity issues of the model-checker were also identified and resolved. Adoption challenges of formal meth- ods were addressed by the development of suitable specification and verification in- terfaces. The properties of the configurable system and its ISA-Oriented interface were verified using various refinement models including the Tau Priority Model. Fi- nally, the conformance of the ISA-Oriented Specification methodology to abstract specifications of selected communication protocols was also verified. This thesis is the first to devise mathematical techniques for expressing and analysing the state-space complexity of formal models, the first to develop and use waveform visualisation for the analysis of timing specifications of formal models, and the first application of the newly released Tau Priority Model.

Bibtex entry.

Contact details

Publication Admin