Talks and Poster Presentations (with Proceedings-Entry):
S. Jaksic, E. Bartocci, R. Grosu, R. Kloibhofer, T. Nguyen, D. Nickovic:
"From Signal Temporal Logic to FPGA Monitors";
Talk: 13th ACM-IEEE International Conference on Formal Methods and Models for System Design,
Austin, TX, USA;
2015-09-21
- 2015-09-23; in: "Proc. of MEMOCODE 2015: the 13th ACM-IEEE International Conference on Formal Methods and Models for System Design",
IEEE,
(2015),
218
- 227.
English abstract:
Due to the heterogeneity and complexity of systems-of-systems (SoS), their simulation is becoming very time consuming, expensive and hence impractical. As a result, design simulation is increasingly being complemented with more efficient design emulation.
Runtime monitoring of emulated designs would provide a precious support in the verification activities of such complex systems.
We propose novel algorithms for translating signal temporal logic (STL) assertions to hardware runtime monitors implemented in field programmable gate array (FPGA). In order to accommodate to this hardware specific setting, we restrict ourselves to past and bounded future temporal operators interpreted over discrete time.
We evaluate our approach on two examples: the mixed signal bounded stabilization; and the serial peripheral interface (SPI) communication protocol.
These case studies demonstrate the suitability of our approach for runtime monitoring of both digital and mixed signal systems.
"Official" electronic version of the publication (accessed through its Digital Object Identifier - DOI)
http://dx.doi.org/10.1109/MEMCOD.2015.7340489