Towards the validation of distributed systems based on data flow analysis.

Abstract

This thesis proposes a new approach for the detection of data flow anomalies and generation of selective test sequences for distributed systems specified in LOTOS. It includes a Data Petri-Net (DPN) model for system specification. The model is an ordinary Petri-net extended with the capabilities of handling abstract data types, unusual actions and data synchronization. Based on the DPN, parameter (variable/constant) occurrences are classified as definition, undefinition and use. A method called DETANOM is then developed for detecting data flow anomalies, such as undef-use, def-def and def-undef anomalies. To facilitate the selection of test sequences, three families of data-flow-oriented coverage criteria are proposed, which include all-defs covers, all-uses covers and all-du-paths covers. Test sequences selected according to these criteria aim at checking whether an implementation under test possesses the desired associations among the values of the input and output parameters. A method called GENTEST is also developed for generating selective test sequences according to these criteria. Finally, these DPN-based methods are applied to the validation of LOTOS specifications. Details of an application to the Alternating Bit Protocol are included.