[lecture notes in electrical engineering] information science and applications (icisa) 2016 volume 376 translating basic metric temporal logic formulas into promela精品.pdfVIP

Translating Basic Metric Temporal Logic Formulas into Promela Punwess Sukvanich, Arthit Thongtak and Wiwat Vatanawood AbstractTo formally verify the real-time system using model checking tech- nique, two necessary elements are required, the real-time system model and its expected real-time properties. In order to specify these real-time properties, an appropriate extended logic system, to cope with quantitative of time constraints is needed. We select one of the most popular real-time logic systems, called Metric Temporal Logic (MTL) to specify our mentioned real-time properties. However, the real-time properties defined in MTL are still not relevant to SPIN model checker. In this paper, we propose a novel scheme to translate the basic MTL for- mulas into Promela and LTL formulas as to be relevantly used in SPIN, in terms of Promela’s inline definitions and macro commands. The punctuality of the for- mulas is preserved during the translation. Practically, the basic timing constraints eventually and always operators of MTL are focused, and the translation of MTL formulas of the real-time safety property patterns is demonstrated. Keywords Metric Temporal Logic · MTL · Promela · SPIN · Model checking 1 Introduction The effort for verifying the correctness of the safety-critical systems, such as medi- cal devices, automotive and aerospace system, is significantly huge in their devel- opment [1]. The real-time system development needs the same processes under the strict time line [2-5]. The low cost and high efficiency and effectiveness of the veri- fication procedures are helpful and become the essential step in the development. Several formal verification approaches are proposed, but the model checking ap- proach is the one that provided the promisingly automated exhaustive verification. P. Sukvanich() · A. Thongtak · W. Vatanawoo