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

Ning Ge, Silvano Dal Zilio, Hongyu Liu, Li Zhang, Lianyi Zhang
Science of Computer Programming 206, apr 2021.

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.

Citation

#

@Article{DalzilioS:scp2021rtmobs,
   author  = {Ge, Ning and {Dal Zilio}, Silvano and Liu, Hongyu and Zhang, Li and Zhang, Lianyi},
   title   = {{RT-MOBS: A compositional observer semantics of time Petri net for real-time property specification language based on μ-calculus}},
   journal = {Science of Computer Programming},
    volume  = {206},
   doi = {10.1016/j.scico.2021.102624},
   month   = apr, 
   year    = 2021
}