You are here
Verified communication modelling of embedded systems in SystemC
Submitted by Sergey Balandin on 13.10.09
Background and Motivation:
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.
Project Summary:
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.
Project goals and future research directions:
<p>Next focus in our research will be in the formal verification aspects of SystemC modelling. The objective will be in creating a bridge between the formal, correct-by-construction system description and the transaction level model in SystemC. Within the next six months we will explore issues including: - Applying formal verification methods to the SystemC 2.2 scheduler and the TLM-2.0 modelling library. - Problems concerning implementation of formal Action Systems model details in SystemC simulation, for example blocking vs. non-blocking communication scheme and the functionality of a shared communication channel arbiter.</p>
List of team members and their organizations:
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
Status:
Graduate
Final deadline:
Monday, April 27, 2009 (All day)
Users:
Group:
