The following information was submitted:
Transactions: WSEAS TRANSACTIONS ON CIRCUITS AND SYSTEMS
Transactions ID Number: 32-862
Full Name: Sa'ed Abed
Position: Assistant Professor
Age: ON
Sex: Male
Address: Faculty of Engineering, Department of Computer Engineering, P.O. Box 150459, Zarqa 13115
Country: JORDAN
Tel: 00962 (5) 390-3333 Ext. 4654
Tel prefix:
Fax: 00962 5 3826613
E-mail address: sabed@hu.edu.jo
Other E-mails: sabed70@yahoo.com
Title of the Paper: Abstract Property Language for MDG Model Checking Methodology
Authors as they appear in the Paper: Kamran Hussain, Otmane Ait Mohamed and Sa'ed Abed
Email addresses of all the authors: k_hussai@ence.concordia.ca, ait@ence.concordia.ca,sabed@hu.edu.jo
Number of paper pages: 18
Abstract: Multiway Decision Graphs (MDGs) are a canonical representation of a subset of many-sorted first-order logic. It generalizes classical Binary Decision Diagrams (BDD's) with abstract data and uninterpreted functions. The original specification language of the MDG tool is called $\mathcal{L}_{MDG}$ that provides temporal operators and abstract data types to formalize properties. Meanwhile, the Property Specification Language (PSL) has a rich temporal operators but without abstract data types. In this paper, we propose a new specification language called Abstract Property Language (APL) suitable for the MDG model checking. This language replaces the $\mathcal{L}_{MDG}$ language of the MDG tool and introduces new operators borrowed from PSL to improve expressiveness. We provide the formal definition of this language in terms of BNF grammar format and formal semantics. APL is associated with a front-end translator that accepts APL specifications and builds veri!
fication-ready models to be handled by the MDG verification tool. Finally, experimental results are presented to show the performance of the APL-Tool and the analysis of the generated code executed on several test benches including Look-Aside Interface design.
Keywords: Abstract Property Language, MDGs, Property Specification Language, Generating Verification-Ready MDG Model
EXTENSION of the file: .pdf
Special (Invited) Session:
Organizer of the Session:
How Did you learn about congress:
IP ADDRESS: 86.108.38.36
