Generic Framework Architecture for Verifying Embedded Components

This dissertation presents a framework for the formal verification of standard embedded components such us bus protocol, microprocessor, memory blocks, various IP blocks, and a software component. It includes a model checking of embedded systems components. The algorithms are modeled on SystemC and transformed on Promela language (PROcess or PROtocol MEta LAnguage) with the integration of LTL (Linear Temporal Logic) properties extracting from state machines in order to reduce verification complexity. Thus, SysVerPml is not only dedicated to verifying generated properties but also for the automation integration of other properties in models if needed. In the following, we will provide the answer to the problems of component representation on the design system, what properties are appropriate for each component, and how to verify properties.

@article{ELJADIRI2020,
  title     = {Generic Framework Architecture for Verifying Embedded Components},
  journal   = {International Journal of Advanced Computer Science and Applications},
  volume    = {11},
  number    = {6},
  year      = {2020},
  publisher = {The Science and Information Organization},
  author    = {Lamia ELJADIRI and Ismail ASSAYAD},
  doi       = {10.14569/IJACSA.2020.0110639},
  url       = {https://doi.org/10.14569/IJACSA.2020.0110639}
}