Erschienen:
Association for Computing Machinery (ACM), 2013
Erschienen in:
ACM Transactions on Software Engineering and Methodology, 22 (2013) 1, Seite 1-36
Sprache:
Englisch
DOI:
10.1145/2430536.2430543
ISSN:
1049-331X;
1557-7392
Entstehung:
Anmerkungen:
Beschreibung:
We present SGR(1), a novel synthesis technique and methodological guidelines for automatically constructing event-based behavior models. Our approach works for an expressive subset of liveness properties, distinguishes between controlled and monitored actions, and differentiates system goals from environment assumptions. We show that assumptions must be modeled carefully in order to avoid synthesizing anomalous behavior models. We characterize nonanomalous models and propose assumption compatibility, a sufficient condition, as a methodological guideline.