In: J. Esparza, C. Lakos (Eds.): Lecture Notes in Computer Science, Vol. 2360: 23rd International Conference on Applications and Theory of Petri Nets, Adelaide, Australia, June 24-30, 2002, pages 217-236. Springer Verlag, June 2002.
Abstract: Scenarios are now widely used when developing distributed systems. In this paper, we provide a semantical foundation for scenarios, which reflects the informal and non-operational use of scenarios. We call this semantics situations. We show that system properties can be specified by implications between situations, and we provide some proof techniques for verifying that a system meets such specifications. The basic proof arguments are automata, which are abstractions of the considered system or some of its causal relations.