Formal method for automated testing data flow aspects of communications protocols, software, and systems specified in Lotos

摘要

In this paper, we discuss the testing of data flow aspects of communications protocols and distributed systems specified in Lotos; the ISO Formal Description Technique (FDT). We also develop a method for automated derivation of sequences to conformance test data flow aspects of a system specified in Lotos. This has applications for communications protocols, software, and distributed real time systems in general. We generalize the testing method, with best known coverage, developed for Extended Finite State Machines (EFSMs) to the algebraic FDT Lotos. The method firstly constructs a "Data-Oriented Restricted Behavior" Tree that represents the behavior of the given specification. An algorithm for the automated construction of T is developed in this paper. Then, the testing sequences are driven.