is the formalisation of a reasonable subset of SystemC based on the classical process algebras ACP (Algebra of Communicating Processes) and ATP (A timed process algebra for specifying real-time systems). The semantics of is defined by means of deduction rules that associate a labelled transition system with a process. A set of properties is presented for a notion of bisimilarity.

Highlights

is aimed at giving formal specifications of SystemC designs and to perform formal analysis of SystemC processes. Furthermore, is a single-formalism that can be used for specifying concurrent systems, finite state systems and real-time systems (as in SystemC). Desired properties (e.g. safety and liveness) of these systems specified in can be verified with existing formal verification tools (e.g. SMV, SPIN and Uppaal) by translating them formally into different formalisms that are the input languages of the formal verification tools (i.e. single-formalism-multi-solution).

Transaction Level Modelling (TLM) is a relatively young kind of approach meant to ease the handling of the constantly growing complexity of electronic systems; by raising the level of abstraction it allows system architects, embedded software engineers, and system developers, to explore architectural alternatives, to start software development, and to produce raw performance estimation at a much earlier stage than it would be possible if a Register Transfer Level (RTL) description of the system were used as platform reference.

With alternatives exploration in mind, the main advantage of TLM is the simulation speed-up that it offers w.r.t. cycle-accurate representation, essentially due to the different abstraction level, which turns into a much smaller amount of information to be handled. The main disadvantage shown by TLM, so far, is the lack of a formal semantics, that could be used both for consistency checking during description refinement, and for property checking on untimed descriptions, mainly aimed at checking functional correctness on an abstraction of the final system. Various attempts to give TLM a formal background have already been made, but none of those has proposed a framework to allow checking on specific aspects of the component being designed with the most suited formal checking tool. To reach such a goal we have focused our attention on SystemC as a language for TLM, and selected as the language to formally represent SystemC designs.

In the frame of a tight collaboration between industrial entities and research institute CEOL (Centre for Efficiency-Oriented Languages), several tools for are currently being developed. These tools enable automatic translations from SystemC codes to specifications and from specifications to various formalisms that are the input languages of some existing formal verification tools. Using tools in combination with some formal verification tools yields automatic verifications of SystemC designs via specifications (for different verification purposes).

This research activity is currently funded by
Solari - Hong Kong (http://www.solari-hk.com/)

and partnered with
International Software and Productivity Engineering Institute - USA (http://www.intspei.com),
Intelligent Support Ltd. - United Kingdom (http://www.isupport-ltd.co.uk) and
Minteos - Italy (http://www.minteos.com).

For questions, suggestions and comments, please send mail to SystemCFL@gmail.com