Abstract
This paper compares six model checkers (Alloy, cadp, fdr2, NuSMV, ProB, Spin) for the validation of information system specifications. The same case study (a library system) is specified using each model checker. Fifteen properties of various types are checked using temporal logics (CTL and LTL), first-order logic and failure-divergence (fdr2). Three characteristics are evaluated: ease of specifying information system i) behavior, ii) properties, and iii) the number of IS entity instances that can be checked. The paper then identifies the most suitable features required to validate information systems using a model checker. © 2010 Springer-Verlag Berlin Heidelberg.
Cite
CITATION STYLE
Frappier, M., Fraikin, B., Chossart, R., Chane-Yack-Fa, R., & Ouenzar, M. (2010). Comparison of model checking tools for information systems. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 6447 LNCS, pp. 581–596). https://doi.org/10.1007/978-3-642-16901-4_38
Register to see more suggestions
Mendeley helps you to discover research relevant for your work.
