Verifying Properties of Scenarios with Fixed Points

During the requirements elicitation phase a software engineer tries to determine what the customer really wants (and needs.) This task requires, on the one hand, strong communication skills and, on the other hand, a good engineering background to construct a coherent set of requirements. There is a thus a conflict informal and formal techniques. Scenarios are a powerful communication tool and may be given a formal semantics so that they may be amenable to formal verification. We present a method to verifying properties of scenarios based on fixed points of predicate transformers. This work is adapted from an approach that had been originally proposed by Sifakis for transition systems. Scenarios are modelled in a similar way to Diijkstras guarded commands.