Lightweight specification and analysis of dynamic systems with rich configurations
Abstract
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.
BibTeX
@inproceedings{Macedo-al:FSE16,
author = {Nuno Macedo and
Julien Brunel and
David Chemouil and
Alcino Cunha and
Denis Kuperberg},
title = {Lightweight specification and analysis of dynamic systems with rich configurations},
booktitle = {FSE},
pages = {373--383},
publisher = {{ACM}},
year = {2016},
}