Cheung, T.-Y.,Huang, Xing.2009-03-232009-03-2319921992Source: Masters Abstracts International, Volume: 32-05, page: 1415.9780315857865http://hdl.handle.net/10393/7760http://dx.doi.org/10.20381/ruor-6954This 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.93 p.Computer Science.Thesis