Abstract property language for MDG model checking methodology

摘要

In this paper, we propose a new specification language called Abstract Property Language (APL) suitable for Multiway Decision Graph (MDG) Model Checking (MC) that replaces L_(MDG) language and introduces new operators obtained from Property Specification Language (PSL). The purpose is to improve expressiveness and to enhance MC verification technique in MDG. Though, the PSL language was modified to model system properties at the same level of abstraction. We provide formal definition in BNF grammar format and formal semantics. APL is associated with a front-end translator that accepts APL specifications and builds verification-ready models to be handled by MDG tool.