Engineering formal requirements: analysis and testing.
KNOWLEDGE SYSTEMS INSTITUTE
We introduce a method for formal analysis and symbolic testing of behavioral aspects of Z specifications. We start defining a (chemical) operational semantics, which supports an abstract execution model and some new constructs to allow the verification of dynamic properties. Moreover, using such a semantics, we have built a parallel animator of Z specifications which automatically constructs distributed prototypes directly from a (refined) specification: such a tool makes effectively observable concurrent behaviors of the Z requirements specification.
|Title:||Engineering formal requirements: analysis and testing|
|UCL classification:||UCL > School of BEAMS > Faculty of Engineering Science
UCL > School of BEAMS > Faculty of Engineering Science > Computer Science
Archive Staff Only