Synthesising Non-Anomalous Event-Based Controllers for Liveness Goals

DIPPOLITO R. NICOLAS; BRABERMAN VICTOR; PITERMAN NIR; UCHITEL SEBASTIAN

ACM TRANSACTIONS ON SOFTWARE ENGINEERING AND METHODOLOGY

ASSOC COMPUTING MACHINERY

Año: 2013 vol. 22 p. 1 - 36

1049-331X

We present SGR(1), a novel synthesis technique and methodological guidelines for automatically constructing event-based behaviour 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 modelled carefully in order to avoid synthesising anomalous behaviour models. We characterise non-anomalous models and propose assumption compatibility, a sufficient condition, as a methodological guideline.