TY - GEN
T1 - Research on process algebraic analysis tools for electronic system design
AU - Man, Ka Lok
AU - Krilavicius, Tomas
PY - 2010
Y1 - 2010
N2 - 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.
AB - 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.
KW - Interoperability
KW - Process algebra
KW - Simulation
KW - Transaction level modelling
KW - Verification
UR - http://www.scopus.com/inward/record.url?scp=84867320360&partnerID=8YFLogxK
U2 - 10.1007/978-90-481-3517-2-32
DO - 10.1007/978-90-481-3517-2-32
M3 - Conference Proceeding
AN - SCOPUS:84867320360
SN - 9789048135165
T3 - Lecture Notes in Electrical Engineering
SP - 415
EP - 427
BT - Intelligent Automation and Computer Engineering
T2 - International Conference in Intelligent Automation and Computer Engineering, Under the Auspices of the International MultiConference of Engineers and Computer Scientists, IMECS 2009
Y2 - 18 March 2009 through 20 March 2009
ER -