@techreport{jsbm09:ir,
author = {Julliand, Jacques and Stouls, Nicolas and Bu\'e, Pierre-Christophe and Masson, Pierre-Alain},
institution = {LIFC, INSA-Lyon},
title = {{B} Model Abstraction Combining Syntactic and Semantics Methods},
note = {15 pages},
number = {RR2009-04},
type = {Research Report},
month = nov,
year = 2009,
PDF = {http://perso.citi.insa-lyon.fr/nstouls/Productions/2010_ABZ/Article-ABZ10.pdf},
abstract = {
In a model-based testing approach as well as for the verification of properties by model-checking, B models
provide an interesting solution. But for industrial applications, the size of their state space often makes
them hard to handle. To reduce the amount of states, an abstraction function can be used, often combining
state variable elimination and domain abstractions of the remaining variables. This paper presents a computer
aided abstraction process that combines syntactic and semantic abstraction functions. The first function
syntactically transforms a B event system M into an abstract one A, and the second one transforms a B event
system into a Symbolic Labelled Transition System. This paper is devoted to define a syntactic transformation
that suppresses some variables in M. We show that this function is correct, by proving that A is refined by M,
and that a process that combines the syntactic and semantic abstractions significantly reduces the number of
proof obligations to prove, and the time cost of abstraction computation.
}
}