Abstractions with Strong Preservation of Concurrent Systems
Mustapha Bourahla · International Journal on Information Technology (IREIT) · 2016
In this paper, we present a method to generate strongly preserving abstractions for model checking concurrent systems. The concurrent system which can be infinite, is first described by a program using a defined syntax and semantics. This program is abstracted using the framework of abstract interpretation where an abstract function will be given. This abstract program is demonstrated to be an accurate approximation of the original program which may contain spurious behaviors. These spurious behaviors will be identified and removed using a new defined abstraction framework based on the restrictions. The new produced abstract program is an exact approximation of the original program.