Chapter 32 Research on Process Algebraic Analysis Tools for Electronic System Design
Ka Lok Man, Tomas Krilavi · 2010
cius Abstract Rapid software/hardware development cycle increased demand for the advanced design and implementation methods. Recently, formal methods have been put forward as a tool for modelling and analysis of electronic systems. Usage of formal semantics and syntax allows unambiguous specifications of the systems, and in such a way provides means for rigorous analysis of correctness and perfor- mance properties. We investigate applicability of two process algebra based tools for the mixed software/hardware modelling and analysis: Process Analysis Toolkit (PAT) and Software/Hardware Engineering (SHE). PAT toolkit is based on CSP-like process algebra extended with mechanisms customary for software developers and engineers. It supports reachability and deadlock analysis, complete Linear Tempo- ral Logic (LTL) model checking and refinement. SHE methodology provides means for correctness and performance analysis by applying model-driven design method- ology at the system level, i.e., high abstraction level design stage of the embedded and mixed hardware/software systems. It combines techniques for development of formal models for analysis and refinement to the actual implementation of the sys- tem. SHE toolset provides tools for modelling, simulation and real-time control code generation. Transaction Level Modelling (TLM) approach has been put forward as a tool for elaborate System-on-Chip (SoC) design. It is quite extensively applied in industry to solve a number of practical problems, occurring at the design, develop- ment and deployment stages. We apply PAT and SHE methodology for functional and performance analysis of a hardware model and a TLM model, and illustrate this by means of examples: a simple pipeline process and a process-memory communi- cation model, respectively.