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.
Type de document :
Communication dans un congrès
Abstract State Machines, Alloy, B and Z, Feb 2010, Orford, Canada. Springer Berlin / Heidelberg, Volume 5977/2010, pp.408, 2010, Lecture Notes in Computer Science. 〈http://www.springerlink.com/content/fj731508j1pt7774/?p=ab2b8df598a145e8b69500e9e385c41c&pi=13〉. 〈10.1007/978-3-642-11811-1_41〉
Liste complète des métadonnées

https://hal.inria.fr/inria-00471320
Contributeur : Nicolas Stouls <>
Soumis le : jeudi 8 avril 2010 - 08:45:13
Dernière modification le : mercredi 11 avril 2018 - 01:54:08

Identifiants

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. Springer Berlin / Heidelberg, Volume 5977/2010, pp.408, 2010, Lecture Notes in Computer Science. 〈http://www.springerlink.com/content/fj731508j1pt7774/?p=ab2b8df598a145e8b69500e9e385c41c&pi=13〉. 〈10.1007/978-3-642-11811-1_41〉. 〈inria-00471320〉

Partager

Métriques

Consultations de la notice

144