Combining Theorem Proving and Model Checking in the Safety-Critical Software Development through Translating Event-B to SMV
Model checking and theorem proving are two key vertification techniques in the formal method, but each has its advantages and disadvantages. In this paper, we first try to present the general model transformation rules from Event-B to SMV in order to realize complementary advantages, and then design...
| Main Authors: | , , |
|---|---|
| Format: | Article |
| Language: | English |
| Published: |
EDP Sciences
2017-01-01
|
| Series: | MATEC Web of Conferences |
| Online Access: | https://doi.org/10.1051/matecconf/201712804004 |