Lightweight specification and analysis of dynamic systems with rich configurations
Nuno Macedo, Julien Brunel, David Chemouil, Alcino Cunha, Denis Kuperberg · 2016
Model-checking is increasingly popular in the early phases of the software development process. To establish the correctness of a software design one must usually verify both structural and behavioral (or temporal) properties. Unfortunately, most specification languages, and accompanying model-checkers, excel only in analyzing either one or the other kind. This limits their ability to verify dynamic systems with rich configurations: systems whose state space is characterized by rich structural properties, but whose evolution is also expected to satisfy certain temporal properties.