Title: Abstract property language for MDG model checking methodology

Authors: Sa'ed Abed; Kamran Hussain; Otmane Ait-Mohamed

Addresses: Department of Computer Engineering, Hashemite University, PO Box 150459, Zarqa 13115, Jordan ' Department of Electrical and Computer Engineering, Concordia University, Montreal H3G 1M8, Canada ' Department of Electrical and Computer Engineering, Concordia University, Montreal H3G 1M8, Canada

Abstract: 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.

Keywords: APL; abstract property language; MDGs; multiway decision graphs; PSL; property specification language; verification-ready MDG models; front-end translators; model checking; model verification.

DOI: 10.1504/IJCAT.2012.048205

International Journal of Computer Applications in Technology, 2012 Vol.44 No.1, pp.23 - 36

Published online: 26 Jul 2012 *

Full-text access for editors Full-text access for subscribers Purchase this article Comment on this article