Towards the validation of distributed systems based on data flow analysis.
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...
| Main Author: | |
|---|---|
| Other Authors: | |
| Format: | Others |
| Published: |
University of Ottawa (Canada)
2009
|
| Subjects: | |
| Online Access: | http://hdl.handle.net/10393/7760 http://dx.doi.org/10.20381/ruor-6954 |
| Summary: | 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. |
|---|