FSM-based properties and abstraction of components

Generating a good abstraction is not an easy task in a model-checking process. A bad abstraction will not only fail the verification but may also lead to numerous unsuccessful refinements due to weak counterexamples. Therefore, the abstraction has to be wisely built in order to attain the verification objective. A property satisfied by a component is a natural abstraction of it. However, the lack of pertinent properties in the selection pool is a hurdle to exploit them for abstraction generation. Considering a system made of synchronous components on which a global property has to be verified, we present a method to generate properties which are directly derived from the component?s FSM. Then we propose to build abstractions by selecting among these properties, those describing variable activation flow related to the global property to be verified. Several experimentations conducted on a realistic CAN bus platform illustrate its applicability and potential benefits.