Abstract | ||
---|---|---|
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. |
Year | DOI | Venue |
---|---|---|
2009 | 10.1007/978-3-642-10452-7_9 | SBMF |
Keywords | Field | DocType |
process algebra csp,finite model,model checking,abstract model,safe abstraction,mechanized strategy,csp specifications,infinite model,trace-based refinement,process algebra,system modeling | Abstraction model checking,Model checking,Programming language,Abstraction,Computer science,Theoretical computer science,Process calculus | Conference |
Volume | ISSN | Citations |
5902 | 0302-9743 | 5 |
PageRank | References | Authors |
0.47 | 9 | 3 |
Name | Order | Citations | PageRank |
---|---|---|---|
Adriana Damasceno | 1 | 5 | 0.47 |
Adalberto Farias | 2 | 11 | 1.91 |
Alexandre Mota | 3 | 72 | 11.09 |