Temporal Logic for Scenario-Based Specifications

We provide semantics for the powerful scenario-based language of live sequence charts (LSCs). We show how the semantics of live sequence charts can be captured using temporal logic. This is done by studying various subsets of the LSC language and providing an explicit translation into temporal logic. We show how a kernel subset of the LSC language (which omits variables, for example) can be embedded within the temporal logic CTL. For this kernel subset the embedding is a strict inclusion. We show that existential charts can be expressed using the branching temporal logic CTL while universal charts are in the intersection of linear temporal logic and branching temporal logic LTL and CTL. Since our translations are efficient, the work described here may be used in the development of tools for analyzing and executing scenario-based requirements and for verifying systems against such requirements.

tacas05.pdf
PDF file

Publisher  Springer Verlag

Details

TypeInproceedings
URLhttp://dx.doi.org/10.1007/978-3-540-31980-1_29
Pages445-460
Volume3440
SeriesLNCS
> Publications > Temporal Logic for Scenario-Based Specifications