文章基本信息

标题：Using Graph Transformation Systems to Specify and Verify Data Abstractions
本地全文：下载
作者：Luciano Baresi ; Carlo Ghezzi ; Andrea Mocci 等
期刊名称：Electronic Communications of the EASST
电子版ISSN：1863-2122
出版年度：2008
卷号：10
语种：English
出版社：European Association of Software Science and Technology (EASST)
摘要：This paper proposes an approach for the specification of the behavior of software components that implement data abstractions. By generalizing the approach of behavior models using graph transformation, we provide a concise specification for data abstractions that describes the relationship between the internal state, represented in a canonical form, and the observers of the component. Graph transformation also supports the generation of behavior models that are amenable to verification. To this end, we provide a translation approach into an LTL model on which we can express useful properties that can be model-checked with a SAT solver.