Adriana Damasceno,  Adalberto Farias,  Alexandre Mota. 

Infinite models cannot be directly analyzed by model checking. An alternative for achieving that is using data abstraction to derive a simpler (abstract) but finite model so that the properties can be verified using the abstract model instead. This work proposes a strategy and an algorithm for generating abstractions of systems modeled in the process algebra CSP. These abstractions are safe in the sense that they preserve trace-based refinements. We show the application of our strategy to an example.

http://www.springerlink.com/content/x1u0802716085280/

Processando consulta.