RT-MOBS: A compositional observer semantics of time Petri net for real-time property specification language based on mu-calculus

【Author】 Ge, Ning; Dal Zilio, Silvano; Liu, Hongyu; Zhang, Li; Zhang, Lianyi

【Source】SCIENCE OF COMPUTER PROGRAMMING

【影响因子】1.039

【Abstract】We define a new verification method, called RT-MOBS, for checking real-time requirements based on Time Petri nets (TPN). Our approach supports requirements specified using a very expressive pattern language, the Property Specification Language (PSL) of Autili, Grusnke et al., and relies on marking observers' verification. RT-MOBS has many distinctive features, such as a focus on performances, a compositional method for deriving the observer and the target property directly from the structure of the specification pattern, and the ability to deal with the whole real-time fragment of PSL. We demonstrate the effectiveness of our approach from three industrial use cases: a mobile ad-hoc network system; the model of a flight management system, which is realistic with respect to the industry use during the architecture evaluation phase; and a model of an order to cash smart contract. Our experimental results show that we can achieve performances that are several orders of magnitude better than with methods based on an interpretation of patterns into Linear Temporal Logic (LTL) formulas. (C) 2021 Elsevier B.V. All rights reserved.

【Keywords】Real-time requirements; Property specification patterns; Model checking; Observer; Time Petri net

【发表时间】2021 2022-06-01

【收录时间】2022-01-02

【文献类型】

【主题类别】

--