Research on Process Algebraic Analysis Tools for Electronic System Design

摘要

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 performance 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 Temporal Logic (LTL) model checking and refinement. SHE methodology provides means for correctness and performance analysis by applying model-driven design methodology 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 system. 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, development 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 communication model, respectively.