Many applications of Cyber-Physical Systems (CPS) play a crucial role in shaping the quality of life. The malfunction of such systems can lead to dangerous consequences, hence safety takes an important role. One of the common issues of CPS is the variability of event delays. This paper addresses formal verification of system ability to withstand event delays. To achieve such property, we use the concept of event timestamps. The paper proposes changes in IEC 61499 syntax to introduce timestamps into the programming language. The application of new syntax introduces better opportunities for formal verification. We enhanced FB2SMV tool to generate SMV models automatically from the initial system. The paper presents a case study of an elevator system that illustrates the proposed approach. Results of verification show that the system can perform time-aware computations. The proposed approach has shown better verification performance compared to timestamps manually added through the data connections between function blocks.