Temporal Property-Based Testing of a Timed C Compiler using Time-Flow Graph Semantics
| العنوان: | Temporal Property-Based Testing of a Timed C Compiler using Time-Flow Graph Semantics |
|---|---|
| المؤلفون: | Natarajan, Saranya, Broman, David, 1977 |
| المصدر: | Proceedings of the 2020 Forum on specification & Design Languages (FDL) 2020 Forum on specification & Design Languages (FDL).. :1-8 |
| الوصف: | The correctness of a real-time system depends both on it being logically sound and temporally correct. To guarantee temporal correctness, the development of such systems includes: (i) developing a model, (ii) formally verifying the model, and (iii) implementing the verified model using a programming language. The temporal correctness then depends on correctly implementing the model using a real-time programming language and compiling it to a hardware platform. Although the timing semantics of many real-time programming languages are well defined, there is no guarantee that the timing semantics of such programs are correctly translated by the compiler. In this paper, we propose a new method for temporal property-based testing. The general method is implemented and evaluated on the Timed C real-time programming language. We formalize the temporal core semantics of Timed C and then use this formalization to specify the properties that are tested by the new property-based testing tool. More specifically, the tool consist of two parts: (i) a generator that randomly generates Timed C programs, and (ii) a property checker that checks whether the language's timing semantics are correctly captured in its execution. We evaluate the method and tool on an embedded Raspberry Pi platform. |
| وصف الملف: | electronic |
| URL الوصول: | https://urn.kb.se/resolve?urn=urn:nbn:se:kth:diva-292191 https://ieeexplore.ieee.org/xpl/conhome/9226655/proceeding http://fdl-conference.org/FDL2020/index.html https://kth.diva-portal.org/smash/get/diva2:1540046/FULLTEXT01.pdf |
| قاعدة البيانات: | SwePub |
| DOI: | 10.1109/FDL50818.2020.9232935 |
|---|