Towards automated software model checking using graph transformation systems and Bogor |
| |
| Authors: | Vahid Rafe Adel T Rahmani |
| |
| Institution: | (1) Department of Computer Engineering, Iran University of Science and Technology, Tehran, Iran |
| |
| Abstract: | Graph transformation systems have become a general formal modeling language to describe many models in software development
process. Behavioral modeling of dynamic systems and model-to-model transformations are only a few examples in which graphs
have been used to software development. But even the perfect graph transformation system must be equipped with automated analysis
capabilities to let users understand whether such a formal specification fulfills their requirements. In this paper, we present
a new solution to verify graph transformation systems using the Bogor model checker. The attributed graph grammars (AGG)-like
graph transformation systems are translated to Bandera intermediate representation (BIR), the input language of Bogor, and
Bogor verifies the model against some interesting properties defined by combining linear temporal logic (LTL) and special-purpose
graph rules. Experimental results are encouraging, showing that in most cases our solution improves existing approaches in
terms of both performance and expressiveness.
|
| |
| Keywords: | Graph transformation Verification Bogor Attributed graph grammars (AGG) Software model checking |
| 本文献已被 维普 万方数据 SpringerLink 等数据库收录！ |
