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. © 2009 Springer-Verlag Berlin Heidelberg.
CITATION STYLE
Damasceno, A., Farias, A., & Mota, A. (2009). A mechanized strategy for safe abstraction of CSP specifications. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 5902 LNCS, pp. 118–133). https://doi.org/10.1007/978-3-642-10452-7_9
Mendeley helps you to discover research relevant for your work.