Skip to Main content Skip to Navigation
Conference papers

B Model Abstraction Combining Syntactic and Semantic Methods

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 illustrates 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 (SLTS). The syntactic transformation suppresses some variables in M. This function is correct in the sense that A is rened by M. A process that combines the syntactic and semantic abstractions has been experimented. It significantly reduces the time cost of semantic abstraction computation. This abstraction process allows for verifying safety properties by model-checking or for generating abstract tests. These tests are generated by a coverage criteria such as all states or all transitions of an SLTS.
Complete list of metadata

https://hal.inria.fr/inria-00471320
Contributor : Nicolas Stouls Connect in order to contact the contributor
Submitted on : Thursday, April 8, 2010 - 8:45:13 AM
Last modification on : Friday, February 4, 2022 - 3:10:11 AM

Links full text

Identifiers

Citation

Jacques Julliand, Nicolas Stouls, Pierre-Christophe Bué, Pierre-Alain Masson. B Model Abstraction Combining Syntactic and Semantic Methods. Abstract State Machines, Alloy, B and Z, Feb 2010, Orford, Canada. pp.408, ⟨10.1007/978-3-642-11811-1_41⟩. ⟨inria-00471320⟩

Share

Metrics

Record views

109