| GIM>Research>Verification of Embe...
| RESEARCH LINE: |
| ||Verification of Embedded Systems |
| Select these links to see PROJECTS or PUBLICATIONS within this research line |
| STAFF: |
Pablo Pedro Sánchez (Responsible for this Research Line) |
| WORK FIELDS: |
|This research area continues the activity in test synthesis and VHDL test application and is closely related to the research in embedded systems specification and design. As a practical exploitation of this know-how, several verification plans for industrial design projects were made [UgSV02][BCHP03a][BCHP03b]. |
Embedded systems verification started as a consequence of the stay of Pablo Sánchez in the MESDAT of the University of California at San Diego (USA). During the stay, Pablo Sánchez explored techniques applicable to systems able to be described with polynomials [SaDe99]. The main objective of these techniques is to find input values provoking the violation of any of the properties and restrictions defined by the designer. The proposed techniques are based on a modification of the interval arithmetic [UgSa03a]. First results in verifying systems described at the algorithmic level without loops are very promising [UgSa03b][UgSa03c]. This activity is being carried out in the CICYT project [PRO05] previously mentioned.
The experience gained in the SystemC simulation kernel allows to modify it in order to ensure a pseudo-random selection of the concurrent processes. The proposed technique improves the verification quality by exploring different posible execution modes of the same input set. [HeVi06b]. This activity is being carried out in the CICYT project [PRO05]. In the IST 033511 ANDRES project, an extension of the OSCI SystemC reference kernel was developed in order to support the Exhaustive Coverage of Schedulings of critical parts in the SystemC specification were the concurrent activity may cause indeterminism [HeVi09].