You are here
Verified communication modelling of embedded systems in SystemC
Verifying the correctness of a modern hardware or HW/SW system design keeps claiming more and more time and resources than before. Verification process of complex multiprocessor and reconfigurable systems brings up new challenges for both researchers and developers in the industry. Verification by test bench simulation is the prevailing approach to this issue. Another approach to a system verification task includes the use of formal methods. By specifying system in a formal design language developer is able to verify the model in a mathematically rigorous manner. Based on a formal specification the design is correct-by-construction and the role of simulation in the verification of the system's logical behaviour can be reduced. However, the industry lacks comprehensive tools that can be used in a formal, stepwise development of embedded HW/SW systems throughout the design project all the way from an abstract specification down to an implementable model. Action Systems is a formal language that provides a method for specifying and verifying modular HW/SW systems. In addition, it uses a framework called refinement calculus, which is a stepwise development method for refining an abstract specification down to a model that can be translated into a suitable implementation. On the other hand, SystemC is a system modelling library that is built on top of the standard C++ programming language. In addition to the object oriented software development techniques provided by C++, SystemC offers a system designer an extensive variety of hardware-oriented modelling features. Now there is also a new standardised TLM-2.0 framework for SystemC communication modelling at transaction level.
The long term goal is to develop a combined framework, in which Action Systems provides a formal foundation for SystemC communication modelling at transaction level. This would provide a developer the means to produce a simulatable system description from an Action Systems description while preserving the formal correctness throughout the model's refinement process as well as during simulation. Thus, the long term goals of the research are: - Producing a method for creating formally verified transaction level SystemC models of communication schemes in a distributed system. - Producing a formal stepwise method for refining a verified transaction level SystemC model into an implementation level model.
Elena Suvorova, PhD, associate professor, Saint-Petersburg University of Airspace Instrumentation (SUAI) Valentin Olenev, Researcher, SUAI Michel Gillet, Nokia Tutors: Sergey Balandin, Nokia Yuriy Sheynin, SUAI