Scenario- Based Property Description and Model Slicing for Real Systems

A. ALFONSO; V. BRABERMAN; D. GARBERVETSKY; N. KICILLOF; A. OLIVER

Linz, Australia

Conferencia; ACM International Conference on Automata Software Engineering; 2004

ACM Sigplan

Two key obstacles to the adoption of automatic exploration and checking of behavioral models by the software development industry are the expertise required for formally describing requirements and the computational cost caused by state space explosion phenomena that arise in the analysis of distributed and concurrent systems. We present here a novel technique that consists in combining a visual language to depict event-based requirements, with state space reduction methods that slice models in terms of virtual observers. We provide proof-of-concept case studies and empirical evidence that this integration can significantly ease the description of complex properties such as freshness, bounded response and event correlation, and their verification on models of real-time systems.