Open Collections

UBC Theses and Dissertations

UBC Theses Logo

UBC Theses and Dissertations

Trace analysis of protocols based on formal concurrent specifications Kim, Myungchul 1993

Your browser doesn't seem to have a PDF viewer, please download the PDF to view this item.

Item Metadata

Download

Media
831-ubc_1993_spring_phd_kim_myungchul.pdf [ 5.33MB ]
Metadata
JSON: 831-1.0051350.json
JSON-LD: 831-1.0051350-ld.json
RDF/XML (Pretty): 831-1.0051350-rdf.xml
RDF/JSON: 831-1.0051350-rdf.json
Turtle: 831-1.0051350-turtle.txt
N-Triples: 831-1.0051350-rdf-ntriples.txt
Original Record: 831-1.0051350-source.json
Full Text
831-1.0051350-fulltext.txt
Citation
831-1.0051350.ris

Full Text

Trace Analysis of Protocols based on Formal Concurrent Specifications by MYUNGCHUL KIM B.Sc. Ajou University, Korea, 1982 M.Sc. Korea Advanced Institute of Science and Technology, Korea, 1984 A THESIS SUBMITTED IN PARTIAL FULFILLMENT OF THE REQUIREMENTS FOR THE DEGREE OF DOCTOR OF PHILOSOPHY in THE FACULTY OF GRADUATE STUDIES (DEPARTMENT OF COMPUTER SCIENCE) We accept this thesis as conforming to the required standard  THE UNIVERSITY OF BRITISH COLUMBIA December 1992 ©MyungChul Kim, 1992  In presenting this thesis in partial fulfilment of the requirements for an advanced degree at the University of British Columbia, I agree that the Library shall make it freely available for reference and study. I further agree that permission for extensive copying of this thesis for scholarly purposes may be granted by the head of my department or by his or her representatives. It is understood that copying or publication of this thesis for financial gain shall not be allowed without my written permission.  (Signature)  Department of The University of British Columbia Vancouver, Canada  Date  DE-6 (2/88)  )e  c  22  -  /  1j2  Abstract To increase the probability of computers communicating reliably with one another, protocol implementations must be tested for conformance to the standards on which they are based. Test case generation and trace analysis are two important topics in protocol testing research. Most of the work so far has focused on test case generation rather than trace analysis. Furthermore, most of the work has dealt only with the sequential aspects of the protocol specifications. In this thesis, a model that combines the two functions of test case generation and trace analysis in a unified framework is presented. The model, which is based on single module extended finite state machines, handles both control and data flows for single module specifications. Symbolic evaluation is used to detect and delete infeasible paths that may be generated. Practical considerations which may occur in a real test environment, such as out of order message sequences, are also addressed. A prototype implementation of the unified model was completed. The application of this method to X.25 LAPB shows that it can manage frame collision and control and data flows of the protocol rigorously. The model is extended to study the trace analysis of concurrent specifications based on multi-module extended finite state machines. This is done by introducing two additional models - concurrency and traceability. The concurrency model deals with concurrent properties such as concurrent events, concurrency blocks, global states, concurrency measures, deadlocks and dataraces which do not arise in sequential or single module specifications. The concurrency model allows a high-level abstraction to be used for understanding and analyzing concurrent behaviors. We also show how concurrency measures can be computed efficiently based on the concept of concurrency blocks. The traceability concept is needed to obtain the precise order of input/output messages of a module without state space explosion. This model for the trace analysis of concurrent specifications without translating them into their sequential equivalence is formalized and proposed for application to multi-module specification, multi-party testing and interoperability testing. The viability of the proposed methodology which can be applied to any specifications based on extended finite state machines is demonstrated using Estelle specifications in the thesis.  ii  Contents Abstract^  ii  Contents^  iii  List of Tables^  vi  List of Figures^  vii  Terms and Acronyms^  viii  Acknowledgement^  ix  1  Introduction 1.1 Motivation ^ 1.2 Thesis Statements ^ 1.3 Summary of Contributions ^ 1.4 Thesis Organization ^  2  Background 2.1 Conformance Testing ^ 2.2 Estelle ^ 2.3 Concurrency ^  7 7 10 12  3  Trace Analysis based on Formal Specifications 3.1 Related Work ^ 3.2 Experiments on Finite State Machines ^ 3.3 Unified Model for Trace Analysis and Test Case Generation ^ 3.4 Trace Analysis in External Test Architectures ^ 3.5 A Case Study - The X.25 LAPB Protocol ^ 3.6 Test Case Generation and Validation ^ 3.7 Chapter Summary ^  15 16 19 21 28 30 36 39  iii  1 2 4 5 6  4  Implementation of Trace Analyzer 4.1 Brief Description of Tools ^ 4.1.1^Estelle.Y with ASN.1 ^ 4.1.2^Translation from Estelle to Estelle.Y ^ 4.1.3^Protocol Data Structure ^ 4.1.4^TESTGEN Parser ^ 4.2 Implementation Issues ^ 4.2.1^Known Initial State ^ 4.2.2^Unfolding Loops ^ 4.2.3^Transitions with Timers ^ 4.2.4^Preprocessing Phase ^ 4.2.5^Search Method ^ 4.2.6^Pruning Candidate Transitions ^ 4.2.7^Verdict and Location of Errors ^ 4.3 Sample Experiments ^ 4.3.1^Cases 1 and 2 ^ 4.3.2^Case 3 ^ 4.3.3^Case 4 ^ 4.3.4^Performance ^ 4.4 Future Work ^  40 40 41 42 43 43 43 43 44 47 49 50 51 51 53 53 56 57 60 61  5  Concurrency Model 5.1 Formal Concurrency Model ^ 5.1.1^Synchronous and Asynchronous Communications ^ 5.1.2^Concurrency Checking ^ 5.1.3^Global Synchronization Cut ^ 5.1.4^Concurrency Measures ^ 5.2 Application to Estelle Specifications ^ 5.3 Application to LOTOS Specifications ^ 5.4 Application to Ada Programs ^ 5.5 Chapter Summary ^  63 63 64 67 69 85 89 90 90 91  6  Trace Analysis based on Concurrent Specifications 6.1 The Basic Blocks ^ 6.1.1^Trace Analysis based on Single-Module Specifications ^ 6.1.2^Concurrency Model ^ 6.1.3^Traceability ^ 6.2 Formal Model ^ 6.3 Applications ^ 6.3.1^Trace Analysis based on Multi-module Specifications ^ 6.3.2^Message Collisions in Multiple Party and Interoperability Testings 6.4 Case Study ^  iv  93 94 95 96 96 99 101 102 103 105  6.5 Chapter Summary ^  107  7 Conclusions and Future Research ^ 7.1 Summary of Results ^ 7.2 Future Research ^  109 109 111  Bibliography^  112  A Estelle Specification of X.25 LAPB ^  119  B Applying Procedure 1 in Section 3.3 to X.25 LAPB^  131  C Flowchart for Example 2 in Section 3.5 ^  133  D High-level Description of Implementation ^ D.1 Preprocessing Phase ^ D.2 Main Analysis Phase ^  137 137 138  E Ada Program having Data Races^  142  F ASN.1 Specification of X.25 LAPB^  144  G Estelle.Y Specification of X.25 LAPB ^  147  H Estelle Specification of Dinning Philosophers ^  154  List of Tables 4.1 Performance of the trace analysis (time unit: second) ^  vi  61  List of Figures 2.1 2.2  OSI Reference Model. ^ Abstract Test Architecture. ^  3.1 3.2  Sequence of Events in Traces ^ Test Case Generation and Trace Analysis ^  33 37  4.1 4.2 4.3  Overall Structure of Trace Analyzer ^ Corresponding Finite State Machine ^ Data Structure for Nondeterminism . ^  41 50 52  5.1 5.2 5.3 5.4 5.5 5.6  Time-event Sequence Diagrams and Their Corresponding DAGs ^ 65 Examples of Global Synchronization Cuts ^ 70 Examples of Global Synchronization Cuts ^ 76 Examples of Global Synchronization Cuts ^ 78 Examples of Global Synchronization Cuts ^ 82 Types of Deadlocks ^ 89  6.1 6.2 6.3 6.4 6.5  Basic Blocks ^ Points of Observation ^ Trace Analysis based on Concurrent Specifications ^ Application ^ Module Structure ^  95 95 100 103 105  E.1  Time-event Sequence Diagram  143  ^  vii  8 9  Terms and Acronyms ACE^Asynchronous Communication Event ASN.1^Abstract Syntax Notation One ASP^Abstract Service Primitive BGSC^Backward Global Synchronization Cut CCITT^International Telegraph and Telephone Consultative Committee DAG^Directed Acyclic Graph DCE^Data Circuit-terminating Equipment DTE^Data Terminal Equipment EFSM^Extended Finite State Machine ETS^Extended Transition System FDT^Formal Description Technique FSM^Finite State Machine FGSC^Forward Global Synchronization Cut GSC^Global Synchronization Cut ISDN^Integrated Services Digital Network ISO^International Organization for Standardization ISP^Input Service Primitive IUT^Implementation Under Test LAPB^Link Access Procedure B LOTOS^Language of Temporal Ordering Specification LT^Lower Tester NFS^Normal Form Specification OSI^Open Systems Interconnection OSP^Output Service Primitive PCO^Points of Control and Observation PDS^Protocol Data Structure PDU^Protocol Data Unit PO^Points of Observation POT^Port of Observation for Traceability SAP^Service Access Point SCE^Synchronous Communication Event SUT^System Under Test TAP^Test Access Port TTCN^Tree and Tabular Combined Notation UT^Upper Tester X.25^Packet-switching protocol and standard (CCITT and ISO)  viii  Acknowledgement I am deeply indebted to my co-supervisors Dr. Samuel T. Chanson and Dr. Son T. Vuong, for their professional support throughout my graduate studies, their encouragement which helped me in gaining confidence in myself, and their guidance which taught me how to conduct scientific research. Especially regular meetings with Dr. Chanson at every two weeks had helped me to come up with ideas, make the ideas clear and write down the ideas on papers. Without the meetings with Dr. Chanson, this thesis would never have existed. I am also very grateful to the other member in my thesis committee, Dr. Carl Seger, for his insightful comments and suggestions. I appreciate Dr. Paul Amer at the University of Delaware for his serving as the external examiner. Thanks to Dr. Gregor v. Bochmann at the University of Montreal and Dr. Robert L. Probert at the University of Ottawa for their valuable comments and information through a project by the Canadian Institute for Telecommunications Research. Many other people at UBC have been very supportive. Many thanks to the members of Protocol Engineering Group: Antonio Loureiro, Sijian Zhang, Jadranka Alilovic-Curgus, Kaichung Ko, Hendra Dany, Russil Wvong, Holger Janssen, Jinsong Zhu, Charles Mathieson, Dr. Masaaki Mori, and Dr. Sang Ho Lee for their sharing the good time for discussion and information exchange. Thanks to Christopher Healey for carefully reading this thesis and making corrections. Thanks to Peter Phillips for helping installing tools and fixing problems of the tools during my studying. I would never become what I am without the unconditional love, understanding and support from my parents and parents-in-law. Their phone calls from home have always been a constant source of strength and encouragement. Thanks to Mr. and Mrs. David C. Lee for their guiding to be acquainted with lives in Vancouver, Mrs. Eun Soon Kim for her constant encouragement and introducing to Jesus Christ, and Mr. and Mrs. Hee Chang Choi for their emotional support and sending magazines. Above all, special thanks to my beautiful daughter Eunah and my wife Kyung Og. It is beyond the power of words to express my debt to the person closest to my heart, Kyung Og, for her patience, her encouragement, and her endless love. I can not imagine what it would have been like without her. The research of this dissertation was supported by Korea Telecom Overseas Studying Fellowship and in part supported by the Canadian Institute for Telecommunications Research under the NCE program of the Government of Canada.  ix  Chapter 1  Introduction The International Organization for Standardization (ISO) and International Telegraph and Telephone Consultative Committee (CCITT) have been standardizing computer communication protocols within the framework of the Open Systems Interconnection (OSI) reference model [Tanen 881. Any systems implemented according to the same OSI protocol standard should be able to communicate with one another. Unfortunately, the standards documents written in English are often unclear or ambiguous and are subject to different interpretations. As a result, independent implementations of the same protocol may be incompatible. To deal with this situation, ISO and CCITT have defined and are standardizing conformance testing procedures [ISOb]. These are to be carried out on a given protocol implementation to ensure that it conforms to the appropriate protocol standards. The testing procedures are to be performed by any one of a number of recognized test laboratories. After a protocol implementation has passed the tests, it is given a certification of approval. Customers may then use the protocol implementation with at least some confidence of compatibility. The client for whom the laboratory performs the conformance tests may be the vendor of the implementation  1  CHAPTER 1. INTRODUCTION^  2  or a potential customer. In either case, the test laboratory has little or no knowledge of the internal workings of the System Under Test (SUT) which contains the Implementation Under Test (IUT). The conformance testing process treats the IUT as a black box; only its external behavior is observed.  1.1 Motivation Research activities in protocol testing can be roughly divided into test case generation and trace analysis [Bochm 89]. However, as in the case for software testing, most of the work has been on test case generation rather than on trace analysis.  ISO has developed two formal description techniques, Estelle and LOTOS [ISOc, ISOd], for the specification of communication protocols and services of OSI architectures. Estelle and  LOTOS are designed to avoid the ambiguity of standard documents written in English. Just as there are formal description techniques for protocol specification, CCITT and ISO have jointly developed a formal notation called the Tree and Tabular Combined Notation (TTCN)  [ISOb] to describe test suites for OSI conformance testing. A test suite specified in TTCN consists of a collection of tables defining the different aspects of the test cases such as service primitives, Protocol Data Units (PDU's) and their parameters, constraints on parameter values and dynamic behaviors (interactions). The interaction order is defined in terms of a tree where each branch from the root to a leaf represents a possible execution sequence. A TTCN test case contains the trace analysis function by expressing verdicts explicitly. This approach gives rise to issues such as how to generate, validate, and manage test suites. Currently, most of the  CHAPTER 1. INTRODUCTION  test cases in use have been created manually in an informal manner. Recently researchers have been investigating the related goals of generating test suites systematically from formal protocol specifications (e.g., [Ural 87, Sarik 87]), and validating TTCN test cases with respect to a formal protocol specification as a result of inverse translation [Bochm 90]. One approach is to make an oracle function which determines whether the message streams exchanged between two protocol entities conform to the formal protocol specification. Even though the approach is most suitable for trace analysis, it can be used for test case validation [Bochm 90], test case generation [Ural 86, Gorli 90] and reducing test case complexity [Wvong 90]. We believe it is possible to combine the applications into one system using a common framework. So far, few people have taken advantage of the close relationship between test case generation and trace analysis. No one has tried to apply the large body of research results in software test case generation (or, for that matter, in protocol test case generation) to protocol trace analysis. Finally, there has been no attempt to build one system to generate test cases and analyze traces with respect to formal protocol specifications using a unified framework. Even though the constraints on test case generation and trace analysis procedures are different, some of the techniques used in test case generation for software testing (e.g., static data flow analysis and symbolic evaluation) can be used to augment the generality, correctness and diagnostics of trace analysis. Until now, work on test case generation and trace analysis has mostly been performed in  CHAPTER 1. INTRODUCTION^  4  a sequential context even though the specifications are concurrent. In general, formal protocol specification languages such as Estelle and LOTOS allow one to specify multiple modules or multiple processes. Most work on the automatic test case generation and trace analysis with respect to Estelle [Sarik 87, Ural 87, Chun 90, Kim 91] assumes a preprocessing stage to translate the multiple modules into a single module in order to obtain sequential behavior [Sarik 86]. Modules are combined by textual replacement to eliminate internal communications between modules. During this process, we may lose semantics on deadlocks and data races and encounter the state space explosion problem. Furthermore, after the translation, it may be difficult to relate the errors detected in trace analysis with respect to the single module specification to corresponding errors in the implementation. For example, a deadlock may be mistaken as an underspecification with respect to the single module specification derived from a concurrent specification. One of the main problems in analyzing multiple concurrent modules is determining the order of events globally. This could easily lead to state space explosion. We believe some concepts in hardware testing (especially chip testing) such as design for testability [Fujiw 85] would be helpful in avoiding the state space explosion problem.  1.2 Thesis Statements In this thesis, we present a model that combines the functions of test case generation and trace analysis in a unified framework. Our model handles both control and data flows. Symbolic evaluation is used to detect and delete infeasible paths which may be the results of path selection. Practical considerations such as out of order message sequences that may occur in a  CHAPTER 1. INTRODUCTION ^  5  real test environment are also addressed. The application of this method to the trace analysis of X.25 LAPB shows that it can manage frame collision, control and data flows of the protocol rigorously [Kim 91]. A prototype of the trace analyzer based on the unified model was implemented and applied to the X.25 LAPB protocol to demonstrate the feasibility of the model. In order to extend trace analysis to the concurrent environment, models of concurrency and traceability have been developed. The concurrency model [Kim 92a] deals with concurrent properties such as concurrent events, concurrency blocks, global states, concurrency measures, communication deadlocks and data races. The concurrency model allows a high-level abstraction to be used for understanding the concurrent behaviors. We show how to compute concurrency measures efficiently based on the concept of concurrency blocks. The traceability concept is needed to obtain the precise order on input/output messages of a module in order to avoid state space explosion. This can occur when applying single module trace analysis to modules with multiple ports. This model for the trace analysis of concurrent specifications is formalized and proposed for application to concurrent specifications, multi-party testing and interoperability testing.  1.3 Summary of Contributions The major contributions of this thesis are fourfold:  1. A unified model for test case generation and trace analysis based on the extended finite state machine has been developed.  CHAPTER 1. INTRODUCTION^  6  2. A prototype implementation of the trace analyzer in the unified model and the application of the prototype to X.25 LAPB have been completed to demonstrate the feasibility of the model. 3. A concurrency model has been developed which gives elegant definitions and computations of concurrent events, concurrency blocks, global states, concurrency measures, deadlocks and dataraces. 4. A methodology for trace analysis with respect to concurrent specifications has been developed based on the trace analysis model in 1, the concurrency model in 3 and the concept of traceability to eliminate state space explosion.  1.4 Thesis Organization The remainder of the thesis is organized as follows. Chapter 2 provides background information on the notions of conformance testing, formal description techniques for protocols, and concurrency. Chapter 3 presents a unified framework for test case generation and trace analysis based on the extended finite state machine. A prototype implementation of the trace analyzer based on the unified model in Chapter 3 is described in Chapter 4. A concurrency model is presented in Chapter 5 which gives elegant and efficient definitions with respect to concurrent specifications. Chapter 6 discusses trace analysis with respect to concurrent specifications. Finally, Chapter 7 concludes the thesis and outlines some future work.  Chapter 2  Background In this chapter, the basic concepts of conformance testing and the Estelle formal description technique are briefly presented as background materials. Further details can be found in [ISOb, Rayne 87, Linn 90, Bosik 91] for conformance testing and [ISOc, Dembi 89] for the Estelle formal description technique. Some basic notions of concurrency are also given.  2.1 Conformance Testing The testing process can be divided into diagnostic testing and conformance testing. Diagnostic testing is carried out by the implementor and is aimed at determining whether the implementation is working correctly according to the implementor's intention. This is based on the protocol standards and the implementation design documents. On the other hand, the main objective of conformance testing is to determine if an implementation conforms to the protocol standards in order to enhance interoperability. The diagnostic testing process treats the Implementation Under Test (IUT) as a white box; its internal and external behaviors are observed, but the conformance testing process treats the IUT as a black box; only its external behavior  7  CHAPTER 2. BACKGROUND^  8  is observed. The seven-layer OSI reference model has been defined by ISO to describe the interconnection of heterogeneous systems [Tanen 88]. Each layer entity in this model, say the (N)-Entity, provides certain services, called (N)-Services, to its upper entity, the (N+1)-Entity as shown in Figure 2.1. (N+1)Entity  (N+1)Entity r  A (N)-ASPs V (N)Entity  A  N)-ASPs (N)-PDUs  ^  (N-1)-ASPs  (N)Entity  (N-1)-ASPs  A  (N-1)-Service Provider  (N)-Service Provider  Figure 2.1: OSI Reference Model. In order to provide these services, an (N)-Entity uses the services provided by its lower entity, the (N-1) Entity. An (N)-Entity together with the services that it provides is called an (N)Service Provider. The abstraction of each entity and services allows flexible implementations since the implementation details are isolated. Two peer (N)-Entities use (N)-Protocol Data Units (PDUs) to communicate with each other through an (N-1)-Service provider. A protocol is the set of rules and conversions that define the communication between the two peer entities. An (N)-Entity communicates with its upper and lower entities by means of (N)- and (N-  CHAPTER 2. BACKGROUND ^  9  1)- Abstract Service Primitives (ASPs), respectively. The points where an implementation can be controlled and observed are called the Points of Control and Observation (PCO). The implementation is not accessible otherwise. During conformance testing, the ASPs and PDUs that are defined as inputs are sent to the (N)-Entity implementation and the ASPs and PDUs generated by the implementation are observed and compared to the permissable outputs. This approach to conformance testing, which considers only the externally visible behavior of the (N)-Entity implementation, is called black box testing. Conformance testing is conducted in a set-up which, in general, consists of several major components. An abstract test architecture (see Figure 2.2) defines the functionalities of these components without giving any implementation details.  Upper Tester  Test Management PDUs Lower  (N+1)-Entity (N)-ASPs  Tester  (N)-PDUs  (N-1)-ASPs  >  (N) Entity  A  JUT (N-1)-ASPs  (N-1)-Service Provider  Figure 2.2: Abstract Test Architecture.  The Lower Tester (LT) is responsible for the control and observation at the PCO below the IUT at the remote end. The lower tester is the peer entity of the IUT. The Upper Tester (UT) controls and observes the (N)-ASPs at the upper service boundary of the IUT. The  CHAPTER 2. BACKGROUND^  10  test events (i.e., atomic interactions between the IUT and an upper or lower tester) used in conformance testing are described in an abstract conformance test suite. The tests in a test suite are organized in a hierarchical structure. The key level, called the test case, is based on a narrowly defined test purpose. The test purpose describes the objective of the test. There are three major components in an abstract test case: test preamble, test body, and test postamble. The preamble defines the necessary steps to bring the IUT into the desired starting state. The test body defines the test steps that are needed to achieve the test purpose. The PDU exchanges needed to verify the new state of the IUT are also part of the test body. The test postamble is used to put the IUT into a stable state after the test body is run. Also it is used to check the destination state of the test case. An abstract test notation, called the Tree and Tabular Combined Notation (TTCN) [ISOb], is defined to represent the abstract test suites in a standard fashion.  2.2 Estelle Estelle is a formal description technique (FDT) for specifying distributed concurrent systems, in particular communication protocols and services. It is based on an extended state transition model, specifically, a model of a nondeterministic automaton extended with elements of the  Pascal language. A distributed system in Estelle is composed of several communicating components called modules. A module is specified by a module definition which may include definitions of other modules. When applied repeatedly, this leads to a hierarchical tree structure of module defini-  CHAPTER 2. BACKGROUND^  11  tions. There are attributing principles that play an important role in defining the behavior of a multiple module system. In Estelle, particular care is taken to specify the communication interface of a module. Such an interface is defined using three concepts: interaction points, channels and interactions (or exchanged messages). Each module has a number of input/output access points called interaction points. A channel which defines two sets of interactions is associated with each interaction point. These two sets consist of interactions which can be sent or received through this interaction point. There are two communication mechanisms in Estelle: message exchange and restricted sharing of variables. First, a module instance can always send an interaction. This principle is called asynchronous communication. An interaction received by a module at its interaction point is appended to an unbounded FIFO queue associated with the interaction point. Second, certain variables can be shared between a module and its parent module. These variables have to be declared as exported variables by the module. This is the only way variables may be shared. Simultaneous access to these variables by the module and its parent is excluded because the execution of the parent's actions always has priority. The internal dynamic behavior of an Estelle specification is characterized in terms of a nondeterministic state transition system. The execution of a transition by a module is considered to be an atomic operation. A state in Estelle is, in general, a complex structure composed of many components such as value of the control state, values of variables and contents of FIFO queues associated with the interaction points.  CHAPTER 2. BACKGROUND^  12  2.3 Concurrency Concurrent behaviors in distributed systems are difficult to specify and analyze. The ISO has developed two formal description techniques, Estelle and LOTOS [ISOc, ISOd], for the specification of communication protocols and services of OSI architectures. In particular, concurrent behaviors can be specified using these techniques. The control part of LOTOS is similar to Calculus of Communicating System [Milne 80] whereas the data part is similar to that of ACT ONE[Ehrig 85]. The LOTOS specification consists of nested processes. The processes may share gates through which communication occurs. The interprocess communication is a two-way rendez-vous mechanism called interaction. Processes can participate in an interaction only if they are simultaneously ready for an interaction. This occurs when they specify the same gate and compatible sorts. A process that offers to receive will wait for a matching send to occur. Similarly, a process that offers to send must wait until the matching receive is executed. Unlike Estelle, there is no other communication mechanism in LOTOS. Since Lamport's pioneering work [Lampo 78], there has been considerable research on concurrency, logical clocks and global states in distributed systems. Charron-Bost[Charro 89] proposed concurrency measures based on a logical clock[Matte 89, Fidge 91]. The logical clock is used to determine whether or not two events are concurrent. A concurrency relation is then used to compute global states and concurrency measures. The concurrency measure is defined as the ratio of the possible number of concurrent events in the system over the number of  CHAPTER 2. BACKGROUND ^  13  concurrent events in a similar system where all the tasks are totally concurrent (i.e. no tasks have communication events) [Charro 89]. This scheme can be extended to detect data races. A data race occurs when two or more concurrent events, at least one of which is a write, access the same shared variable. In this case, the value of the variable is not predictable since it is dependent on the order of execution. With the emergence of concurrent languages such as Ada, Modula II and Occam, there has been growing interest in concurrent program debugging. Debugging concurrent programs is harder than debugging sequential programs because of probe effects and nonreproducibility [Mcdow 89]. These two properties are closely related to nondeterminism. Generally speaking, debugging work on Ada and languages dealing with parallelism at the process level [Helmb 85, Young 88] have concentrated on message passing communication. Debugging work related with lower level parallel programs such as Parallel Fortran, which deal with parallel operations or instructions [Choi 91, Mille 88], have focused on shared memory accesses. The former aims to determine whether the number, order, and semantics of communication statements are proper. The latter tries to detect data race conditions in the interactions of communicating tasks through shared memory. The classes of communication deadlocks that can occur depend on the communication paradigms supported by the programming system. The classification of deadlocks is important in measuring the coverage of deadlock detection algorithms. For example, Cheng showed that a number of proposed techniques [Helmb 85, Young 88] could not detect the complete class of synchronous communication deadlocks in Ada [Cheng 90]. Cheng's classification is based on  CHAPTER 2. BACKGROUND^  14  five different types of waiting relations among tasks in Ada [Ada 83]. It is interesting to compare debugging of concurrent programa[Mcdow 89] with trace analysis based on concurrent specifications. The former works on white box representation of the implementation to detect and locate errors and the latter works on a black box or grey box representation of an implementation for ensuring conformance of external behaviors (traces) to specifications. Other related work includes static concurrency analysis of a path selection mechanism for symbolic execution as a pruning mechanism for concurrency analysis[Young 88]. Also, Weiss provided a formal foundation for a theory of concurrent program testing by representing a concurrent program as a set of sequential programs [Weiss 88].  Chapter 3  Trace Analysis based on Formal Specifications In this chapter, we describe the design of a unified model for test case generation and trace analysis. The unified model can be applied to any formal description techniques (FDTs) based on extended finite state machines (EFSMs). The trace analysis of the unified model is performed using a two phase scheme: a path selection phase based on the control flow (with or without data flow) of the EFSM followed by an infeasible path detection and deletion phase using symbolic evaluation. This scheme can be extended to realize test case generation. The design objectives are listed below:  • Generality: the analysis is based on the EFSM model. Thus, the technique will work with any protocol specifications that can be mapped into an EFSM (see for example [Karjo 90] in LOTOS). • Extendability: the trace analyzer can be easily extended to perform test case generation functions using common functionalities and the same system view.  15  CHAPTER 3. TRACE ANALYSIS BASED ON FORMAL SPECIFICATIONS ^16  • Correctness: infeasible paths are detected and eliminated by detecting inconsistencies in the path conditions using symbolic evaluation. • Error Identification: the analyzer should help to identify the cause of errors when they  occur. • Practicality: the system should be able to handle real life protocols and testing environments.  This chapter focuses primarily on trace analysis. First, related work is given in Section 3.1. Section 3.2 outlines some basic theories in finite state machines relevant to trace analysis. In Section 3.3, our model based on extended finite state machines is presented. The relationship between extended finite state machines and finite state machines is given. The model is extended to different test architectures in Section 3.4, and illustrated using X.25 LAPB as a case study in Section 3.5. We discuss the relationship between trace analysis and test case generation in Section 3.6 and outline how the model can be used to generate and validate test cases. Finally Section 3.7 summarizes the work.  3.1 Related Work Ural presented the concepts of protocol trace analysis [Ural 86]. The work was designed to validate a protocol implementation, SFR_K (System Functionality Representative_K), according to the protocol specification SFR_K - I. The SFR_K - 1 is assumed to be acceptable as a reference for consistency checking. In trace checking, SFR_K - 1 is employed as a test oracle  CHAPTER 3. TRACE ANALYSIS BASED ON FORMAL SPECIFICATIONS^17  which determines whether or not an observed trace of SFR_K is permissible. In trajectory  checking, all allowed responses to a stimulus are included in a tree-structured trajectory. The paper [Ural 86] proposes that a Prolog procedure implementing an abstract SFR_K based on  Estelle can be used as a generator to produce interaction sequences and as a validator to check observed interaction sequences. This requires Estelle specifications to be translated into SFRs in Prolog and the SFRs to be capable of reverse execution. However, not all Prolog programs are reversible because of the arithmetic evaluation and depth first search rules of Prolog. In order to execute Prolog programs in reverse, the programs have to be structured properly, for example, by checking loops whenever transitions are visited. Furthermore, the automatic translation of Estelle specifications into Prolog is quite complicated. In the paper by Bochmann [Bochm 90], a test trace analyzer called TETRA was constructed by modifying a LOTOS interpreter. TETRA takes interaction parameters into account and uses backtracking to determine whether the tree of possible execution histories defined by the specification includes the observed trace of interactions. For nondeterministic choices which are not directly visible, backtracking is necessary until either a correct path is located or no possible match exists. In order to avoid backtracking over all possible paths, the system instantiates interaction parameters as late as possible. It waits until their values can be determined from the constraints of the specification and/or subsequent observed input or output values. Nonetheless, certain features of LOTOS such as non well-guarded expressions and general CHOICE statements can easily explode the number of paths that have to be processed. Also, currently  TETRA cannot be used for test case generation and there are limitations when the behavioral  CHAPTER 3. TRACE ANALYSIS BASED ON FORMAL SPECIFICATIONS ^18  tree of the protocol is too complex. Mockingbird [Gorli 90], on the other hand, can be used as both a generator - producing test cases whose properties conform to the specification, and an acceptor - validating test cases against the specification. The specification language is a combination of context-free grammars and constraint systems. The semantics of the specification are based on constraint logic programming (CLP). However, not all CLPs are reversible because of the possible infinite recursions generated by the unfair method of rule selection in CLP. The model is not suitable for real-life protocols. In [Wvong 90] a trace analyzer is used to simplify test cases. Test cases only need to describe the expected behaviors of the protocol implementation. The unexpected behaviors are checked by the analyzer. The technique was applied to an implementation of X.25 LAPB. There has been much work on static data flow analysis [Oster 81, Podgu 90] and symbolic evaluation [King 76, Clark 85] in software engineering. Static data flow techniques require the selection of subpaths based on particular sequences of definitions and references to the variables in the program without execution. These techniques are used to detect suspicious or erroneous use of data, such as referencing undefined variables and defining variables without subsequent usage. Symbolic evaluation is a program technique that derives algebraic representations, over the input values, of the computations and their applicable domains. Thus symbolic evaluation describes the relationship between the input data and the resulting values, whereas normal execution computes numeric values but loses information about the way in which they were derived. Static data flow analysis methods can be used to detect paths containing suspect  CHAPTER 3. TRACE ANALYSIS BASED ON FORMAL SPECIFICATIONS^19  sequences of events but cannot determine if these paths are executable. Symbolic evaluation can be used to determine which paths are unexecutable by computing the consistency of path conditions and thus can greatly simplify the complexity of trace analysis.  3.2 Experiments on Finite State Machines Our approach uses some principles of the finite state machine (FSM) model. The reader is assumed to have a basic knowledge of FSMs. In this section, only the principles and theories relevant to trace analysis are outlined. An FSM (e.g., Mealy machine) is an abstract model consisting of a finite number of states, a finite number of input symbols, and a finite number of output symbols. Every possible combination of input symbol, output symbol, present state and next state of an FSM is described by either a transition table or a transition diagram. An experiment performed on a finite state machine consists of applying one or more input sequences, observing the corresponding output sequences, and drawing a conclusion about the internal behavior of the machine. A machine is assumed to be finite, deterministic, reduced, strongly connected, and completely specified, and is available to the experimenter as a black box. This means the experimenter has access to its input and output terminals, but cannot inspect the internal structures. The experimenter may have to consider a class of problems, known as measurement and  control problems, to conduct experiments on a machine for which the transition table is supplied. The control problem is concerned with finding input sequences that take a given machine from a known initial state to a predesignated terminal state. The measurement problem is the  CHAPTER 3. TRACE ANALYSIS BASED ON FORMAL SPECIFICATIONS ^20  identification of the unknown initial state of the machine. The general machine control problem that brings the machine to a specified final state from an unknown initial state can be viewed as being composed of two distinct subproblems: a measurement problem followed by a simple control problem. Experiments are classified into synchronizing experiments, homing experiments, and distinguishing experiments according to their purpose [Gill 62, Henni 68]. A synchronizing experiment  consists of the application of a fixed input sequence (or synchronizing sequence) that is guaranteed to leave the machine in a particular final state. A homing experiment consists of the application of either a preset or an adaptively chosen input sequence such that the resulting output sequence uniquely specifies the machine's final state. A distinguishing experiment is similar to a homing experiment except that it is used to determine a machine's initial state. The homing experiment is solvable but not all distinguishing experiments are solvable [Gill 62, Henni 68]. Finally synchronizing experiments are dependent on the existence of synchronizing sequences of machines. Typically, solutions to the measurement and control problem make use of the information contained in the machine's transition table in conjunction with the machine's response tree [Gill 62, Henni 68]. A response tree is generated from the transition table, and is basically a graphical presentation of the results obtained when different input sequences are applied to the machine. The different paths through this tree correspond to the possible input sequences that might be used in an experiment. The nodes of this tree correspond to the possible states that the machine can be in after the application of the input sequences that lead to those nodes.  CHAPTER 3. TRACE ANALYSIS BASED ON FORMAL SPECIFICATIONS^21  The level of a node corresponds to the length of the input sequence required to reach the node. A path through a response tree terminates whenever certain termination rules are satisfied. The response tree approach is, in effect, an exhaustive tree search process. Theorems 1 and 2 below give an upper bound on the lengths of the simple preset homing experiments [Das 79]. Theorem 1 The homing problem for a v-state sequential machine M with m admissible states  can always be solved by a simple preset experiment of length Lh s where Lh s < (v —1)(In — 1). The admissible states of machine M refer to the initial states of the machine. A simple  experiment is one which is performed on a single copy of the machine, and an experiment is preset if all the input sequences are predetermined independent of the outcome of the experiment. The homing problem becomes trivial when m = 1. Theorem 2 Let M be a sequential machine in which every pair of states is k —distinguishable.  The homing problem for M with m admissible states can always be solved by a simple preset experiment of length Lh s where Lh s < k(m-1). Two states are k — distinguishable if and only if there exists an input sequence of length k that yields one output sequence when the machine is started in one state, and a different output sequence when the machine is started in the other state.  3.3 Unified Model for Trace Analysis and Test Case Generation Our model is based on extended finite state machines (EFSM). The extended finite state machine is an abstract model which associates a program segment with each transition instead of simply  CHAPTER 3. TRACE ANALYSIS BASED ON FORMAL SPECIFICATIONS^22  defining an input/output message pair as in the case of the FSM. Thus, there can be predicates, variables, and a sequence of actions associated with each transition. A specification written in  Estelle or SDL is an EFSM, and trace analysis can be viewed as experiments on the EFSM. First, we note the differences between test case generation and trace analysis with respect to path analysis methods for control and data flows: 1. In test case generation, the initial and final states of each path are supposed to be known. This is not the case for trace analysis, so we need to determine the initial and final states from the observed input and output message sequences. Even for FSMs which deal with control flow only, determining the initial state is not always possible (see Section 3.2). This condition is even more complicated for EFSMs which deal with both control and data flows. 2. In test case generation, every possible path of a formal specification has to be considered. Trace analysis, on the other hand, need only consider a finite number of paths that comply with the observed sequence of input and output messages. Actually, generating all test cases can be done efficiently. The problem is in the identification of any infeasible paths from the set of paths produced. For example, data flow techniques that attempt to generate only feasible paths by excluding inconsistent branch predicates have been shown to be NP-complete [Gabow 76]. However, the techniques for the restricted class of program flow graphs which are trees are not NP-complete [Gabow 76]. This suggests, therefore, that trace analysis can be done faster than test case generation in general.  CHAPTER 3. TRACE ANALYSIS BASED ON FORMAL SPECIFICATIONS ^23  3. As a consequence of point 2 above, the paths which have to be considered in trace anal-  ysis are finite in number and are a subset of those for test case generation. The trace contains information to determine the actual number of loop iterations, specific values of parameters, and the outcome of conditional statements. The absence of this information is largely responsible for the inefficiency in test case generation. We start with an Estelle specification which is supposed to be error-free and conforms to the standards. Furthermore, the specification is assumed to be a single module, without state sets, procedures and functions as a result of transformations. Unlike Normal Form Specification (NFS) [Sarik 87], however, we allow conditional statements which help to avoid the transition explosion problem that occurs in NFS for complex protocols.  Definition 1 A single-module Estelle specification E is defined as a 5-tuple E=<S,P,A,I o ,D>  where • S is the set of states of E, • P is a set of program segments, each program segment associated with a transition of E, • PCSx P x S is a relation of the transitions, • L is the initial state, and  • D is declaration and/or initialization of variables and interaction service primitive. Definition 2 A finite state machine F is defined as a 4-tuple F=< S, L, E, 4  • S is the set of states of F,  > where  CHAPTER 3. TRACE ANALYSIS BASED ON FORMAL SPECIFICATIONS ^24  • L is a set of labels on the transitions of F and each label is represented in the format "input symbol/output symbol", • ECSxLxS is a relation of the transitions, and • I° is the initial state. Procedure 1 Mapping from Estelle specification E to finite state machine F.  For program segment Pi(labelLi) between states A and B of E (F) in Definition 1 (2) respectively, a transition e in E is defined as EE =.< A, Pi , B > and a transition e in F is defined as eF =< A, Li,B >. Pi , contains interaction service primitives  gpi, • • • ,Pn)/0(qi, • • • , q n )  where  • I and 0 are input and output interaction service primitives, respectively, • (pb• • • ,p ° ) and (qi, • • • , q,) are sets of input and output interaction service primitive parameters respectively. The mapping from eE to F is given by the following: if the domain size of every interaction service primitive parameter is small, then  eF =< A, Li, B > if Li = I x p l x • • • x p ° / 0 x qi x • • • x q ° is valid with respect to Pi , else  SF =< A, Li, B > iff Li = I/O is valid with respect to Pi In other words, when the domain sizes of the parameters are small (i.e., the possible combinations of parameter values are manageable), the interaction service primitives and their  CHAPTER 3. TRACE ANALYSIS BASED ON FORMAL SPECIFICATIONS ^25  parameters are enumerated and then included. Otherwise, they are left out to avoid state explosion. In the latter case, symbolic evaluation is used to detect and discard infeasible paths that may be generated as a result (see Definition 3 below). Definition 3 AllPath(X,Si,S0 ,C) is the set of all executable paths from the initial state Si to the final state So of an Estelle (or finite state machine) specification X with constraint C. The constraint C bounds the set of feasible paths. It includes restrictions on the iteration number of while loops and transition loops and conditions limiting the domain space of variables and interaction service primitive parameters for Estelle. Since FSMs have no program segments and do not deal with data and predicates, the constraints C1 of an FSM derived from an Estelle specification E using Procedure 1 is a subset of the constraints C e of E. Theorem 3 Given finite state machine F obtained from an Estelle specification E using Procedure 1, AllPath(F,Si,S 0 ,Cf) D AllPath(E,Si,So,Ce) The proof is obvious when we note that C e D Cf. Definition 4 The set of test cases T, generated from specification X (E or F) with constraints C, initial state Si, and final state So , is Te = {t it =7 (p) such that p E (AllPath(X, Si, So ,C))) where T is a one-to-one function from a path to a test sequence t. The test cases TT consist of a set of test sequences t exhibiting an external behavior of X. Definition 5 Conformance testing is defined as M conf e X if EXT(M)ITT C EXT(X) where EXT is the external behavior function. This definition states that an implementation M of a specification X with constraints C  CHAPTER 3. TRACE ANALYSIS BASED ON FORMAL SPECIFICATIONS ^26  passes a conformance test using test case Tc if the external behaviors of the test is a subset of the allowable behaviors specified by X.  Definition 6 As a generalization of conformance testing in Definition 5, the following definition is useful for trace analysis: M conf X if VC VSi VS0 , M con fc X If X in Definition 6 is replaced by F of Definition 2, then M conf F turns out to be the homing problem discussed in Section 3.2. Theorems 1 and 2 give the bound of message length to uniquely identify the machine's final state. Thus, after at most Lizs messages, the state of the implementation is known and subsequent traces can be determined if they are legal paths according to the specification. The actual length is usually much shorter than the bound given in Theorems 1 and 2. We now outline our proposed procedure for trace analysis/conformance testing as follows: Given an Estelle specification and its implementation M, 1. Transform the Estelle specification into the form given in Definition 1, 2. Apply Procedure 1 to map the Estelle specification E obtained in step 1 into its finite state machine representation F. 3. In accordance with Definition 6 for trace analysis and Definition 5 for conformance testing, (a) Select from F the set of paths satisfying the input and output messages in the case of trace analysis. And select from F all the paths from the given initial state to the given final state with constraints for test case generation,  CHAPTER 3. TRACE ANALYSIS BASED ON FORMAL SPECIFICATIONS ^27  (b) Detect and delete the infeasible paths using symbolic evaluation if necessary, (c) Assign verdict. We may have information loss in the transformation of Procedure 1. The loss is the difference between AllPath sets of F and E in Theorem 3 due to reduction of the constraints. An empirical study on the number of feasible versus infeasible paths for several programs using control flow only [Wood 80] showed that almost every program has a significant number of infeasible paths. The infeasible paths can be detected and deleted by symbolic evaluation [King 76, Clark 85]. Some of the infeasible paths may also be detected using static data flow analysis, but the result is not as satisfactory because the method gives only the necessary (not sufficient) condition for deleting infeasible paths [Podgu 90]. There are three basic methods for symbolic evaluation [Clark 85]: path-dependent symbolic  evaluation describes data dependencies for a path specified by the user or the system; dynamic symbolic evaluation produces a trace of the data dependencies for particular input data sequence; global symbolic evaluation represents the data dependencies for all paths in a program. In our case, we use symbolic evaluation to select a set of paths with consistent path conditions from the set of paths matching the input and output message sequences. This can be considered an extension of path-dependent symbolic evaluation. Even though we may not know the values of internal variables which have an effect on the execution of the specification, they can be inferred by using path condition consistency based on the following rules: 1. We can select a path (or a set of paths) from the specification which matches the observed  CHAPTER 3. TRACE ANALYSIS BASED ON FORMAL SPECIFICATIONS ^28  trace with respect to the interaction service primitives and their parameters. 2. Once the path(s) is determined, the values of some internal variables on the path can be obtained from the specification. 3. The values of the other internal variable can be inferred from the interaction service primitive parameters. Verdicts on external behaviors are dependent on the characteristics of the application: whether we know the initial state, the final state, and the constraints. If we have a nonambiguous test case 7', of Definition 5, then it is possible to determine if the implementation conforms to the specification. In trace analysis where the initial state, final state and constraints are not known as in Definition 6, what we can say about the correctness of the implementation depends on the length of the observed path. For a given protocol, there is a threshold path length It less than or equal to that given by Theorems 1 and 2 which will differentiate every possible ambiguity on the path (see Section 3.5 for i t for X.25 LAPB). For message sequences of length less than or equal to I t , one may conclude the implementation contains error(s) only if EXT(M)  g  EXT(X). However, EXT(M) C EXT(X) does not necessarily  imply conformance.  3.4 Trace Analysis in External Test Architectures In the last section, we have outlined the basic technique for determining whether a trace of input and output messages is permissible with respect to a specification given as an EFSM. However, the method assumes it is possible to correctly observe the input and output messages  CHAPTER 3. TRACE ANALYSIS BASED ON FORMAL SPECIFICATIONS^29  and in the order they are generated. If the implementation under test (IUT) is to be observed externally, it may not be possible to have access to the interaction points of both the upper and the lower interfaces of the IUT directly, thus the assumptions may no longer hold. It is known that local observers are unable to detect all errors [Bochm 89]. We will assume that a system clock will timestamp all events occurring at the IUT, and that a test architecture such as the Ferry [Chans 89] or Astride [Rafiq 90] is used to transfer all local observations to the global analyzer with timing information. The problem remains as to how to organize the local traces into one global trace with the input and output messages ordered properly. This is difficult since messages may be generated spontaneously by the IUT (i.e., without external stimuli) and message delays may occur inside the IUT. We will use the following notation to describe the order of message sequences. Notation 1 Suppose an input message pi results in a response message qi. This input and  output sequence is represented as pi < qi. Notation 2 Suppose the two message sequences pi < qi and pi + i < qi + i have no order rela-  tionship between them. This is expressed as {pi < qi ; pi + i qi + i). Notation 3 If the message pair pi < qi is completed before the sequence pi + i < qi + i starts, the  composite message sequence is represented as pi < qi << pi+i < qi+1. Let (5 be the maximum round-trip propagation delay between the observer and the IUT; that is, the maximum time it takes for a message to travel from the observer to the IUT, for the IUT to send a response, and for the response to travel from the IUT to the observer. The  CHAPTER 3. TRACE ANALYSIS BASED ON FORMAL SPECIFICATIONS^30  order relationship between messages pi and qi can be determined if the timestamps of input message t(pi), output message t(qi) and the round trip delay S is available [Wvong 90]:  1. If t(qi) < t(pi), then qi < pi, 2. If t(qi) > t(pi)+ 5, then pi < 3. If t(pi) < t(qi) < *0+ (5, then pi 54 qi and pi qi.  In case 3 where there is uncertainty on the order of messages, we may consider every possible set of sequences that satisfies the constraints of the program paths of the formal specification. In addition, each message might be spontaneous without external stimuli. If there is an order relationship between messages pi and qi, the number of possible cases will be reduced.  3.5 A Case Study - The X.25 LAPB Protocol We now demonstrate the feasibility of the proposed methodology by applying it to a specific protocol, the X.25 LAPB protocol as specified by ISO 7776 [ISOa]. Section 4.7.1 of the book [Tanen 88] contains a simple overview of the X.25 LAPB protocol. The given Estelle specification of LAPB in Appendix A was translated into the FSM diagram of Appendix B using Procedure 1 described in Section 3.3. The translation was done under the following conditions:  • we had a single module Estelle specification, • we had access to the interaction points at the upper and the lower interfaces,  CHAPTER 3. TRACE ANALYSIS BASED ON FORMAL SPECIFICATIONS ^31  • we integrated the parameters of those interaction service primitives (with very small domain space for each of their parameters) into their message types (see below for details), and, • the transitions containing timer operations were also considered.  From Appendix B we note that there are identical input and output messages such as the sequences g/j or h/k (marked with an * in the appendix). Not only are the message types and parameter values identical, they also end in the same states. Thus, if these sequences are observed without leading message sequences before them, it is not possible to determine the states from which the message sequences start. Note also that transition loops such as w/_ and v/_ (marked ** in Appendix B) may make the threshold value of the homing sequence path length / t large. However in this example the transition loops w/_ and v/_ are used for exception handling so the iteration number is likely to be small. The threshold value of path length I t (measured in terms of number of messages) for X.25 LAPB is, from Appendix B, given by / t = 2 + 2 x (the iteration number of loop transitions).  LAPB has interaction service primitive parameters such as Address, P/F, N(S) and N(R). The address, whose value is either A or B, identifies the intended receiver of a command frame and the transmitter of a response frame. Frames containing commands transferred from the  DCE to the DTE contain the address A and frames containing responses transferred from the DCE to the DTE contain the address B. In the case of DTE, the address is the reverse of the above. In order to differentiate polling and response to polling, LAPB uses the P/F bit  CHAPTER 3. TRACE ANALYSIS BASED ON FORMAL SPECIFICATIONS ^32  which has the value 0 or 1. Each I frame contains a send sequence number N(S). Also all I frames and supervisory frames contain N (R), the expected send sequence number of the next received I frame. For sequence numbers based on modulo 8 or higher, the possible combinations of N (S) and N (R) are large and will cause a large number of transitions if integrated into the control flow. Therefore we have included only the data variables Address and PIF in the control flow (for LAPB, this includes all transitions except those associated with the self loop at state ABM). This means the transitions from ABM to ABM must be handled differently from the rest. The transitions from ABM to ABM will produce infeasible paths which must be detected and deleted. No infeasible paths will be produced for the other transitions, since the data values are integrated into the interaction service primitives.  We demonstrate our approach using two examples from [Wvong 90]. The first example deals with a trace which has no data transfer but involves frame collision. In trace (a) of Figure 3.1, the DCE and the DTE send DISC commands at the same time (DISC collision). The DCE then tries to initiate link set up. Finally the DCE requests link reset by sending a FRMR response, and the DTE resets the link. Note that in our example, the trace analyzer is located near the DCE side and is observing the behavior of the DTE at the both lower and upper interfaces. Based on the timestamps on each message (given in [Wvong 90] but not shown in Figure 3.1) and information on request and response of the messages, we obtain the message sequences  {DISC, A,1 < U A, A,1; {__ < DISC, B,1 ^U A, B,1 < _}} « SABM, A,1 < U A, A,1 «  CHAPTER 3. TRACE ANALYSIS BASED ON FORMAL SPECIFICATIONS ^33  DCE  DIE^DCE^  DISC,A,I  DISC,B,1^I,A,0,2,2  UA,B,1  UA,A,1^  SABM,A,1  DIE  RR,A,0,3 I,B 4O,2,3  .&/  .  UA,A,1  RR,B4O,3  FRMR,B,1 SABM,B,1 ..-------"--  (a) Format:Coremand,AddressOF  (19  Format:1,AddressAN(S),N(R) RR,Address,P,N(R)  Figure 3.1: Sequence of Events in Traces  FRMR, B,1 < SABM, B,1 for the interaction point at the lower interface. Here "2' means the message is either null or not observable from the trace at the lower interface. However, it can be obtained from the upper interaction point or deduced from the specification that the first "_._" is DiscReq from the upper interaction point. There are three transitions, namely ABM --* SEND_DM,SEND_DISC --*  SEND_DISC, and WAIT_S'ABM —' SEND DM which can produce the message pair DISC < UA. From the figure in Appendix B, only one of them satisfies the constraints of the observed trace: Transitions : ABM ► SEND_DISC 24 SENDDISC SEND_DM  A^ B^ C ,----"---,—.—..„ ,----".----, ,--.---,..---,  Messages seqs: DiscReq < DISC, B,1 << DISC, A,1 < UA, A,1 <<U.A,B,1 <  Therefore the trace (a) is valid according to the formal specification.  The second example contains data transfer: the DCE and DTE exchange I frames as  CHAPTER 3. TRACE ANALYSIS BASED ON FORMAL SPECIFICATIONS^34  shown in Figure 3.1(b). Based on the timestamp on each message and information on message types (request or response), we obtain the message trace A^ „--."----.,^  B ,--...",-.,  I, A,0,2,2I_ « _IRR, A, 0,3 << _II, B, 0,2,3 « RR,B, 0,3/_  for a transition from ABM to ABM. The first, third and fourth "2' can be inferred to be  Acklnd << Datalnd, DataReq and Acklnd respectively from the upper interaction point. Therefore the trace becomes  A^  B  I, A, 0,2, 2/{Acklnd << DataInd} << __MR, A,0,3 << DataReql I,B, 0, 2,3 << RR, B, 0, 3/Acklnd.  To analyze the input/output sequences A and B, an examination of transitions t16 and t18 (see Appendix C) shows there are 196 and 48 paths respectively even before the while statements are considered. This means that if we adopt the Normal Form Specification [Sarik 87] instead of Definition 1, the number of Normal Form Transitions (one per path) will be enormous. The Estelle source must not contain procedures and functions in our method; the procedures and functions must be expanded. Timer operations are omitted from those transitions containing timer operations. Also, system functions such as allocation and deallocation of memory space should be deleted as they do not affect the outcome of trace analysis but unnecessarily complicate the processing. To improve efficiency in the analysis, we use a technique similar to program slicing [Weise 81]. Paths which do not modify program variables are bypassed unless subsequent trace shows the assumption to be incorrect. For example, IsCorrectAck of transition t16 generates some paths  CHAPTER 3. TRACE ANALYSIS BASED ON FORMAL SPECIFICATIONS ^35  which contain conditional statements only but do not update any program variables. These paths are bypassed by assuming the path in bold arrow. If the assumption is invalid, inconsistencies will show up in subsequent external behaviors of the IUT, such as OUTPUT statements. In our example, OUTPUT statements of transitions t16 and t33 show the assumption to be correct using symbolic evaluation. Of the four paths between points B and C of the flow chart in Appendix C (derived from Appendix A), three of them containing OUTPUT P.Acklnd are candidate paths by rule 1 of path condition consistency listed in Section 3.3. With this information, we can deduce the predicate frameA.NR <> LastRxNR by rule 2, but we do not know whether TimerRecovery  = false. Just after point C in the flow chart, Datalnd from the upper interaction point gives us one path by rule 1, and this allows us to decide that LocalRNR=false by rule 2. Also  WriteSFrame(RR,O,A) comes from transition t33 which is between D and E. At that time, timer "delay(T2)" is skipped. Transition t27 from E to F in the flow chart gives us the values of a number of variables such as RemoteRNR=false, TimerRecovery=false, aframeA.NS=VS and aframeA.NR=VR by rule 2. These in turn allow us to select paths which are dependent on internal variables. For example, the information TimerRecovery=false, which was unknown between points B and C, provides enough information to select one path (in bold line) out of the three candidate paths. Also, the second I frame in the trace containing aframeA .NR gives the value 3 for the internal variable VR because of the assignment statement aframeA .NR := VR just after point E in the flow chart. Since the I frame's aframeA.NS has value 2, the predicate frameA.NS <> VR  CHAPTER 3. TRACE ANALYSIS BASED ON FORMAL SPECIFICATIONS ^36  which appears between points C and D is inferred to be false by rule 3. Thus, the correct path between points C and D which was marked in bold can be verified as one matching the observed trace. Furthermore, clearrecovery in ReadSFrame just after point F is evaluated to false using the values of variables already known to us. The values of interaction service primitive parameters of RR, the interaction service primitive type RR itself, the value of clearrecovery, and the predicate RemoteRNR = false eliminate all but one path in transition t18 between points F and G that satisfies all the constraints. As a result we have one path satisfying the observed input and output message trace. Therefore the trace (b) is valid according to the formal specification.  3.6 Test Case Generation and Validation Early work on automating the selection of test cases is based on the FSM model. This model discusses the control flow of a protocol and has been widely used in test case generation. More recently, the data flow of a protocol is being taken into consideration as well by using an EFSM model. As mentioned earlier, test case generation and trace analysis share some common functions which can be depicted using Figure 3.2. For test case generation, the Path Selection phase generates a set of paths whose initial and final states are equal to that of FSM F. For trace analysis this phase generates a set of paths whose input and output interactions match the observed input and output sequences as described in Section 3.3. In order to make the number of paths manageable, we make use of structural constraints which place limitations  CHAPTER 3. TRACE ANALYSIS BASED ON FORMAL SPECIFICATIONS^37  Initial and Final States Constraints  ^ Formal Specification  Back End of Passive Monitoring  Path Selection  Trace  V Data Selection  Path Selection  Symbolic Evaluation ti  Test Case Generation  Trace Analysis  Test Case Validation  Figure 3.2: Test Case Generation and Trace Analysis on transition loops, while statements, and intermodule communication. We have described  AllPath, the most powerful criterion in data flow analysis. For test case generation, the Data Selection phase generates a set of test data for each path selected in the Path Selection phase. In trace analysis, a trace can be viewed as a modified test case. The verdict is removed, and information is randomly mixed with environmental effects such as uncertainty of message ordering and/or loss of test data. In the Data Selection phase, in order to make the number of test cases finite, we make use of data constraints which place limitations on the variables and input interaction parameters. The general constraint satisfaction problem is undecidable. If the domain of variables and input parameters of the protocol is finite, the constraint satisfaction problem is NP-complete but may be solved in reasonable computation time [Chun 90]. Recently proposed test case generation approaches for Estelle include data flow analysis for test path selection [Ural 87], a hybrid method combining the control and data flows [Sank 87],  CHAPTER 3. TRACE ANALYSIS BASED ON FORMAL SPECIFICATIONS^38  and Constraint Logic Programming for generating only feasible test cases with constraints on the parameters of input interactions [Chun 90]. Podgurski compares a number of data flow path selection criteria [Podgu 90]. One of the major weaknesses of all data flow criteria is that they are based solely on syntactic information and do not consider semantic issues such as infeasible paths. The presence of a data flow anomaly does not imply that execution of the program will definitely produce incorrect results; it only implies that it may produce incorrect results. Our model, which handles both control flow and data flow, can be used not only for trace analysis but also for test case generation. For example, if we transform the Estelle specification of X.25 LAPB into F by Procedure 1, we can generate all possible execution paths  All P ath(F, Si, So C). By selecting specific initial and final states with constraints for test case ,  generation, the paths can be structured as a tree. All paths except those transitions from the state ABM to ABM of LAPB cover every possible combination of data flow. Therefore, we do not need to use the Data Selection phase on them. Unfortunately, even though the domains of variables and input interactions are finite, paths containing the transition from ABM to ABM have a large number of value combinations of variables and input interaction parameters. For these paths, data selection can be done by random selection, static data flow analysis [Ural 87], constraints [Chun 90], or simply by exhaustive enumeration. Test case validation is equivalent to trace analysis without considering the environmental effects on traces such as uncertainty of the message order and/or loss of the test data. The test case validation based on LOTOS was done by using TETRA[Bochm 90], a modified version of a LOTOS interpreter, and the test case validation based on Estelle has been done [Zhou 92]  CHAPTER 3. TRACE ANALYSIS BASED ON FORMAL SPECIFICATIONS ^39  by using the trace analyzer (this will be shown in the Chapter 4).  3.7 Chapter Summary We have presented the basic techniques used to perform trace analysis for Estelle specifications. Indeed, since the model is based on EFSMs, it will work with any specifications that can be translated into EFSM representations. In order to avoid transition explosion as a result of normalization of Estelle specifications, we included conditional statements and introduced symbolic evaluation to detect and discard infeasible paths. Some practical issues such as trace analysis using an external test architecture were also discussed. The technique was illustrated using X.25 LAPB to show that it can handle some of the difficult problems such as frame collisions and data flow rigorously. We also showed the relationship between trace analysis and test case generation and briefly discussed how our framework can be extended to include test case generation and validation.  Chapter 4  Implementation of Trace Analyzer In this chapter, a prototype implementation of the trace analyzer is described in order to demonstrate the feasibility of the unified model proposed in the previous chapter. A high-level description of the implementation is given in Appendix D.  4.1 Brief Description of Tools The tools used for developing the trace analyzer are briefly outlined below. Details can be found in [Sampl 90] (on ASN.1) and [Lu 91] (on TESTGEN parser). The specification of X.25 LAPB in Estelle.Y and ASN.1 was hand coded and translated from an Estelle specification of the protocol to be traced. The TESTGEN parser together with an ASN.1 parser is used to translate the specification in Estelle.Y and ASN.1 into an internal format known as Protocol Data Structure (PDS). The trace analyzer consists of two phases: a preprocessing phase and a main analysis phase. It works directly on the PDS for trace analysis or test case validation.  40  CHAPTER 4. IMPLEMENTATION OF TRACE ANALYZER ^  41  Protocol Specification in Estelle ....,.....,..................,-•-•""^---s.............................4._  ASN.1 representation of Data Part  Protocol Specification in Estelle.Y  TESTGEN Parser  /Protocol Data Structure  Trace from Passive Monitoring  Preprocessing Phase^Test Suites  Trace Analysis  .e',^Test -.------  Case Validation  Main Analysis Phase = File Trace Analyzer  II  .-^N, Verdict ^i ,  C) Dynamic Module  v1 Data Structure  Figure 4.1: Overall Structure of Trace Analyzer  4.1.1 Estelle.Y with ASN.1 Estelle.Y uses an Extended Transition System (ETS) to model the observable behaviors of a protocol, and ASN.1 to model the data representations. The syntax of the behavior part of an  Estelle.Y specification is essentially that of a single module Estelle specification. Abstract Syntax Notation One (ASN.1) is a notation or language for the definition of abstract data types and their values. It is also used as a transfer syntax. ASN.1 is standardized by ISO[ISOe] and is widely accepted as a formal language for specifying the data structures of  CHAPTER 4. IMPLEMENTATION OF TRACE ANALYZER^  42  higher level OSI protocols. The structure of Input Service Primitives (ISPs), Output Service Primitives (OSPs) and Protocol Data Units (PDUs) in Estelle.Y specifications are also specified using ASN.1. The  ASN.1 parser[Sampl 90] was developed using the UNIX Lex/Yacc tools. It produces an ASN.1 type tree from an ASN.1 specification. The PDS maintains pointers into the ASN.1 type tree to allow information to be accessed. The main differences between Estelle.Y and NormalFormSpecification [Sarik 86], which is used in most protocol testing work based on Estelle, are that:  • Estelle.Y uses ASN.1, and • Estelle.Y supports more Pascal statements such as the conditional and loop statements in transitions. The inclusion of ASN.1 provides explicit language support on data structures for ISPs,  OSPs, PDUs and their parameters.  4.1.2 Translation from Estelle to Estelle.Y Estelle.Y supports only single module specifications, at most one ISP and at most two OSPs (one at the lower interface and one at the upper interface) for each transition, no procedures, no functions and no state sets. Besides the problem of multiple modules, two issues arise in the translation: how to handle while loops containing OSPs and how to handle transitions containing timers. These issues will be discussed in Section 4.2.2 and 4.2.3 respectively.  CHAPTER 4. IMPLEMENTATION OF TRACE ANALYZER ^  43  4.1.3 Protocol Data Structure The PDS is designed to be a machine accessible form of the ETS/ASN.1 based formal description. It holds information about both the control and the data flows of a protocol specification. The ISP, OSP and PDU data types are stored in the data structures of the service primitives in ASN.1 type trees.  4.1.4 TESTGEN Parser The TESTGEN parser is designed for test case generation with respect to control and data flows of formal protocol specifications. It parses Estelle.Y /ASN.1 specifications and generates a corresponding PDS. The ASN.1 parser is used to convert the ASN.1 specification into  ASN.1 type trees. The ASN.1 type trees are linked to the PDS by the TESTGEN parser when the Estelle.Y specification is being parsed. As a result, the PDS includes both Estelle.Y and ASN.1 protocol information generated from an Estelle.Y/ ASN.1 specification.  4.2 Implementation Issues 4.2.1 Known Initial State Our techniques assume the initial state is known. There are two reasons for this: one is that protocols run reactively (i.e., they will always return to the initial state at some time), and the other is that after idling for some time, protocols usually start at the initial state [Chans 91]. This assumption provides simple, fast and efficient solutions for symbolic evaluation. Whenever we interpret symbolic predicate expressions, decisions can be made without back-tracking because the values of variables and ISP and OSP parameters are known.  CHAPTER 4. IMPLEMENTATION OF TRACE ANALYZER ^  44  4.2.2 Unfolding Loops The Estelle specification may contain while statements in some of the transitions. The while statements may or may not contain "OUTPUT" primitives. The latter case poses no problem since the values of variables, including the number of loop iterations, are known. The former case cannot be included in a transition of Estelle.Y, since Estelle.Y allows at most one input and at most two outputs for each transition. Therefore, the while loops containing "OUTPUT" statements must be unfolded. The number of iterations of a while loop containing "OUTPUT" statements depends on the particular trace. One possibility is to translate into Estelle.Y form by using auxiliary states and variables. The transition in Estelle below is translated into five transitions in Estelle.Y. In order to handle the while statement containing "OUTPUT", an auxiliary state "ABMONE" and the variables "tmppf" and "tmpnr" are used. Note that last two transitions in the Estelle.Y specification are spontaneous ones and include the false condition of while statement in their "PROVIDED" clause.  /* a transition in Estelle */ FROM ABM TO ABM WHEN P.Datalndicat BEGIN while (LastRxNR <> Datalndicat.nr) do begin LastRxNR := (LastRxNR + 1) mod Modulus; OUTPUT S.AckIndicat;  CHAPTER 4. IMPLEMENTATION OF TRACE ANALYZER ^  end; if (DataIndicat.PF = 1) SendingREJ := false; else SendingREJ := true; END;  /* a set of transitions in Estelle.Y from the above */ FROM ABM TO ABMONE WHEN Datalndicat PROVIDED (LastRxNR <> Datalndicat.nr) OUTPUT Acklndicat BEGIN LastRxNR := (LastRxNR + 1) mod Modulus; tmppf := Datalndicat.PF; tmpnr := Datalndicat.nr; END;  FROM ABM  45  CHAPTER 4. IMPLEMENTATION OF TRACE ANALYZER ^  TO ABMONE WHEN Datalndicat PROVIDED (LastRxNR = Datalndicat.nr) BEGIN tmppf := Datalndicat.PF; tmpnr := Datalndicat.nr; END;  FROM ABMONE TO ABMONE PROVIDED (LastRxNR <> tmpnr) OUTPUT Acklndicat BEGIN LastRxNR := (LastRxNR + 1) mod Modulus; END;  FROM ABMONE TO ABM PROVIDED ( tmppf = 1) AND (LastRxNR = tmpnr) BEGIN  46  CHAPTER 4. IMPLEMENTATION OF TRACE ANALYZER^  47  SendingREJ := false; END:  FROM ABMONE TO ABM PROVIDED (tmppf <> 1) AND (LastRxNR = tmpnr) BEGIN SendingREJ := true; END: As a result of unfolding loops, one atomic transition from an Estelle specification could be split into multiple atomic transitions in an Estelle.Y specification. This could lead to semantic inconsistency. However, this does not effect the results of trace analysis since the order of transition execution is not changed. Unfolding loops while maintaining semantic integrity may be useful for some other applications and is left as future research.  4.2.3 Transitions with Timers Physical global clocks in distributed systems usually do not exist. In conformance testing, two clocks are used: one in the IUT and the other in the Tester. Some transitions of the IUT may depend on the timer. A transition may be executed after a specific time given by the timer has elapsed. It is generally hard to relate external behaviors of IUT with time. Therefore, when we analyze traces with respect to formal specifications, we do not rely on these timers. Instead we consider the traces as transitions without timers. If the output of the IUT matches  CHAPTER 4. IMPLEMENTATION OF TRACE ANALYZER^  48  with one from the formal specification, we include those transitions as candidate transitions to be checked. This means the number of candidate transitions could be more than in the case where timers are considered. However, if there are no candidate transitions when timers are not considered, there will be no candidate transitions even if timers are included. For the purpose of trace analysis, no incorrect conclusion will be drawn by ignoring the timers. It is possible to use a loosely-tuned timer to increase performance when processing transitions containing timers, since this technique could produce fewer candidate transitions.  /* a transition in Estelle */ FROM SEND DM TO SEND DM PROVIDED (TxAttempts <= N2) delay(T1) BEGIN frame.frametype := DM; frame.pf := 0; frame.address := A; TxAttempts := TxAttempts + 1; OUTPUT P.DataRequest(frame); END;  /* a transition in Estelle.Y */  CHAPTER 4. IMPLEMENTATION OF TRACE ANALYZER^  49  FROM SEND_DM TO SEND_DM PROVIDED (TxAttempts <= N2) OUTPUT DataRequest BEGIN DataRequest.frametype := DM; DataRequest.pf := 0; DataRequest.address := A; TxAttempts := TxAttempts + 1; END;  4.2.4 Preprocessing Phase The preprocessing phase is not considered part of the actual trace analysis. Its function is to improve the performance and efficiency of the main analysis phase. The preprocessing phase shown in Appendix D.1 translates some transitions of EFSM into FSM transitions consisting of input symbols and output symbols only (i.e., no internal variables). This scheme is a modification of Procedure 1 in Chapter 3. Instead of enumerating all possible combinations of service primitives and their parameters, some parts of the enumeration are done based on cost-effectiveness. For example, the transition below is in the form of an FSM with "INPUT" and "OUTPUT" involving no internal variables.  FROM SEND_DM  CHAPTER 4. IMPLEMENTATION OF TRACE ANALYZER ^  50  TO SEND_DM  I  WHEN Datalndicat^  PROVIDED (DataIndicat.frametype = I) AND 'INPUT (Datalndicat.address = A) AND ^I (Datalndicat.pf = 1)^  I  OUTPUT DataRequest^ I BEGIN^  I  DataRequest.frametype := SABM; !OUTPUT DataRequest.pf := 1;^I DataRequest.address := B;^I  END;  Format: (set of input values)/ (set of output values)  SEND_DM Figure 4.2: Corresponding Finite State Machine.  4.2.5 Search Method As mentioned in Section 3.6, test case generation requires the initial and terminal states to be known but trace analysis does not. Test case generation can adopt either depth-first or  CHAPTER 4. IMPLEMENTATION OF TRACE ANALYZER ^  51  breadth-first search method, but it is more appropriate to use breadth-first search for trace analysis since the terminal states are not known. This implies that breadth-first search can be used for both trace analysis and test case generation.  4.2.6 Pruning Candidate Transitions At any state, the values of related variables are known because of the assumption in Section 4.2.1. In order to prune candidate transitions, three steps are used: Step 1. If a transition is in the form of an FSM, compare the input/output list produced by the preprocessing phase in Procedures 4.1 and 4.2 in Appendix D to the trace. If the list does not match the trace, prune the transition. Step 2. For the transitions in an EFSM form, interpret the symbolic predicate expressions by substituting the values of variables and ISP parameters. If the result of the interpretation is false, prune the transition. Step 3. Of those transitions that survive Step 2, execute the statements inside the transitions and compare the OSP parameters with the trace. If the OSP parameters do not match the trace, prune the transition.  4.2.7 Verdict and Location of Errors The trace analyzer logs the transitions of a formal specification which satisfy the given traces in a file. If a trace does not conform to the formal specification, the trace analyzer stops at that point with an error message displayed on the screen for the user. It also provides the  CHAPTER 4. IMPLEMENTATION OF TRACE ANALYZER^  52  values of related variables just before the point of failure to help the user locate the errors in the Estelle.Y specification. An example is shown in Section 4.3.1. If the trace conforms to the formal specification, the trace analyzer continues processing. Once all traces have been processed, the logged information shows which transitions were executed. Sometimes, more than one path may satisfy the traces due to nondeterminism. In this case we can follow these paths using "transition keys" given in the file. Every transition has a unique "transition key" identifying its location in the source of the Estelle specification. In addition, each executing transition is labelled by a unique "transition id" and its "parent transition id". In the notation "(i, j)", i and j denote transition id and parent transition id respectively. For example, "(1,0)" in Figure 4.3 depicts a transition with "transition id" 1 and "parent transition id" 0. This allows the user to resolve the case when more than one path satisfies a given trace. (0,0)  Figure 4.3: Data Structure for Nondeterminism.  CHAPTER 4. IMPLEMENTATION OF TRACE ANALYZER^  53  4.3 Sample Experiments The prototype implementation of the trace analyzer has around 7,000 lines of C code. We tested the trace analyzer using the X.25 LAPB protocol. The Estelle specification of X.25 LAPB in Appendix A is around 700 lines. The Estelle.Y in Appendix G and ASN.1 in Appendix F translated from the Estelle specification are around 1600 and 100 lines, respectively. Four cases of LAPB trace analysis are documented below.  4.3.1 Cases 1 and 2 Case 1 checks to ensure the IUT sends a DM with F=1 in response to a DISC command with P=1 received in the disconnected state. Each test case consists of "inputl (or input2) / outputl / output2" where inputl and outputl are to the lower interaction point of the IUT and input2 and output2 are to the upper interaction point. Inputl and outputl consist of "interaction primitive", "PDU type", "address", "P/F bit", "send sequence number", "receive sequence number" and "data" fields. In this case, we send a DISC and wait for a DM or UA as the preamble; we send an RR command with P=1 and wait for a DM with F=1 as the postamble. This trace conforms to the specification and produces the following log file.  Trace for Case 1: Datalndicat DISC A 1 - - - / DataRequest DM A 1 - - - / Datalndicat DISC A 1 - - - / DataRequest DM A 1 - - - / Datalndicat RR A 1 - 0 - / DataRequest DM A 1 - - - / -  CHAPTER 4. IMPLEMENTATION OF TRACE ANALYZER ^  54  Log file for Case 1: Transition Key = 2 From State = SEND_DM To State = SEND_DM Parent_Transition_ID = 0 Transition_ID = 0  Transition Key = 2 From State = SEND_DM To State = SEND_DM Parent_Transition_ID = 0 Transition_ID = 1  Transition Key = 5 From State = SEND_DM To State = SEND_DM Parent_Transition_ID = 1 Transition_ID = 2 Case 2, below, shows invalid IUT behaviors. We send a DISC and wait for a DM or UA as the preamble. In the test body, the IUT sends a UA in response to the tester's DISC command, instead of a DM. This trace does not conform to the specification. Therefore, the trace analyzer produces log information up to the point where the trace no longer conforms to the specification and gives the values of variables to help locate errors.  Trace for Case 2: Datalndicat DISC A 1 - - - / DataRequest DM A 1 - - - / Datalndicat DISC A 1 - - - / DataRequest UA A 1 - - - / -  Log file for Case 2: Transition Key = 2 From State = SEND_DM To State = SEND_DM  CHAPTER 4. IMPLEMENTATION OF TRACE ANALYZER ^  Parent_Transition_ID = 0 Transition_ID = 0  Values of Variables: key = 0 name = TxAttempts type = INT_TYP int val = 0 key = 1 name = clearrecovery type = BOOL_TYP bool val = false  • • key = 20 name = tmpaddress type = INT_TYP int val = 0  55  CHAPTER 4. IMPLEMENTATION OF TRACE ANALYZER ^  56  4.3.2 Case 3 In this trace, the tester and the IUT send DISC commands at the same time (DISC collision) after the preambles. The first two test cases are preambles used for connection setup. The trace conforms to the specification.  Trace for Case 3: Datalndicat DISC A 1 - - - / DataRequest DM A 1 - - - / Datalndicat SABM A 1 - - - / DataRequest UA A 1 - - - / Conlnd DiscReq ^ / DataRequest DISC B 1 - - - / Datalndicat DISC A 1 - - - / DataRequest UA A 1 - - - / Datalndicat UA B 1 - - - / Disclnd ^ / -  Log file for Case 3: Transition Key = 2 From State = SEND_DM To State = SEND_DM Parent_Transition= 0 Transition_ID = 0  Transition Key = 1 From State = SEND_DM To State = ABM Parent_Transition= 0 Transition_ID = 1  Transition Key = 96 From State = ABM To State = SEND_DISC Parent_Transition= 1 Transition_ID = 2  CHAPTER 4. IMPLEMENTATION OF TRACE ANALYZER ^  57  Transition Key = 123 From State = SEND_DISC To State = SEND_DISC Parent_Transition= 2 Transition_ID = 3  Transition Key = 124 From State = SEND_DISC To State = SEND_DM Parent_Transition= 3 Transition_ID = 4  4.3.3 Case 4 This trace checks to ensure the IUT handles an I frame transfer and an REJ command with P=1 correctly, by sending an RR with F=1. As a preamble, the tester sends a DISC and waits for a DM or UA, then sends a SABM and waits for a UA. For the postamble, the tester sends an FRMR and waits for a SABM or DM. This trace conforms to the specification. Trace for Case 4: Datalndicat DISC A 1 - - - / DataRequest DM A 1 - - - / Datalndicat SABM A 1 - - - / DataRequest UA A 1 - - - / Conlnd Datalndicat I A 0 0 0 9/ Datalnd ^ / ^ / DataRequest RR A 0 - 1 - / DataReq ^ / DataRequest I B 0 0 1 9 / DataIndicat I A 0 1 0 9/ DataInd ^ / ^  -  / DataRequest RR A 0 - 2 - / -  DataReq ^ / DataRequest I B 0 1 2 9 / -  CHAPTER 4. IMPLEMENTATION OF TRACE ANALYZER ^  Datalndicat I A 0 2 0 9/ Datalnd ^ / ^ / DataRequest RR A 0 - 3 - / -  DataReq ^ / DataRequest I B 0 2 3 9 / DataIndicat REJ A 1 - 0 - / DataRequest RR A 1 - 3 - / Datalndicat RR B 0 - 0 / ^ / Datalndicat FRMR B 0 - - - / DataRequest SABM B 1 - - - / Disclnd Datalndicat DM B 1  / -  Log file for Case 4: Transition Key = 2 From State = SEND_DM To State = SEND_DM Parent_Transition= 0 Transition_ID = 0  Transition Key = 1 From State = SEND_DM To State = ABM Parent_Transition= 0 Transition_ID = 1  Transition Key = 30 From State = ABM To State = ABM Parent_Transition= 1 Transition_ID = 2  Transition Key = 103 From State = ABM To State = ABM Parent_Transition= 2 Transition_ID = 3  58  CHAPTER 4. IMPLEMENTATION OF TRACE ANALYZER^  Transition Key = 94 From State = ABM To State = ABM Parent_Transition= 3 Transition_ID = 4  Transition Key = 30 From State = ABM To State = ABM Parent_Transition= 4 Transition_ID = 5  Transition Key = 103 From State = ABM To State = ABM Parent_Transition= 5 Transition_ID = 6  Transition Key = 94 From State = ABM To State = ABM Parent_Transition= 6 Transition_ID = 7  Transition Key = 30 From State = ABM To State = ABM Parent_Transition= 7 Transition_ID = 8  Transition Key = 103 From State = ABM To State = ABM Parent_Transition= 8 Transition_ID = 9  Transition Key = 94 From State = ABM To State = ABM Parent_Transition= 9 Transition_ID = 10  59  CHAPTER 4. IMPLEMENTATION OF TRACE ANALYZER ^  60  Transition Key = 59 From State = ABM To State = ABM Parent_Transition= 10 Transition_ID = 11  Transition Key = 47 From State = ABM To State = ABM Parent_Transition= 11 Transition_ID = 12  Transition Key = 92 From State = ABM To State = SEND_SABM Parent_Transition= 12 Transition_ID = 13  Transition Key = 16 From State = SEND_SABM To State = SEND_DM Parent_Transition= 13 Transition_ID = 14  4.3.4 Performance We measured the performance of the trace analyzer running on a SUN 4/690 with 65 M Bytes of main memory for the three test cases given above. The number of traces applied, total time taken, average time per trace, and number of candidate transitions processed are shown in rows (1), (2), (3) and (4) respectively. Row (4) shows transitions applied between the beginning and end of trace analysis, not including the preprocessing phase. These values can be split into four groups: items corresponding to Step 1, Step 2 and Step 3 as described in Section 4.2.6 and an item for processing the matched transitions. The fact that Cases 1 and 3 deal with control flow exclusively and Case 4 contains  CHAPTER 4. IMPLEMENTATION OF TRACE ANALYZER^  (1) Number of Traces (2)Total Time (3)=(2)/(1)Average Time per Trace (4)Total Number of Transitions (5)Number of Transitions pruned in Step 1 (6)Number of Transitions pruned in Step 2 (7)Number of Transitions pruned in Step 3 (8)Number of Matched Transitions  Case 1 3 0.78 0.26  Case 3 5 1.31 0.26  Case 4 15 5.45 0.36  39 36 0 0 3  95 90 0 0 5  601 534 52 0 15  61  Table 4.1: Performance of the trace analysis (time unit: second) both control and data flow accounts for the differences in the values for row (3). Row (3) gives the average time taken to process a trace. In particular, note that of the 3 steps classified in Section 4.2.6, no transitions were processed in Step 3 as shown in (7). We believe that most traces could be checked for conformance to the formal specification using only Steps 1 and 2. Also, a trace like Case 4 consisting of a pair of inputs and outputs dealing with both control and data flows spends an average of 0.4 seconds per trace. Cases 1 and 3, which have no data flow, have no data related to Step 2 as shown in row (6).  4.4 Future Work Several improvements can be made on the prototype implementation.  1. Automate the translation of Estelle specifications to Estelle.Y and ASN.1, 2. Automatic unfolding of while loops, 3. Support more than two Interaction Points for more general protocols, and  CHAPTER 4. IMPLEMENTATION OF TRACE ANALYZER ^  62  4. As the implementation was built upon a prototype of TESTGEN, system tuning is needed to reduce memory requirements and to improve performance.  Chapter 5  Concurrency Model In this chapter, we present a concurrency model as an intermediate step to extend the trace analysis model shown in Chapters 3 and 4 to a concurrent environment. Concurrent events, concurrency blocks, global states, concurrency measures, communication deadlocks and data races are defined based on the model. The model allows high-level abstractions to be used for understanding concurrent behaviors and allows concurrency measures to be computed efficiently. The definitions are applicable to the formal description techniques Estelle and LOTOS, as well as any high-level concurrent languages such as Ada, Occam and Modula II.  5.1 Formal Concurrency Model Communication deadlocks and data races are silent errors which do not generate any error message. We will assume that time-event sequences, or traces, are available for every task that interacts with other tasks directly or indirectly through message passing or shared memory. Tasks that do not interact are not of interest here as they will not affect the behavior of other tasks.  63  CHAPTER 5. CONCURRENCY MODEL ^  64  Definition 7 An event is the atomic execution of a statement of a task 1 . Definition 8 The k-th event of the i-th task is represented as T1(k). The events in a task are totally ordered, numbered and executed sequentially. The total order of events in a task is transitive, asymmetric and irreflexive. 5.1.1 Synchronous and Asynchronous Communications Definition 9 A Synchronous Communication Event (SCE) between two tasks i and j consists of two symmetric events denoted by SCE(Ti(k), Ti(1)) where Ti(k) and Tj(1) are matching send/receive (or offer/accept) events. One of the tasks involved in an SCE will wait until the matching event is offered by the other task. Then both tasks will proceed simultaneously. If the communication is asynchronous, denoted as ACE(Ti(k), Ti (1)), the receiving task j will wait for the matching send event and then proceed. The sending task i, however, can proceed as soon as the message is sent. We will adopt the 2 relation given in [Lampo 78] to specify the partial ordering of events in concurrent programs. The relation is transitive, asymmetric and irreflexive. Two distinct events are said to be concurrent if there is no relation between them. The send/receive events of an SCE are concurrent whereas there is a relation between the two events of an  ACE.  B".  'A task is equivalent to a module instance in Estelle or a process in LOTOS. 'Event A happened before event B is denoted by "A —• B", and event A is concurrent with event B by "A co  ^ ^  CHAPTER 5. CONCURRENCY MODEL^  ^0  ^0 i^1 0^0 2 4)^02^20^02^  65  2••2  3 101 3 3 11111 3^3^3^3 4 4)^0 4^4 4o^4) 4 4 4 4  p4  •^  5 5 /4 5 60^06^60^4) 6^6^6^6•6  ^5 0^0 5^5 0^0 5  5  0^07 7 0^0  (a) synchronous  (b)asynchronous  (a')  (b')  Figure 5.1: Time-event Sequence Diagrams and Their Corresponding DAGs To further illustrate the differences between synchronous and asynchronous communications, refer to Figure 5.1. Cases (a) and (b) in Figure 5.1 are time-event sequence diagrams. The observable events are represented by circles, the vertical edges (arrows) denote total ordering of the events within each task, and the diagonal edges represent the message send/receive events between the two tasks. The origin of an arrow denotes the send event and the head of the arrow the receive event. In case (a), where the communications are synchronous, the following relations hold in addition to the total orders of the internal events of each task:  CHAPTER 5. CONCURRENCY MODEL^  66  TA(1) co (any event in set {TB(1),TB(2)}), TA(2) co TB(3), (any event in set {TA(3),TA(4),TA(5)}) co TB(4),  TA(6) co TB(5), TA(7) co (any event in set {TB(6),TB(7)}) and, (any event in set {TA(1),TB(1),TB(2)}) -+ (any event in set {TA(2),TB(3)}) —> (any event in set {TA(3),TA(4),TA(5),TB(4)}) —> (any event in set {TA(6),TB(5)}) --+ (any event in set {TA(7),TB(6),TB(7)}). In case (b), in addition to the total orders of the internal events of each task, there is another total order listed below: TA(1) —> TA(2) --+ TB(3) -- TB(4) -4 TB(5) —> TA(6) --4 TA(7). Furthermore, the following relations also hold.  (any event in set {TA(1),TA(2),TA(3),TA(4),TA(5)})  co (any event in set {TB(1),TB(2)}), (any event in set {TA(3),TA(4),TA(5)})  co (any event in set {TB( 3 ),TB( 4 ),TB(5),TB(6),TB(7)}), (any event in set {TA(6),TA(7)}) co (any event in set {TB(6),TB(7)}).  CHAPTER 5. CONCURRENCY MODEL^  67  5.1.2 Concurrency Checking The ordering relations for events in a time-event sequence diagram can be explicitly represented using a graph notation shown in (a') and (b') of Figure 5.1. The algorithm to transform a timeevent sequence diagram into this graph form is straightforward: Procedure 2 (Transformation)  For all i and all k, construct edge(—► from T, (k) to Ti (k +1). For all ACE(Ti(k),Ti(1)) where i j, construct edge (—p) from Ti (k) to Ti(l). For all SCE(Ti(k),Ti(1)) where i j, combine Ti(k) and Ti(1) into a single event E. {Note that E will have two incoming arrows from nodes corresponding to Ti(k — 1) and Tj — 1) in the time-event sequence diagram respectively. There are also two outgoing arrows from E to nodes corresponding to Ti (k + 1) and Ti (l + 1) in the time-event sequence diagram respectively.) With Procedure 2, the problem of determining the concurrency relation between two events in a time-event sequence diagram becomes one of determining the connectivity relation between two vertexes in a Directed Acyclic Graph (DAG). The asymmetric and irreflexive properties of the —> relation makes the graph acyclic. The graphs (a') and (b') of Figure 5.1 are simple 3 , finite, directed and have unit-length edges 4 . To determine the concurrency relation between 3 The  graph has neither parallel edges nor cycles.  4 The graph can have arbitrary positive length edges, but the unit-length definition fulfills the definition of --+ relation.  CHAPTER 5. CONCURRENCY MODEL^  68  two events in the graph, all we need to know is whether there are any directed paths between the corresponding vertexes. The widely used algorithm suggested by Moore [Moore 59] for determining the shortest path can be adapted for our application. The complexity of Moore's algorithm is 0(E), where E is the number of edges. Algorithm 1 (Concurrency Checking) Apply Procedure 2 to the time-event sequence diagram to produce a DAG. Two events are concurrent if there is no directed path (using, for example, Moore's algorithm) between them. In all other cases, the events are ordered. Note that the events in an SCE are concurrent. This algorithm works for both asynchronous and synchronous communications. It can be easily shown that applying Algorithm 1 to (d) and (be ) produces the same ordering relations as listed above. The logical time technique used in [Fidge 91, Matte 89] is similar to the problem of labelling nodes in a graph. The logical time approach needs to label every event using vector time. However, once the labelling is done, the comparison time of any pair of vertexes is uniform. Our method does not require the events to be labeled, but if the graph is large, computing the shortest path becomes expensive. We will introduce a technique to minimize the number of events which have to be managed by this method to make it efficient. Definition 10 A communication deadlock 5 exists if 1. in an SCE or ACE, one of the matching events never occurs, or 5  The term deadlock is also used to mean blocking in this chapter.  CHAPTER 5. CONCURRENCY MODEL^  69  2. there is a transitive closure of relation among the synchronous send and receive events (i.e., circular waits). Execution of concurrent specifications (or programs) can be represented by the Rendezvous Graph [Tai 86], Concurrency Map [Stone 88], or Parallel Dynamic Program Dependence Graph [Mille 88]. These representation methods focus on exhibiting potential concurrency with the emphasis on intertask dependencies. Basically, these are attempts to capture Lamport's —+ relation and impose partial orders on the set of events that make up an execution instance. However, so far there has been no elegant method based on these representation techniques to describe concurrent events, global states, concurrency measures, communication deadlocks and data races of concurrent specifications. We shall present a new model in the following sections.  5.1.3 Global Synchronization Cut The basic concept is to detect ordering of events among tasks in a system based on their communication behaviors. Other forms of synchronization such as those due to task activation and completion are not considered.  Synchronous Communication Let us suppose that a set of distributed tasks interact with one another using synchronous communications. We observe that how far the events of a task may proceed may be limited by other synchronous communication operations which are yet to be executed. For example, in Figure 5.2, task A may execute events TA (1) and TA (2), but must wait for the SCE(TA(3),TB(4)) before it can proceed further. Similar constraints exist for every task. Thus, from a particular point in time when an SCE occurs, it is possible to draw a line in a time-  CHAPTER 5. CONCURRENCY MODEL ^  TASK A  B  C  70  BGSCO Block 1 FGSC I fr  Time  ^  BGSC 1 Block2 BGSC2  -- FGSC2 Block3  FGSC3 BGSC3 Block4 - FGSC4  Figure 5.2: Examples of Global Synchronization Cuts event sequence diagram representing the furthest possible progress of the tasks in the system. Furthermore, using the same line of reasoning and from the same point in time, a task may back-track its events until it is limited by some SCE that has already occurred. Thus a line of the maximal regression can also be drawn. The lines will be called Global Synchronization Cuts  (GSC). For simplicity, the GSC of the furthest progress will be denoted as FGSC (Forward GSC), and the GSC of maximal regression will be called BGSC (Backward GSC). Between these two extremes, there are many valid combinations of task states representing possible global states of the distributed system. Note that GSC's are defined in this section only for systems using synchronous communications. At this point, we would like to study the -4  CHAPTER 5. CONCURRENCY MODEL ^  71  relation on events, SCEs, and GSCs. Specifically, the --+ relation on SCEs and GSCs are extensions of Lamport's relation which is defined for asynchronous communication events only. Definition 11 A Concurrent SCE is an SCE that is concurrent with respect to at least one  other SCE in the system. To check if an SCE is concurrent with another SCE, the events that make up the two SCE's can be checked for a concurrency relation using Algorithm 1 or logical clock. Algorithm 2 below shows how the GSCs can be constructed. Notation 4 GSCk = k-th GSC in the system IT1(a),^T2 (1),^T,, (z)}  = (a, ..., 1, ..., z) (i.e. for simplicity, the events in each task are represented by integers, and the position of an integer in the vector denotes the task number). Notation 5 GSCk =^(a), • •^(1), • • •, Tn (4} Ii = {Ti N}  = The notation  "i i " means the projection of GSCk with respect to Ti. As a result, we get the  event number of Ti. These notations apply to both FGSC and BGSC. Notation 6 SET_SCE is the set of SCEs that has been processed so far. Notation 7 MORE_SCE(TO is a boolean function indicating whether T s has more SCEs which  have not been processed.  72  CHAPTER 5. CONCURRENCY MODEL ^  Notation 8 SCE_AFTER_SET_SCEMO is a function returning the next (chronological) SCE event number in T, just after the last SCE event of Ts in SET_SCE. Notation 9 NEXT_EVENT_AFTER_SET_SCE(T8 ) is a function returning the next (chronological) event number in T., following the last SCE event of T., in SET_SCE.  Algorithm 2 (GSC Construction) /* Except for the index variables, all variables in the algorithm are global. The variable k keeps track of the current concurrency block. The events are examined in chronological order in task T i = .1, . n. In particular, the set of SCE 's for each task are assumed to be known (e.g., from its trace). The set of last events are denoted as {Ti (lasts), • • •, T, (last=), ...,Tn (last n )} */  k = 0; FGSCO = (0, • •  0, •• •, 0);  BGSCo = (0, . •  0, •• •, 0);  /* SET_SCE = { the initial set consists of imaginary SCEs from Ti (0) to Ti (0) with j = + I, i = I, ..., n-1 } */ SET_SCE = {SCE (Ti (0),  T2  (0)),  • • • , SCEM  (0), Tj (0)), • • • , SCE(Tn— (0),  draw the BGSCo; ---(1) while (1) do /* the SCEs are examined in chronological order */  Tn (0))};  CHAPTER 5. CONCURRENCY MODEL ^  73  check_S'CEO; if the next SCE(7'p (x),Tq (y)) 0 a Concurrent SCE --(2) then  k = k + 1; add the SCE(Tp (x), Tq (y)) into the set SET_SCE; else  check_SCEO; add the SCE(Tp (x),Tq (y)) into the set SET_SCE; continue; fi for(i = 1; i < n; i++) /* for each task */ --(3) do case  /* for tasks having nonconcurrent SCE selected at (2) */  --  (4)  (i == I)) --+ FGSCicip = {Tp(x)}; BGSCkip = {Tp(4}; (i == q) -4 FGSCkJ q = {Tq (y)}; BGSCkI q = {Tq (y)}; /* for tasks having more SCEs left */ --(5) (i == s) and (i 0 p) and (i 0 q) and (MORE_SCE(T3 ) == true) —4 FGSC/c Is =  {T, (v-1)};  CHAPTER 5. CONCURRENCY MODEL^  with v = SCE_AFTER_SET_SCE(T9 ). BGSCk l, = {T, (v)}; with v = NEXT_EVENT_AFTER_SET_SCE(T 9 ). /* for tasks with no more SCEs left */ --(6) (i == t) and (i 0 p) and (i 0 q) and (MORE_SCE(Tt) == false) —4 FGSCkit = {Tt(lastt)}; BGSCkI t = {Tt(w)}; with w = NEXT_EVENT_AFTER_SET_SCE(Tt ). esac od  draw a FGSCk and a BGSCk; -- (7)  check_SCEO; od  procedure check_SCE0 --(8) /* check whether there are unprocessed SCEs */ for(i=1; i<n; i++) do if( MORE_SCE(Ti) == true)  74  CHAPTER 5. CONCURRENCY MODEL^  75  return;  fi od  /* if there are no more SCEs */ draw FGSCk+i = {716asti), • • ., Ti(lasti), • • ., T„ (last„)}; stop;  Let's apply this algorithm to Figure 5.2 where there is no Concurrent SCE. The algorithm starts by drawing BGSCo. Since there is no Concurrent SCE, the if statement at (2) of the algorithm is always true. The for statement at (3) is used to determine the events for the current  FGSC and BGSC. If there are no SCEs unprocessed as a result of (8), the algorithm draws the last FGSC and terminates. All SCEs that occur between BGSC1 and FGSCi+i (excluding the SCEs that lie on those two lines) for any i are Concurrent SCEs. The Concurrent SCEs provide us with some order information for the events of tasks participating in the Concurrent  SCEs. We call that part of the time event sequence diagram between BGSC and FGSCi+i a concurrency block. Definition 12 A Concurrency Block Bdocki+ i consists of the events between BGSC; and  FGSCi+i including the events on the GSC's. Consider Figure 5.3. There are 4 tasks: A, B, C, and D, with the GSC's obtained using Algorithm 2 shown as dashed lines. In particular, the SCEs between BGSCI and FGSC2 are concurrent SCEs. Therefore, the if statement at (2) of the algorithm is false until SCE(Tc(5),  CHAPTER 5. CONCURRENCY MODEL^  TASK  A  B  C  76  D  BGSCO BGSCI  BGSC2 BGSC3 _ _ . FGSC2 - FGSC3  ^ FGSC4 BGSC4 FGSC5  Figure 5.3: Examples of Global Synchronization Cuts TB(6)) after FGSCi and BGSCI. Even though the events TA (2), TB (3), Tc (3), and TD (2) are concurrent, we have total order in TB(2) TB(3) -p (any event in the set {TB(4), TA(3)}) -4 TA(4). Thus, if Concurrent  SCEs exist, in general we need to check every possible combination of events from each task to determine their concurrent relation. Fortunately, the GSC's divide the time-event sequence diagram into concurrency blocks, and checking needs to be done only on the events in each block, rather than on the entire graph. Since the complexity of checking for concurrency relations increases more than linearly with the number of events, this technique greatly reduces  CHAPTER 5. CONCURRENCY MODEL^  77  the amount of work involved. If there are Concurrent SCEs in a concurrency block, there is some total order in events as illustrated above. The concurrency relation is symmetric, irrefiexive and nontransitive. But it is transitive in the case where each concurrent event belongs to a different task.  Asynchronous Communication Let us suppose that a set of distributed tasks interact with one another using asynchronous communications. We observe that how far the events of a task may proceed may be limited by receive events of other asynchronous communication operations done by tasks which are yet to be executed. Definition 13 A Concurrent ACE is one whose receive event is concurrent to the receive event of at least one other ACE in the system. Algorithm 1 or logical clock technique can be used to check for the presence of a concurrency relationship between the receive events. Algorithm 3 below shows how the GSCs can be constructed for asynchronous systems. Notation 10 SET_ACE is the set of ACE s that have been processed so far. Notation 11 MORE_ACE(7'3 ) is a boolean function indicating whether T s has more ACE receive events which have not been processed. Notation 12 ACE_AFTER_SET_ACE(TO is a function returning the next (chronological) ACE receive event number in T, just after the last ACE event of T, in SET_ACE.  CHAPTER 5. CONCURRENCY MODEL ^  78  TASK A  BGSC I  Time  •  •  • - • .....  BGSC  -  -FGSC 1 — FGSC2 FGSC3 FGSC4  Figure 5.4: Examples of Global Synchronization Cuts Notation 13 NEXT_EVENT_AFTER_SET_ACE(Ts ) is a function returning the next (chronological) event number in T, following the last ACE event of Ts in SET_ACE.  Algorithm 3 (GSC Construction) /* Except for the index variables, all variables in the algorithm are global. The variable k keeps track of the current concurrency block. The events are examined in chronological order in task Ti i = 1,^n. In particular, the set of events of ACE 's for each task are assumed to ,  be known(e.g., from its trace). The set of last events are denoted as {Ti (lasti), ^Ti(lasti), . . . , Tn (1 ast n )} */  CHAPTER 5. CONCURRENCY MODEL ^  k = 0; FGSCo = (0, • • 0, • • 0); BGSC0 = (0, • • 0, • • •, 0); /* SET_ACE = {the initial set consists of imaginary ACEs from Ti (0) to Ti (0) with j = + 1)mod(n+1), i = 1, ^n } */ SET_ACE = {ACE(Ti (0),  T2  (  0  )),  •••,A  CE (Ti (0), Tj (0)), • • A CE(Tn-i (0), Tn (0)),  ACE(Tn (0), T1(0))1; draw the BGSCo; --(1) while (1) do /* the ACES are examined in chronological order */ check_ACEO; if the next ACE(Tp (x), Tq (y)) 0 a Concurrent ACE —(2) then k = k + 1; add the ACE(Tp (x), Tq (y)) into the set SET_ACE; else check_ACEO; add the ACE(Tp (x), Tq (y)) into the set SET_ACE; continue; fi  79  80  CHAPTER 5. CONCURRENCY MODEL^  for(i = 1; i < n; i++) /* for each task */ --(3) do case  /* for tasks having nonconcurrent ACE selected at (2) */  --  (4)  (i == q) -4 FGSCkI q = {;(y-1)}; BGSCkl q = {TqW}; /* for tasks having more ACEs left */ --(5) (i == s) and (i 0 q) and (MORE_ACE(T3 ) == true) —, FGSCkl s = {Ts (v-1)}; with v = ACE_AFTER_SET_ACE(Ts ). BGSCk is = IL Oh ; with v = NEXT_EVENT_AFTER_SET_ACE(T. ^ ). /* for tasks with no more ACEs left */ --(6) (i == w) and (i 0 q) and (MORE_ACE(T t ) == false) --3 FGSCk it = {Tt (lastt)} ; BGSCkIt = {Tt NA ; with w = NEXT_EVENT_AFTER_SET_ACE(Tt). esac od  draw a FGSCk and a BGSCk; --(7)  CHAPTER 5. CONCURRENCY MODEL^  81  check_ACEO; od  procedure check_ACEO --(8) /* check whether there are unprocessed ACEs */ for (i=1; i<n; i++) do if( MORE_ACE(Ti) == true) return; fi od  /* if there are no more ACEs */ draw FGSCk+i = {71 (lash), • • • , Ti (last;), . . ., Tn (lastn)}; stop;  To illustrate, we shall apply this algorithm to Figure 5.4 where there is no Concurrent ACE. The algorithm starts by drawing BGSCo. Since there is no Concurrent ACE, the if statement at (2) of the algorithm is always true. The for statement at (3) determines the events for the current FGSC and BGSC. If there are no ACEs unprocessed as a result of (8), the algorithm draws the last FGSC and terminates. All ACEs that occur between BGSC; and FGSCii-i  CHAPTER 5. CONCURRENCY MODEL ^  82  for any i are Concurrent ACEs. The Concurrent and non-concurrent ACEs provide us with some order information for the events of tasks participating in them. Similar to the case for synchronous communication systems, we will call that part of the time event sequence diagram between BGSCi and FGSC1+i a Concurrency Block as in Definition 12. Events in different concurrency blocks cannot be concurrent with one another. TASK A  C  D  BGSCO  Time  FGSC 1  Figure 5.5: Examples of Global Synchronization Cuts  Consider Figure 5.5. There are 4 tasks: A, B, C, and D, with the GSC's obtained using Algorithm 3. Since every ACE in Figure 5.5 is concurrent, the if statement at (2) of the Algorithm 3 is false. The algorithm is terminated by check_ACE() in the else part of (2) of the  CHAPTER 5. CONCURRENCY MODEL^  83  algorithm by drawing FGSCi at the end of the traces. Even though events are concurrent, we have some total ordering generated by ACEs. Thus, in general we need to check every possible combination of events from each task to determine whether a concurrent relation of Concurrent ACEs exists. More research is needed to devise sub-blocks of Concurrency Blocks. Intuitively, the fact that the Concurrency Block sizes of synchronous communication (Figures 5.2 and 5.3) and asynchronous communication (Figures 5.4 and 5.5) have the same pattern of internal and external events shows that the latter has more possibility for concurrency. This is validated using the concurrency measure described in Section 5.1.4.  Properties from GSC From the informal definition of GSC in Section 5.1.3 and Algorithms 2 (or 3) which implement the GSC, it should be clear that the following properties hold. Property 1 The events in BGSCk + i cannot occur before those in BGSCk for k = 0,1,.... The same is true for the FGSC's. Proof: According to Algorithm 2 (or 3), the SCE's (or ACE's) are examined in chronological order at statement (2). Given BGSCk, BGSCk+i contains at least one nonconcurrent SCE (or ACE) (processed at (4)) whose events must have occurred after the events belonging to the same tasks in BGSCk, even though the events at (5) and (6) could be the same as those in BGSCk. Properties 2 and 3 follow as corollaries.  CHAPTER 5. CONCURRENCY MODEL^  84  Property 2 An event in a concurrency block cannot be concurrent with any event outside the block.  Property 3 If two events are concurrent, they must be in the same concurrency block. The global state of a system at time t consists of an event from each task in the system at time t (i.e., the set of concurrent events, one from each task, at time t). The GSC's are examples of global states. In addition, there are other valid global states within a concurrency block. Definition 14 For each concurrency block Blocki, the Valid Global States are the set of concurrent events {Ti(k), ..., Ti (s) , . . ., Tn (z)} such that Ti(k), ..., Ti(s), ..., Tn (z) E B1 ocki , and each event belongs to a different task Ti, j=1, ..., n. If an SCE is included in a global state, the two matching events that make up the SCE must be parts of the global state at the same time. But two events consisting of an ACE can not be global states at the same time. Definition 15 Data races occur if concurrent events have read/write or write/write access conflicts to shared variables. The following examples taken from Figure 5.3 would indicate data races occurring in Blocks with respect to a variable X:  • Example 1: Tc (1) is read X and Td(1) is write X. • Example 2: 7 c (1) is write X and Td(1) is read X. 1  CHAPTER 5. CONCURRENCY MODEL ^  85  • Example 3: Tc (1) is write X and Td(1) is write X.  Depending on the order of events in the above examples, the value of X and the outcome of the subsequent events that reference X are different. In other words, data races produce unintended nondeterminism. 5.1.4 Concurrency Measures Now we turn to concurrency measures. Based on the logical clock concept [Fidge 91, Matte 89] for characterizing concurrency relations, two concurrency measures, w and m, are proposed for distributed systems [Charro 89]: Definition 16 w=  a2^a2 + + a n or m = an  —  where  ak: the number of k-antichains 6 in the system. 4: the number of k-antichains if all the tasks were completely concurrent. w and m are in the range [0,1], with 0 representing sequential computations and 1 denoting completely concurrent computations. The measures are based on the principle [Charro 89] that the less the events of one process block progress of other processes, the more concurrent is the computation. The use of a logical clock in computing the antichain relations in the entire trace requires B A k-antichain in combinatorial theory is analogous to our Valid Global States in Definition 14 for a system with k tasks. The k-antichain of a trace is a subset of the trace in which k events from n different tasks(k < n) are incomparable or concurrent.  CHAPTER 5. CONCURRENCY MODEL^  86  substantial processing power. In contrast, our method for synchronous communication systems does not need logical clocks and it defines a block structure restricting the number of events which may be concurrent. The trace is divided into blocks which contain concurrent events. An event cannot be concurrent with another event outside the block. This minimizes the work needed to check an antichain relation and also makes Algorithm 1 efficient. As extensions of w and 7n, we propose W and M as concurrency measures for synchronous or asynchronous distributed systems based on concurrency blocks. Definition 17 Concurrency measures of synchronous or asynchronous distributed systems are El (^I ,Brocki) W = ^a2  TN I f I  !Bloc) =1 ka2 !Block +... + a, ^k or M = ELi (a2 IBlocki)^Ei=1(a2 'Block; + • • • + 4 IBlocki)  where n is the number of tasks, 1 is the number of concurrency blocks, and a n 1Block i and  an IBlocki  are respectively the a n and acn of Block;.  Like w and m, W and M are in the range [0,1]. In order to compare the efficiency of computing W and M with that of w and m, the work can be divided into two parts: determining whether two events are concurrent and finding events having an antichain relationship. For w and 7n, concurrency checking requires labelling events using logical clocks and comparing all event pairs whereas for W and M the work is that described in Algorithm 1. It is hard to quantify but we believe Algorithm 1 requires less work because of its block structure. For antichain computation, w and m require events in the entire trace to be examined whereas W and M look at events in each concurrency block only. Some indications of the savings in computation are illustrated by the following examples. Let us assume, for simplicity, that the  87  CHAPTER 5. CONCURRENCY MODEL^  concurrency blocks do not overlap and the trace is equally divided into blocks each of which contains at least one SCE in synchronous communication. Also, to simplify the computation, we will assume the two events that make up an SCE have no effect in the order of the events in the two tasks involved in the SCE. The error introduced by this assumption is small if the number of SCE's is small compared with the total number of events in the system. For n number of tasks each with e events equally divided into b blocks, the ratio Rk of W over w (or for M over m) with respect to the number of event pairs that need to be compared in order to obtain the k-antichain relation is:  bxNx  (ril +  )  k^  n!  Rk =^where N is Binomial[n,k] = k1 N x (e +1)^ k1 k.(n — k)!'  bx  (ril +1)k  (e + 1)k^•  For an example of 3 tasks each with 9 events divided into 3 blocks, the ratio R2 for the 2antichain is: 7.,  3x  48 _ 100  (131 + 1) 2  it2=-(9 + 1) 2  The larger the value of k, the larger the savings. For example, the ratio R3 for the 3-antichain in the above example is: 83_ 3  x (1 1 1 +1 ) 3^192 (9 + 1) 3^‘= 1000  Furthermore, if a block does not contain concurrent SCEs, it is not necessary to determine if the events in the block are concurrent as all the events in the block are concurrent. In this case,  CHAPTER 5. CONCURRENCY MODEL^  88  the value of R2 is the same as the concurrency measure W. Thus, the concurrency measures can be obtained trivially. This characteristic does not apply to w and m and makes our technique even more efficient and elegant. As an example, let's compute R3 for the synchronous system in Figure 5.2: Blocky^SCE(TC(2),TB(2))^Blocks^SCE(T4(3),TB(4))^Block3^SCE(Tc(5),TB(6))^Block4 ...,....."....,^,...."...,^,„......"■,,^,..."...,^,,,....■"......,^,.......,^,,,,■"■..,„ R3 =  3 x 2 x 2 +^3 x 1^+ 3 x 2 x 3+^1 x 3^+ 3 x 2 x 3+^1 x 3^+3 x 2 x 2 6x8x7  69 = 336' Also, R3 for the asynchronous system in Figure 5.4: Bz.ch i^Blo o k2^Block3^  Bio.k4  R 3 —^ _ 6 x 2 x 7+6 x 2 x 5+3 x 3x 5+3x 3 x 2 6)(8x7  207 = 336' The R3 for the asynchronous system is greater than that for the synchronous system. Therefore, we validated the intuition at the end of Section 5.1.3 that an asynchronous system has more possibility for concurrency than a synchronous one. Another approach of concurrency measures is to determine the critical path of a concurrent specification using the concurrency measure [Rayna 91] with respect to computing delay. The specification can be redesigned to minimize the the computing delay and the idle time. This method is designed for static analysis with integer counters but can be extended to dynamic analysis with floating point number counters. When the computing delay of each operation is known, total system performance can be estimated using simulation.  CHAPTER 5. CONCURRENCY MODEL^  89  5.2 Application to Estelle Specifications The semantics of Estelle [Dembi 89, ISOc] allows two waiting relations - message receive and task release. The type of asynchronous communication deadlocks possible in Estelle is similar to that shown in Figure 5.6(b). This is the first condition presented in Definition 10 where the matching send event is missing. A minor difference is that the ACE event rather than the receive operation is blocked.  TASK A Time  B  A  1  Blocked Operation l  i  (a)  (b)  (c)  Figure 5.6: Types of Deadlocks  The other type comes from the dynamic behavior of Estelle. This case has the same outcome as case (b) of Figure 5.6. The 'X' (termination of operation) in case (c) of Figure 5.6 is a result of the release primitive of Estelle. The release terminates the child task C. The termination may prevent the sending of an expected message. Reordering the release and sending message normal task termination. In Estelle, variables can be shared between a module and its parent module by declaring them to be exported variables. This is the only way variables may be shared. The parent/child priority principle prevents modules from accessing the shared variables simultaneously because the parent always has priority. This principle in effect prevents data races. The order of actions between parent and children is determined and serialized. The concept is similar to  CHAPTER 5. CONCURRENCY MODEL ^  90  that proposed by Lamport [Lampo 78] which serializes events according to process identifiers (priority). We can use W or M of Definition 17 as concurrency measures. More research is needed to analyze asynchronous communication inside Concurrency Blocks to minimize the number of candidate events which are supposed to be concurrent and to enumerate the events which are supposed to be in the antichain relation.  5.3 Application to LOTOS Specifications According to the semantics of LOTOS [Bolog 87, ISOd], there are two waiting relations message send and message receive. The kinds of synchronous communication deadlocks possible in LOTOS are depicted in Figure 5.6 (a) and (b) corresponding to condition 1 of Definition 10, and circular waits corresponding to condition 2 of Definition 10. LOTOS requires type matching between message send and receive at the same gate. If type matching is not satisfied, the SCE does not occur. The matching can take the forms of value to value, value to typed variable, and typed variable to typed variable as shown in [Logri 88]. Data races cannot occur since LOTOS does not support shared variables. The degree of concurrency can be measured using W or M of Definition 17.  5.4 Application to Ada Programs The Ada standards [Ada 83] define shared variables in terms of five types of synchronization between tasks. The five types of synchronization occur at the start and the end of synchronous communication, the start and the end of a new task's activation, and the completion of a task.  CHAPTER 5. CONCURRENCY MODEL^  91  The first two types of synchronization are associated with task communications called rendezvous. This is semantically equivalent to our definition of synchronous communication event (SCE) (Definition 9) and therefore our concurrency model can be used to identify concurrency blocks in Ada programs based on rendezvous. We apply the concurrency model for synchronous communications to an Ada program (See Appendix E for program listing). By applying Algorithm 2 in Section 5.1.3, we see dataraces are possible in this program. Specifically, the two events executing "v := v + 1;" in each of the concurrency blocks are concurrent. Therefore, the value of the variable "v" depends on the order of task execution and cannot be determined from the program code before execution. The degree of concurrency can be measured using W or M of Definition 17.  5.5 Chapter Summary As a step to investigating the trace analysis in a concurrent environment, we have presented a model to transform the concurrency-checking problem into the path-detection problem in graph theory. This method is general enough to be used for both synchronous and asynchronous communications. The concept of Global Synchronization Cuts is presented to provide an elegant model for defining concurrency blocks, global states and concurrency measures. This model allows high-level abstractions to be used for understanding concurrent behaviors of formal protocol specifications written in languages such as Estelle and LOTOS. The model is also applicable to any high-level concurrent languages such as Ada, Modula II and Occam which use synchronous or asynchronous message passing and/or shared variables as communication  CHAPTER 5. CONCURRENCY MODEL^  92  mechanisms. Furthermore, based on the model, we have proposed concurrency measures W and M for programming systems that support synchronous or asynchronous communications. These measures are extensions of w and m but can be computed much more efficiently.  Chapter 6  Trace Analysis based on Concurrent Specifications Two important aspects of protocol testing are test case generation and trace analysis. Up until now, they have been studied in a sequential context even though the specifications are concurrent. Most work on automatic test case generation and trace analysis with respect to  Estelle specifications assumes a preprocessing stage to translate multiple modules into a single module in order to obtain a specification in terms of sequential behaviors [Sarik 86]. In this chapter, we propose a model for performing trace analysis based on concurrent specifications. Recall the specifications are based on multi-module extended finite state machines. The model consists of three basic building blocks:  1. Trace analysis with respect to a single module of formal specification: this allows us to determine whether a given trace is a permissible behavior of a protocol. 2. Concurrency model: this model deals with concurrent properties such as deadlocks and data races which do not arise in sequential specifications.  93  CHAPTER 6. TRACE ANALYSIS BASED ON CONCURRENT SPECIFICATIONS 94  3. Traceability: this concept is needed to obtain a precise order on input/output messages of a module while avoiding a state space explosion when applying the first basic building block to modules having multiple ports.  In this chapter, we will adopt the scheduler-independent observation principle [Taylo 92, Araka 91], but not the single stimulation principle [Araka 91] since operations of distributed environments are generally executed in parallel. In this work, our model of concurrent trace analysis can be applied to the problem of debugging concurrent programs [Mcdow 89] as well.  6.1 The Basic Blocks The basic idea of our model is summarized as follows. A concurrent specification can be considered to be a set of single-module specifications that interact with one another (see Section 6.2). Traceability (see Section 6.1.3) of the implementation of each single-module specification allows a precise ordering on input/output messages of the implementation (see (a) of Figure 6.1).  The input/output messages, or traces, of each module are checked for conformance to the single-module specifications (see Section 6.1.1, Chapter 3 and Chapter 4). At this stage, we can infer the internal events of tasks based on the single-module specifications (see (b) of Figure 6.1). During the trace analysis process, non-conformance due to a missing or mismatched output message in the trace could indicate deadlock. This will be detected by the concurrency  CHAPTER 6. TRACE ANALYSIS BASED ON CONCURRENT SPECIFICATIONS 95  TASK A^B^C^A^B -  0  0  1e  *** .. ..  \t1^ ^ (C) (a)^ (b)  Figure 6.1: Basic Blocks model. The set of traces associated with multiple single-modules allows the construction of a time-event sequence diagram which is needed for analysis using the concurrency model (see Section 6.1.2 and Chapter 5). The concurrency model provides a method to detect deadlocks and data races (see (c) of Figure 6.1).  6.1.1 Trace Analysis based on Single-Module Specifications Generally speaking, the trace analysis model shown in Chapter 3 and Chapter 4 deals with a single module as a black box with two interaction ports: one at the upper-interface and the other at the lower-interface (see (a) of Figure 6.2).  IUT  (a)  ^  (b)  ^  (c)  Figure 6.2: Points of Observation  The trace analyzer determines if a given trace conforms to the Estelle specification of the  CHAPTER 6. TRACE ANALYSIS BASED ON CONCURRENT SPECIFICATIONS 96  protocol. If not, it logs a history of the activities as well as values of variables to help locate the source of errors.  6.1.2 Concurrency Model In summary, the model presented in Chapter 5 deals with trace analysis of a set of tasks communicating with each other. Each task can be considered as a module treated as a white box. The model allows us to determine the happened before relation among message sends and receives between the modules, since the internal details are known (white box assumption). If the modules are treated like black boxes, then we may need to enumerate every possible combination of message sends and receives. This enumeration may cause state space explosion. In order to solve this problem, traceability as discussed in the next section is proposed.  6.1.3 Traceability In the hardware area, especially chip testing, testability research is mature and various techniques have been standardized. Some chips have been built following the standards. These chips can be tested more easily, precisely and in a cost-effective manner using standard techniques through Test Access Ports [Parke 89]. This approach will be called grey box testing, and falls somewhere between white box and black box testing. It is clear that the aims of both hardware and software testability are similar: avoiding or minimizing state space explosion in order to reduce the time and cost of testing. However, there are major differences between software and hardware with respect to the testing process [Hoffm 89]. The differences are mainly due to the fact that the purpose of hardware testing  CHAPTER 6. TRACE ANALYSIS BASED ON CONCURRENT SPECIFICATIONS 97  is to determine whether an implementation (chip) is an accurate copy of the circuit design, since the correctness of the circuit design has been established in an earlier verification process. Implementations originating from the same proven valid design may still contain serious errors introduced in the manufacturing phase. On the other hand, for software, once an implementation is proven correct by testing, copies of the same implementation are always correct. In addition, hardware consisting of distributed circuits or boards often has a single physical global clock, but this is almost impossible for software running in a distributed system. Current research in software testability can be divided into two main areas - intra-module and inter-module. Since we can infer the internal activity using the first basic block of our model if the order of input/output messages is known, we deal only with testability on intermodules here. We use the term traceability to mean testability from the viewpoint of trace analysis. In other words, we are concerned with observation rather than control. A new direction of research concentrates on the design of testable protocols, that is, protocol designs whose implementations are easier to test [Dssou 90]. The idea is to follow certain guidelines in the software design stage so that any implementation of this design can be more easily tested. Design decomposition and modularity and increased observability through trace collection provide the basis of the method [Dssou 90]. The finer the degree of decomposition, the more efficient will be the localization. However it may not be realistic to keep the modular structures in the implementation. Also, the order of messages obtained from the Points of Observation (PO) and/or the Points of Control and Observation (PCO) between modules as shown in Figure 6.2 (b) does not always correspond to the order of actual occurrences inside the  CHAPTER 6. TRACE ANALYSIS BASED ON CONCURRENT SPECIFICATIONS 98  IUT. For example, consider two input messages where the input message at port 1 arrives at the IUT earlier than the input message at port 2. The messages may be executed in the reverse order of the arrival. In order to determine the right order, we may need to enumerate every possible combination of message inputs and outputs. This may cause state space explosion in the trace analysis. Our solution is to insert additional output statements with a message identifying the specific transition. These are placed after each output statement of every transition in the original  Estelle specification. For each module, these trace output statements are directed to a special port created for the purpose of tracing (which shall be called the Port of Observation for Traceability (POT)) where a log of the trace will be recorded (see Figure 6.2 (c)). The POT gives us a precise order of message input/output independent of the number of interaction ports in the module. This instrumentation can be done easily without modifying the Estelle compiler or semantics. Also, we can define some convention to turn off the output mechanisms if the performance of the implementation is critical. If an IUT is implemented according to the  Estelle specification which was instrumented for traceability as described above, the correct order of input/output sequences can be obtained. From the order, one transition out of a set of possible transitions conforming to the trace (if it exists) can be identified. In this way, nondeterministic transitions can be handled more efficiently. This approach introduces the minimum number of changes to the original specifications. As a reference, [Saleh 92] used four operations - probe, trace, restart(reset) and set in. Our proposal consists of getting the trace from the POT of each module and the current state information if available. The current  CHAPTER 6. TRACE ANALYSIS BASED ON CONCURRENT SPECIFICATIONS 99  state information is helpful in minimizing the state space when we are exploring the formal specification as shown in Section 6.1.1, Chapter 3 and Chapter 4.  6.2 Formal Model In this section, a module means an implementation executing as a single process. Let us assume that a concurrent module M,„„, consists of a set of sequential modules MI, , Mi, ... , Mn ; a concurrent formal specification Sconc consists of a set of sequential formal specifications Sl , , Si,...,S„; and, a concurrent trace T., from consists of a set of sequential traces  ... , Ti, , Tn from individual modules MI, , Mi, , Mn , respectively. The concurrent formal specification S., is assumed to be error-free and conform to the standards. As a result of this assumption, the communication events between the sequential formal specifications of Sconc will not have deadlocks.  Definition 18 The sequential trace Ti of module Mi consists of a chronologically ordered set of event vectors t lf, k = 1, 2, .... If Mi has p interaction ports, then the event vector = <^outlfa), . ,(in ifp ,out4)> where in ky and outs are the input and output messages respectively at interaction port j associated with the k-th event vector in trace Ti. ins and outs may be null. Notice that we have a trace structure equivalent to the ones presented in Section 3.3 and 3.4. Recall those trace structures dealt with trace analysis based on single modules of formal specification. Therefore, an event vector consists of zero or one input, and i output messages where 0 < i < p.  CHAPTER 6. TRACE ANALYSIS BASED ON CONCURRENT SPECIFICATIONS 100  •• •  S  ••  Tn  •  •  TI  •• •  MI  A  ••  •  TI  Si  •  ••  ••  ScAonc  Tconc  Mi  Mconc  Mn  Figure 6.3: Trace Analysis based on Concurrent Specifications  Definition 19 A sequential module Mi is pointwise conformant to the formal specification Si on an event vector d if the behavior of the event vector is permissible in the specification. This is denoted as pconf(Mi, Si t lf). ,  Note that even if more than one path (or transition) of the specification satisfies the event vector, the pconf relation still holds based on the above definition.  Definition 20 A trace Ti conforms to the sequential module M1, written as conf,  eq  (Mi, Si,  Ti) if pconf(Mi, Si, t lf) for all d in Ti. The sequential trace Ti from Definition 18 consists of the external behaviors of a module Mi with respect to its environment (i.e., the other modules). If cortf„ q (Mi, Si, Ti) is valid, the trace Ti conforms to the specification of Mi. In addition, the input/output messages to/from the other modules in Ti are also valid since we assume that Sc,,„ c is error-free.  CHAPTER 6. TRACE ANALYSIS BASED ON CONCURRENT SPECIFICATIONS 101  Definition 21 A concurrent trace Tic of a concurrent module Mac conforms to the concurrent specification Scan , of Mconc , written as con fconc (ldconc , Sconc , Teonc ) if conh eq (Mi , S1, T1) A • • • A amf,"(Mi, Si ., Ti) A • . • A confseq (Mn , Sn ,Tn ), i.e., A i _ i confseq (Mi, Si, Ti). Note that the trace analysis proposed does not depend on the communication scheme (synchronous or asynchronous). The trace analysis of concurrent modules with respect to concurrent formal specifications provides verdicts based on a set of trace analyses of single modules with sequential formal specifications. Since the two unique types of errors that could arise in concurrent (or distributed) environments are deadlocks and data races, we need to show how they can be detected in the concurrent model. To detect data races, we note that a set of con f seq (Mi, S i,Ti) - trace analyses with respect to single module - allows the construction of the time-event sequence diagram which is used by the concurrency model (see Section 6.1.2 and Chapter 5). The concurrency model provides a way to detect data races as shown in Section 5.2 and Appendix E. Deadlock detection will be illustrated in Section 6.4.  6.3 Applications We begin by discussing the application of our model of trace analysis based on concurrent specifications in a general context where a set of modules (IUTs) are interacting with one another. In this general setting, the configuration of the modules is not taken into consideration; the modules may be implemented on the same machine or on different machines. We then show how  CHAPTER 6. TRACE ANALYSIS BASED ON CONCURRENT SPECIFICATIONS 102  the model can be used in specific applications such as multi-party testing and interoperability testing.  6.3.1 Trace Analysis based on Multi module Specifications -  In order to check certain properties for a set of concurrent programs, the relative order of interactions occurring at different ports as well as the order of operations occurring at each of the modules must be determined. This is a difficult problem in distributed systems. In order to construct an order of observed and unobserved (i.e. internal) events, our model consists of two parts. The first obtains the order of interactions between modules from the trace using the method given in Section 6.1.3. The second obtains the order of operations within each module from the trace using the method given in Section 6.1.1. We can determine the interaction order of input and output messages at each module from the POT independent of the number of interaction ports. Based on the formal model in Section 6.2, trace analysis of concurrent specifications could be considered as a set of trace analyses on the individual modules with the POT depicted as in Figure 6.4.  There are two kinds of POs: one, which is supported by the OSI architecture, will be called  OSI POs and the other, supported by our model, will be called POTs. The OSI POs have been used for the black box testing on which conformance testing is based. In testability terms, we can say that the OSI architecture was built with POs (or PCOs) provided between the protocol layers only. No POs (or PCOs) exist within the individual layers. In our model, we can get the exact order of interactions among modules using the concept of POT as described  CHAPTER 6. TRACE ANALYSIS BASED ON CONCURRENT SPECIFICATIONS 103  POT  OSI Layer N POT^ POT POT  Figure 6.4: Application in Section 6.1.3, and the order of operations inside a module using the trace analysis technique discussed in Section 6.1.1 and Chapter 3. Deadlocks can be detected by the method presented in Section 6.4 and Chapter 5. The concurrency model in Section 6.1.2 allows data races between modules to be detected. The block structure of events which contains possible concurrent events allows data races to be checked easily for systems or languages using synchronous or asynchronous communications.  6.3.2 Message Collisions in Multiple Party and Interoperability Testings The need for multi-party testing arises in the situation where an action (or an instance of communication) of the protocol entity to be tested causes subsequent actions at other protocol entities. Examples can be found in Message Handling System, Routing Protocol, Integrated Services Digital Network, Distributed Transaction Processing and Directory Services. In this situation, the results of these actions may only be observed and reported by third parties. Hence, the requirement of testing such a protocol suggests the need for a test method which may involve multiple peer entities distributed among several systems, each communicating with  CHAPTER 6. TRACE ANALYSIS BASED ON CONCURRENT SPECIFICATIONS 104  the IUT through a unique association or connection. Testing OS/ protocol implementations before deployment to production fields provides a measure of confidence in their correctness. A protocol implementation is said to conform to the relevant standards if conformance testing yields a positive verdict. This, however, does not necessarily guarantee it is able to interwork properly when deployed as part of a complete working system. Therefore, interoperability testing is needed in order to verify the end-to-end behavior of protocol implementations in their working environment. As shown in the Ferry Clip approach for multi-party and interoperability testing [Chans 92], the IUTs can be located at physically different sites. One of the difficulties of trace analysis in the distributed environment is checking for the message collision phenomenon [Probe 92]. Probert et al. [Probe 92] used the logical clock by [Fidge 91] to model global events in a distributed system. In fact, these applications are natural extensions of the general problem described in the previous section. A message collision is said to have occurred when a message send event and a message receive event between modules occur concurrently. This can be detected using Procedure 2 and Algorithm 1 in Section 5.1.2 on events participating in the message sends/receives. If such an event happens in asynchronous communication, it is a message collision. If it occurs in synchronous communication, it is a deadlock. The trace analysis techniques discussed in Section 6.1.1, Chapter 3 and Chapter 4 should be able to handle message collision. Our prototype implementation [Kim 91] using Estelle (which supports asynchronous communication) shows that message (in this case, frame) collision problems are correctly analyzed.  CHAPTER 6. TRACE ANALYSIS BASED ON CONCURRENT SPECIFICATIONS 105  6.4 Case Study The Five Philosopher's Dining Problem is a traditional example of concurrent systems which requires synchronization among the processes according to some protocol. The five philosophers spend their lives eating or thinking. Each philosopher has his own place at a round table. Only five forks are provided, one between each pair of philosophers. The philosophers can only pick up the forks on their immediate left or right. The food is at the center of the table, and two forks are needed to eat the food. Here we modify the problem description to avoid deadlocks and indefinite postponement (i.e., livelock). When a philosopher is hungry, he goes to the dining room and sits down at his own fixed position. After eating, he leaves the room and continues to think. The model includes a manager to monitor the five philosophers. Each philosopher has to apply to the manager to enter the dining room. Only when he gets the permission can he enter or leave the dining room.  Manager M2  T2 Lp2 Rp2 LI RI Forkl  Phil2  Figure 6.5: Module Structure  Figure 6.5 shows a part of the module structure of the problem and Appendix H contains  CHAPTER 6. TRACE ANALYSIS BASED ON CONCURRENT SPECIFICATIONS 106  a part of the Estelle description of module instances "Phil2", "Forkl" and "Fork2". In the figure, symbols T2, Li, Ri, Lpi and Rpi (where i is 1 or 2), are the interaction points between module instances.  After the following traces:  t Phil2 =^ (°k Phil2,T21 Cb) , (01 P iCk PhiI2,Lp2) , ( 0 0) > and tForkl =<^f ork_providecliF orkl ,R1) 7 07 4) (  )  let's say that we have the following traces from each module:  t Phil2 =< (0, 0), (f ork_provide4 hii2,42 61 7 iCk e- hil2,Rp2) > and • • •(6• ^2rs t 2Fork2 =< (ick F 2 ork2,L2 , 0) , (0 , 0) >•  Trace tPhil2 shows that "Phil2" sent a message "pick" to the left fork of "Phil2" - "Forkl" - through interaction point "Lp2" after the manager allowed "Phil2" into the room to eat using the input message "ok" through interaction point "T2". "Forkl" responded with a "fork_ provided" to the input message from "Phil2" as indicated in t F l orki . The trace t 2pk i1 2 shows that "Phil2" sent a "pick" message to its right fork, namely "Fork2", through interaction point "Rp2" after receiving the message "fork_provided" from "Forkl". Now, if the system functions correctly, trace ti, ork2 should be similar to t Fl orki . However, the trace from MFork2  (i.e., 4, 042 ) shows that the output message "fork_provided" through L2 is missing. Therefore, the trace t 2Fork2 from MFork2 does not conform to the specification S F ork2. As a result of  CHAPTER 6. TRACE ANALYSIS BASED ON CONCURRENT SPECIFICATIONS 107  this non-conformance, "Phil2" is blocked waiting for the "fork_provided" message from M F ork2 •  Suppose in the above trace, 4, 042 is replaced by the following: 40,42 =< (iCk2F ork2,L21 no or k F ork2 ,L2) 7 (0)  0)  •  The output message "no_fork" from module Fork2 does not conform to the formal specification since there is no transition in the formal specification of "Phil2" satisfying the message "no_fork". Furthermore, the system is deadlocked as a result of the fact that the "fork provided" message from  or k2 MFork2  will never come.  A third type of error occurs when the message sent conforms to the specification of the receiver module but not that of the sender module. In this case, there is no blocking or deadlock but the sender module is incorrectly implemented nevertheless.  6.5 Chapter Summary Until now most work on trace analysis based on formal specifications has been studied in a sequential context, even though the specifications are concurrent. In this chapter, we have presented an approach to perform trace analysis of concurrent specifications without translating them into their equivalent sequential specification. The concurrency model and the concept of traceability through the use of Port of Observation for Traceability (POT) and output statements were introduced. The case study of a concurrent protocol based on the Five Philosophers' Dining Problem was used as an illustration. Applications to multi-party and interoperability  CHAPTER 6. TRACE ANALYSIS BASED ON CONCURRENT SPECIFICATIONS 108  testings were also briefly discussed.  Chapter 7  Conclusions and Future Research We conclude this thesis by summarizing the major results and listing some future research.  7.1 Summary of Results This thesis has four parts: The first part describes trace analysis with respect to a single-module specification based on extended finite state machines. The second part describes a prototype implementation of the first part. The third part presents concurrency models to describe and deal with concurrent properties; and the fourth part examines the trace analysis of concurrent specifications based on multi-module extended finite state machines. Protocol Trace Analysis based on Single-Module Specifications We have presented a unified model to perform trace analysis and test case generation using single-module Estelle specifications. Indeed, since the model is based on single-module extended finite state machines, it will work with any specifications that can be translated into extended finite state machine representations. In order to avoid transition explosion as a result of normalization of Estelle specifications, we include conditional statements and introduce  109  CHAPTER 7. CONCLUSIONS AND FUTURE RESEARCH^  110  symbolic evaluation to detect and discard infeasible paths. Some practical issues such as trace analysis using an external test architecture were also discussed. The technique was illustrated using X.25 LAPB to show that it can handle some of the difficult problems, such as frame collisions and data flow, rigorously. We have also shown the relationship between trace analysis and test case generation, and briefly discussed how our framework could be extended to include test case generation and validation. Using our model, we implemented a prototype trace analyzer based on Estelle specifications. It can handle both control and data flows of Estelle specifications with respect to traces or test cases. In addition, the tool can be used to debug  Estelle specifications with respect to traces or test cases. Concurrency Model In order to extend trace analysis to the concurrent environment, we introduced a concurrency model. The model transforms the concurrency-checking problem into a path-detection problem in graph theory. This method is general enough to be used for both synchronous and asynchronous communications. The concept of Global Synchronization Cuts is presented to provide an elegant model for defining concurrency blocks, global states and concurrency measures. This model allows high-level abstractions to be used for understanding and analyzing concurrent behaviors in formal description techniques for protocols such as Estelle and  LOTOS. The model is also applicable to languages such as Ada, Modulo II and Occam which use synchronous or asynchronous message passing and/or shared variables as communication mechanisms.  CHAPTER 7. CONCLUSIONS AND FUTURE RESEARCH^  111  Furthermore, based on the model, we have proposed concurrency measures W and M for programming systems that support synchronous or asynchronous communications. These measures are extensions of w and m which can be computed much more efficiently. Trace Analysis based on Concurrent Specifications As an approach to investigate the trace analysis of concurrent specifications without translation into the equivalent sequential specification, we have proposed a model consisting of three basic building blocks: trace analysis with respect to a single-module extended finite state machine, concurrency model, and traceability. This model is formalized and proposed to apply to multi-module specifications, multi-party testing and interoperability testing. A case study of the model on the five philosopher's dining problem was also presented.  7.2 Future Research There are a number of areas in which future research may lead to useful results:  • In order to facilitate trace analysis with respect to concurrent specifications using our approach, the following work would be useful: — how to implement the Point of Observation for Traceability given in the specification in a systematic (or a standard) way, — how to augment OUTPUT statements for a subset of the transitions instead of for all transitions in order to improve performance without loosing information on the precise order of input/output messages,  CHAPTER 7. CONCLUSIONS AND FUTURE RESEARCH^  112  — how to automate the translation phase from Estelle specifications to Estelle.Y and  ASN.1 specifications, and — how to merge trace analysis of concurrent systems with testers (e.g. Ferry Clip Approach [Chans 92]). • In order to make the trace analyzer simple and efficient, we have assumed that the initial state is known. Even though in practice this can be achieved by waiting for an idle period, it would be interesting to see if the initial state assumption can be removed. • The trace analyzer can be built based on a symbolic simulator using Binary Decision Diagrams [Burch 92]. This technique is popular for hardware verification and is worth investigating for application in trace analysis. • For improved performance, it would be useful to investigate building the trace analyzer on a multiprocessor system (e.g., Transputers) [Mohr 92]. • An investigation of the use of the trace analyzer in distributed program debugging systems would be informative.  Bibliography [Abadi 90] Martin Abadi and Leslie Lamport, Composing Specifications, DEC SRC Report 66, Oct. 1990. [Ada 83] Reference Manual for the Ada Programming Language, U.S. Dept. of Defence, U.S. Government Printing Office, ANSI/MIL-STD-1815A edition, Jan. 1983. [Araka 91] Noriyasu Arakawa and Terunao Soncoka, A Test Case Generation Method for Concurrent Programs, The 4th Int'l Workshop on Protocol Testing Systems, 1991. [Bochm 89] Gregor v. Bochmann, Rachida Dssouli, and et al, Trace Analysis for Conformance and Arbitration Testing, IEEE Tr. on Software Engineering, pp. 1347 - 1356, November 1989. [Bochm 90] Gregor v. Bochmann, D. Desbiens, and et al, Test Result Analysis and Validation of Test Verdicts, 3rd Intl Workshop on Protocol Test Systems, October 1990. [Bolog 87] Tommaso Bolognesi and Ed Brinksma, Introduction to the ISO Specification Language LOTOS, Computer Networks and ISDN Systems 14, pp. 25 - 59, 1987. [Bosik 91] Barry S. Bosik and M. limit Uyar, Finite State Machine based Formal Methods in Protocol Conformance Testing: from Theory to Implementation, Computer Networks and ISDN Systems 22, pp. 7-33, 1991. [Bryan 89] Doug Bryan, An Algebraic Specification of the Partial Orders Generated by Concurrent Ada Computations, Proceedings of TR1-ADA '89, pp. 225 - 241, Oct. 1989. [Burch 92] J. R. Burch, E. M. Clarke and et al., Symbolic model checking: 10 20 states and beyond, Information and Computation, p 142-170, June 1992. [CCITT 88] CCITT, CCITT Specification and Description Language (SDL) Recommendations Z.100, CCITT Blue Book, 1988. [Chans 89] S. T. Chanson, B. P. Lee, and et al, Design and Implementation of a Ferry Clip Test System, The Ninth Intl Symposium on Protocol Specification, Testing, and Verification, June 1989.  113  BIBLIOGRAPHY^  114  [Chans 91] S. Chanson and J. Lo, Open Systems Interconnection Passive Monitor OSI-PM, The Intl Workshop on Protocol Test Systems, pp. 423 - 442, 1991. [Chans 92] Samuel T. Chanson, Son T. Vuong and et al, On Multi-party and Interoperability Testing using the Ferry Clip Approach, Computer Communications, pp. 153 - 168, April 1992. [Charro 89] Bernadette Charron-Bost, Combinatorics and Geometry of Consistent Cuts: Applications to Concurrency Theory, The 3rd International Workshop of Distributed Algorithms, LNCS 392, Springer-Verlag, pp. 45 - 56, Sept. 1989. [Charro 91] B. Charron-Bost, F. Mattern, and et al., Synchronous and Asynchronous Communication in Distributed Computations, LITP Research Report 91-55, 1991. [Cheng 90] Jingde Cheng, A Classification of Tasking Deadlocks, ACM Ada Letters, pp. 110 127, May/June 1990. [Choi 91] Jong-Deok Choi and Sang Lyul Min, RACE FRONTIER: Reproducing Data Races in Parallel-Program Debugging, The Third ACM SIGPLAN Symposium on Principles & Practice of Parallel Programming, pp. 145 - 154, Apr. 1991. [Chun 90] Woojik Chun and Paul D. Amer, Test Case Generation for Protocols Specified in Estelle, The Third Intl Conference on Formal Description Techniques, pp. 197 - 209, 1990. [Clark 87] E. M. Clarke and 0. Grumberg, Research on Automatic Verification of Finite-State Concurrent Systems, Annual Review Computer Science, pp. 269 - 290, 1987. [Clark 85] L. A. Clarke and D. J. Richardson, Application of Symbolic Evaluation Methods, The Journal of Systems and Software 5, pp. 15 - 35, 1985. [Das 79] Sunil R. Das, C. L. Sheng and et al, Transition Matrices in the Measurement and Control of Synchronous Sequential Machines, Information Sciences 18, pp. 47 - 65, 1979. [Dembi 89] P. Dembinski and S. Budkowski, Specification Language Estelle, The Formal Description Technique Estelle, Elsevier Science Publishers B.V.(North-Holland) pp. 335 - 74, 1989. [Dssou 90] Rachida Dssouli and Reine Fournier, Communication Software Testability, The 3rd Intl Workshop on Protocol Testing Systems, 1990. [Dssou 91] Rachida Dssouli, Reine Fournier and et al., Distributed Observation and FIFO Queues, Third Intl Conference on Formal Description Techniques, pp. 303 - 310, 1991.  BIBLIOGRAPHY^  115  [Ehrig 85] H. Ehrig and B. Mahr, Fundamentals of Algebraic Specification 1, Springer-Verlag, Berlin, 1985 [Fidge 91] Colin Fidge, Logical Time in Distributed Computing Systems, IEEE Computer, pp. 28 - 33, Aug. 1991. [Fujiw 85] Hideo Fujiwara, Logic Testing and Design for Testability, MIT Press, 1985. [Gabow 76] Harold N. Gabow, Shachindra N. Matheshwari, and et al, On Two Problems in the Generation of Program Test Paths, IEEE Tr. On Software Engineering, pp. 227 - 231, Sept. 1976. [Gill 62] A. Gill, Introduction to the Theory of Finite-State Machines, McGraw-Hill, New York, 1962. [Gorli 90] Michael M. Gorlick, Carl F. Kesselman, and et al, Mockingbird: A Logical Methodology for Testing, The Journal of Logic Programming, pp. 95 - 119, January/March 1990. [Helmb 85] David Helmbold and David Luckham, Debugging Ada Tasking Programs, IEEE Software, pp. 47 - 57, March 1985. [Henni 68] Frederick C. Hennie, Finite-State Models for Logical Machines, John Wiley & Sons, Inc., 1968. [Hoffm 89] Daniel Hoffman, Hardware Testing and Software ICs, The Pacific NW Software Quality Conference, pp. 234 - 244, September 1989. [ISOa]^ISO 7776, Information processing systems - Open Systems Interconnection - Description of the X.25 LAPB-compatible DTE data link procedures. [ISOb] ISO DS 9646, OSI Conformance Testing Methodology and Framework, 1990. [ISOc] ISO 9074, ESTELLE - A Formal Description Technique Based on an Extended State Transition Model, 89-07-15. [ISOd] ISO 8807, LOTOS - A Formal Description Technique Based on the Temporal Ordering of Observational Behavior, 89-02-15. [ISOe]^ISO 8824, Specification of Abstract Syntax Notation One, 1987. [Jard 83] C. Jard and G. v. Bochmann, An Approach to Testing Specifications, Proc. of ACM SIGSOFT/SIGPLAN Software Eng. Symposium on High-Level Debugging, 1983. [Karjo 90] G. Karjoth, A Compilation of Algebraic Process Based on Extended-Action Derivation, Third Intl Conference on Formal Description Techniques, 1990.  BIBLIOGRAPHY^  116  [Kim 91] M.C. Kim, Samuel T. Chanson and Son T. Vuong, Protocol Trace Analysis based on Formal Specifications, Fourth Intl Conference on Formal Description Techniques, pp. 399 - 414, Nov. 1991. [Kim 92a] M.C. Kim, Samuel T. Chanson and Son T. Vuong, Concurrency Model and Its Application to Formal Protocol Specifications, accepted for publication of IEEE Infocom '93. [Kim 92b] M.C. Kim, Samuel T. Chanson and Son T. Vuong, Trace Analysis based on Concurrent Specifications and Its Applications, submitted for publication. [King 76] James C. King, Symbolic Execution and Program Testing, CACM, pp. 385 - 394, July 1976. [Lampo 78] Leslie Lamport, Time, Clocks, and the Ordering of Events in a Distributed System, CACM, pp. 558 - 565, July 1978. [Linn 90] R. J. Linn, Conformance Testing for OSI Protocols, Computer Networks and ISDN Systems, pp. 203 -219, April 1990. [Logri 88] L. Logrippo, A. Obaid, and et al., An Interpreter for LOTOS, A Specification Language for Distributed Systems, Software-Practice and Experience, pp. 365 - 385, April 1988. [Lu 91] Ying Lu, On TESTGEN, An Environment for Protocol Test Sequence Generation, and Its Applications to the FDDI MAC Protocol, Master Thesis, Dept. of Computer Science, Univ. of British Columbia, 1991. [Matte 89] Friedemann Mattern, Virtual Time and Global States of Distributed Systems, Parallel and Distributed Algorithms, pp. 215 - 226, North-Holland, 1989. [Mcdow 89] Charles E. Mcdowell and David P. Helmbold, Debugging Concurrent Programs, ACM Computing Surveys, pp. 593 - 622, Dec. 1989. [Milne 80] R. Milner, A Calculus of Communicating Systems, Lecture Notes in Computer Science, Springer-Verlag, 1980. [Mille 88] Barton P. Miller and Jong-Deok Choi, A Mechanism for Efficient Debugging of Parallel Programs, ACM SIGPLAN Workshop on Parallel and Distributed Debugging, pp. 141 - 150, May 1988. [Mohr 92] Bernd Mohr, Standardization of Event Traces Considered Harmful or Is an Implementation of Object-Independent Event Trace Monitoring and Analysis Systems Possible?, Univ. Erlangen-Nurnberg, IMMD 7, Germany, 1992. [Moore 59] E. F. Moore, The Shortest Path Through a Maze, Proc. Internat. Symp. Switching Th., 1957, Part II, Harvard Univ. Press, pp. 285 - 292, 1959.  BIBLIOGRAPHY^  117  [Oster 81] L. J. Osterweil, L. D. Forsdick, and et al, Error and Anomaly Diagnosis through Data Flow Analysis, Computer Program Testing, edited by B. Chandrasekaran and S. Radicchi, North-Holland Publishing Co., pp. 35 - 64, 1981. [Parke 89] Kenneth P. Parker, The Impact of Boundary Scan on Board Test, IEEE Design & Test of Computers, pp. 18 - 30, Aug. 1989. [Podgu 90] Andy Podgurski and Lori A. Clarke, A Formal Model of Program Dependences and Its Implications for Software Testing, Debugging, and Maintenance, IEEE Tr. on Software Engineering, pp. 965 - 979, Sept. 1990. [Probe 92] Robert L. Probert, Hualong Yu, and et al, Relative-Clock-based Specification and Test Result Analysis of Distributed Systems, The 11th IEEE Intl Phoenix Conference on Computers and Communications, 1992. [Rafiq 90] 0. Rafiq and R. Castanet, Experience with the Astride Testing Approach, The IFIP TC6 Intl Conference on Computer Networking COMNET'90, 1990. [Rayne 87] D. Rayner, OSI Conformance Testing, Computer Networks and ISDN Systems 14(1) pp. 79-98, 1987. [Rayna 91] Michel Raynal, Synchronization and Concurrency Measures for Distributed Computations, IRISA Publication Interne 610, Oct. 1991. [Rayna 92] Michel Raynal, About Logical Clocks for Distributed Systems, ACM Operating Systems Review, pp. 41 - 48, Jan. 1992. [Saleh 92] Kassem Saleh, Testability-directed Service Definitions and their Synthesis, The 11th IEEE Int'l Phoenix Conference on Computers and Communications, 1992. [Sampl 90] M. Sample and G. Neufeld, Support for ASN.1 within a Protocol Testing Environment, The Third Int'l Conference on Formal Description Techniques, Nov. 1990. [Sarik 86] Behcet Sarikaya and G. v. Bochmann, Obtaining Normal Form Specifications for Protocols, Computer Networks Usage: Recent Experiences, pp. 601 - 612, Elsevier Science Publishers, 1986. [Sarik 87] Behcet Sarikaya, Gregor V. Bochmann, and et al, A Test Design Methodology for Protocol Testing, IEEE Tr. on Software Engineering, pp. 518 - 531, May 1987. [Stone 88] Janice M. Stone, A Graphical Representation of Concurrent Processes, ACM SIGPLAN Workshop on Parallel and Distributed Debugging, pp. 226 - 235, May 1988. [Tai 86] K. C. Tai A Graphical Notation for Describing Executions of Concurrent Ada Programs, ACM Ada Letters, pp. 94 - 103, Jan/Feb 1986. [Tanen 88] Andrew S. Tanenbaum, Computer Networks, Second Edition, Prentice-Hall, 1988.  BIBLIOGRAPHY^  118  [Taylo 92] R. N. Taylor, D. L. Levine, and et al, Structural Testing of Concurrent Programs, IEEE Tr. on Software Engineering, pp. 206 - 215, March 1992. [Tripa 91] Piyu Tripathy and Behcet Sarikaya, Test Generation from LOTOS Specifications, IEEE Tr. on Computers, April 1991. [Ural 86] Hasan Ural and Robert L. Probert, Step-Wise Validation of Communication Protocols and Services , Computer Networks and ISDN Systems 11, pp. 183 - 202, 1986. [Ural 87] Hasan Ural, Test Sequence Selection Based on Static Data Flow Analysis, Computer Communications, pp. 234 - 242, Oct. 1987. [Vuong 89] S. T. Vuong, Y. L. Chan and et al., The UIOv-Method for Protocol Test Sequence Generation, The Second Intl Workshop on Protocol Test Systems, Oct. 1989. [Weise 81] M. Weiser, Program Slicing, IEEE 5th Intl Conference on Software Engineering, pp. 439 - 449, 1981. [Weiss 88] Stewart N. Weiss, A Formal Framework for the Study of Concurrent Program Testing, Second Workshop on Software Testing, Verification, and Analysis, pp. 106 - 113, 1988. [Wood 80] Marin W. Woodward, David Hedley, and et al, Experience with Path Analysis and Testing of Programs, IEEE Tr. on Software Engineering, pp. 278 - 286, May 1980. [Wvong 90] R. Wvong, A New Methodology for OSI Conformance Testing Based on Trace Analysis, Master Thesis, Dept. of Computer Science, Univ. of British Columbia, Oct. 1990. See also LAPB Conformance Testing using Trace Analysis, 11th Intl Symposium on Protocol Specification, Testing, and Verification, pp. 248 - 261, June 1991. [Young 88] Michal Young and Richard N. Taylor, Combining Static Concurrency Analysis with Symbolic Execution, IEEE TR. on Software Engineering, pp. 1499 - 1511, Oct. 1988. [Zhou 92] Jingsong Zhou, TESTGEN Implementation and Test Case Validation, Master Thesis, Dept. of Computer Science, Univ. of British Columbia, 1992.  Appendix A  Estelle Specification of X.25 LAPB  C• .  ^  lapb.e  ^  •)  specification DataLink systemprocess; ^ default individual queue; ^ timescale second;^  procedure writeiframesent (no: INTEGER); EXTERNAL; procedure writeinfor(infor:char); EXTERNAL; PROCEDURE writestate(stn,rec_com,sends,initstate,finalstate:INTEGER); EXTERNAL;  initialize to hostready type^ aFrameType = (I, RR, RNR, REJ, SABM, DISC, UA, DM, FRMR, BAD); ^begin Iframesent := 0; anAddress = (A, B);^ datano := 0; ftype = RECORD^ TEMP := 0; Address: anAddress;^ end ; Frametype: aFrameType; NS: integer;^ trans PF: integer;^ from hostready to datatrans NR: integer;^ begin Udata: integer;^ writestate(usern,0,20,11,14); END;^ output Uu.ConReq; end ; aBufferPtr = "ftype; trans from datatrans to datatrans channel User_Channel(User, Provider); ^ by User:^ when Uu.Conlnd ConReq;^ begin DiscReq;^ writestate(usern,0,23,14,14); ResetReq;^ output Uu.DataReq(datano); DataReq(datano:integer);^ writeiframesent(Iframesent); by Provider:^ writedatano(datano); Conlnd;^ datano := datano + 1; Disclnd;^ Iframesent := Iframesent + 1; Resetlnd;^ end; DataInd(datano:integer); Acklnd;^ trans from datatrans to datatrans channel aPhysicalAccess(User, Provider); ^ when Uu.Datalnd by User:^ begin DataRequest(frame: aBufferPtr);^ writestate(usern,0,23,14,14); by Provider:^ output Uu.DataReq(datano); Datalndicat(frame: aBufferPtr); ^ writeiframesent(Iframesent); writedatano(datano); module anMLProcedure process(usern: integer); ^ datano := datano + 1; ip Uu: User_Channel(User) individual queue;^ Iframesent := Iframesent + 1; end;^ end; body MLPBody for anMLProcedure ; ^ var^ Iframesent : integer; ^ datano: integer;^ TEMP: integer;^ state hostready, hostbusy, disconn, datatrans, linkreset ; procedure writedatano (no: INTEGER); EXTERNAL;  trans from datatrans to datatrans when Uu.Acklnd begin writestate(usern,25,25,14,14); end; trans from datatrans to linkreset provided (Iframesent > 3) begin writestate(usern,26,26,14,15); output Uu.ResetReq;  end;^ trans^ from linkreset to datatrans^ when Uu.Conlnd^ begin^ writestate(100,27,26,15,14);^ TEMP := 100;^ end;^ trans^ from datatrans to disconn^ provided (TEMP = 100) begin^ writestate(usern,0,22,14,13); ^ output Uu.DiscReq;^ end;^ trans^ from disconn^ when Uu.Disclnd begin^ {writestate(usern,28,0,13,13);)^ end;^ END ;^ module anSLProcedure process (stn:integer); ^ ip^ SEND: aPhysicalAccess(User) individual queue; RECV: aPhysicalAccess(Provider) individual queue; ^ P: User_Channel(Provider) individual queue; ^ end; body SLPBody for anSLProcedure; ^  (• Reset flow-control variables and clear error conditions. •) begin VS := 0; LastRxNR := 0; Unacked := 0; VR := 0; LastTxNR := 0; SendingREJ := false; Loca1RNR := false; TimerRecovery := false; RemoteRNR := false; end; function Between(a, b, c: integer): boolean; begin if (a <= c) then Between := ((a <= b) and (b <= c)) else Between := ((b <= c) or (a <= b)); end; function IsCorrectAck(nr: integer):boolean; (•2.3.4.9•) begin if (TimerRecovery = false) then IsCorrectAck := Between(LastRxNR, nr, VS) else IsCorrectAck := Between(LastRxNR, nr, x); end; PROCEDURE writestate(stn,rec_com,sends,initstate,finalstate:INTEGER); EXTERNAL; procedure writedatano (no: INTEGER); EXTERNAL;  state^ SEND_DM, SEND_SABM, ABM, WAIT_SABM, SEND_DISC; ^  PROCEDURE w_send_data(ns,nr,data: INTEGER) ; EXTERNAL;  const^ T1^2;^ T2 = 1;^ N2 = 6;^ k = 8;^ Modulus = 8;^  (• tl initialize to SEND_DM begin new(FRMRBuffer); for VS := 0 to Modulus - 1 do new(RetxBuffer(VS]); TxAttempts := 0 end;  var^ TxAttempts: integer; ^ clearrecovery: boolean; oldvs: integer;^ T1Running: boolean; (• used to restart the T1 timer •) ^ FRMRBuffer, frametwo, aframe: aBufferPtr; ^ VS, LastRxNR, Unacked: integer;^ RetxBuffer: array(0..Modulus) of aBufferPtr; ^ VR, LastTxNR: integer;^ SendingREJ, LocalRNR: boolean;^ TimerRecovery, RemoteRNR: boolean;^ Correctack: boolean;^ x: integer; {• used in timer recovery •) ^ procedure ResetWindow;^  t2 trans from SEND_DM (*2.4.4.4•) when P.ConReq to SEND_SABM begin new(frametwo); frametwoA.Frametype := SABM; frametwoA.PF := 1; frametwoA.Address := 8; writestate(stn, 20,1,2,3); OUTPUT SEND.DataRequest(frametwo);  OUTPUT SEND.DataRequest(frametwo); end; dispose(frame) end;  TxAttempts := 0; end; t3 •} from SEND_DM when RECV.DataRequest provided (frameA.Frametype = SABM) •2.4.4.4.1") to ABM begin new(frametwo); frametwoA.Frametype := UA; frametwoA.PF := frameA.PF; frametwoA.Address := A; writestate(stn,5,3,2,4); OUTPUT SEND.DataRequest(frametwo); ResetWindow; OUTPUT P.Conlnd; TxAttempts := 0; dispose(frame); end; (' t4 ")  (' t5 ")  V t6 ")  provided (frameA.Frametype = DISC) ("2.4.4.4.1') to SEND_DM begin new(frametwo); frametwoA.Frametype := DM; frametwoA.PF := frameA.PF; frametwoA.Address := A; writestate(stn,2,4,2,4); OUTPUT SEND.DataRequest(frametwo); TxAttempts := 0; dispose(frame) end; provided (frameA.Frametype = DM) (•2.4.4.7') to SEND_SABM begin new(frame); frameA.Frametype := SABM; frameA.PF := 1; frameA.Address := B; writestate(stn,4,1,2,3); OUTPUT SEND.DataRequest(frame); TxAttempts := 0; dispose(frame) end; provided otherwise V2.4.3/2.4.4.4.1') to SEND_DM begin if (frame".Address = A) AND (frameA.PF = 1) then begin new(frametwo); frametwoA.Frametype := DM; frametwoA.PF := 1; frametwoA.Address := A; writestate(stn,26,4,2,2);  f" t7 ')  from SEND_DM  provided TxAttempts <= N2 ('2.4.4.4.2') delay(T1) begin new(frametwo); frametwoA.Frametype := DM; frametwoA.PF := 0; frametwoA.Address := A; writestate(stn,6,4,2,2); OUTPUT SEND.DataRequest(frametwo); TxAttempts := TxAttempts + 1 end;  (' t8 ') provided TxAttempts > N2 ['2.4.4.4.2•) delay(T1) begin f' "initiate appropriate recovery actions" ') end; f' t9 "I from SEND_SARM (•2.4.4.1') when RECV.DataRequest provided (frameA.Frametype = SABM) (•2.4.4.5.1') begin new(frametwo); frametwoA.Frametype := UA; frametwoA.PF := frameA.PF; frametwoA.Address := A; writestate(stn,5,3,3,3); OUTPUT SEND.DataRequest(frametwo); f' See 2.4.4.5.1.(1) is being used here. ^') TxAttempts := 0; dispose(frame) end; ('  t10 •)  (' t11 ')  provided (frame.Frametype = DISC) (•2.4.4.5.2') to SEND_DM begin new(frametwo); frametwoA.Frametype := DM; frametwoA.PF := frameA.PF; frametwoA.Address := A; writestate(stn,2,4,3,2); OUTPUT SEND.DataRequest(frametwo); TxAttempts := 0; dispose(frame) end; provided (frameA.Frametype = UA) (•2.4.4.1•) to ABM begin  ResetWindow; writestate(stn,3,20,3,4); OUTPUT P.Conlnd; TxAttempts := 0; dispose(frame) end; (' t12 ')  f' t13 ')  provided (frameA.Frametype = DM) AND (frameA.PF = 1) ("2.4.4.1') to SEND_DM begin TxAttempts := 0; dispose(frame) end; provided otherwise (•2.4.4.1') to SEND_SABM begin dispose(frame) end;  end;  (' t14 ') from SEND_SABM provided TxAttempts <= N2 ('2.4.4.1") delay(T1) begin new(frametwo); frametwoA.Frametype := SABM; frametwoA.PF := 1; frametwoA.Address := B; writestate(stn,6,1,3,3); OUTPUT SEND.DataRequest(frametwo); TxAttempts := TxAttempts + 1 end; f' t15 '} provided TxAttempts > N2 f'2.4.4.1") delay(T1) begin (' "initiate appropriate recovery actions end; (' t16 ') from ABM (•2.4.5') when RECV.DataRequest ^ provided (frameA.Frametype I) AND IsCorrectAck(frameA.NR) begin if (frameA.NR = LastRxNR) then (no frames acknowledged) begin end else begin if (TimerRecovery = false) then begin while LastRxNR <> frameA.NR do begin LastRxNR := (LastRxNR + 1) mod Modulus; (' writestate(stn, 7, 25, 4, 4); ') OUTPUT P.Acklnd; end; Unacked := (VS + Modulus LastRxNR) mod Modulus; end  •)  else begin if (frame'.NR = x) then begin frame'.NR := (frameA.NR + Modulus - 1) mod Modulus; end; (In the timer recovery condition, we need at least one unacknowledged I-frame to poll with. See 2.4.5.9 ) while LastRxNR <> frameA.NR do begin LastRxNR := (LastRxNR + 1) mod Modulus; (' writestate(stn, 7, 25, 4, 4); ') OUTPUT P.Acklnd; end; VS := (frameA.NR + 1) mod Modulus; (in timer recovery, Unacked is always set to 1 end; TxAttempts := 0; (one or more frames have been acked}  if Loca1RNR then begin [cannot accept information field) if frameA.PF = 1 then begin(' status request ') (' Begin of WriteSFrame(RNR,1,A) in APPENDIX C '} new(frametwo); frametwo'.Frametype := RNR; frametwoA.PF := 1; frametwoA.NR := VR; frametwoA.Address := A; (' writestate(stn, 7, 8, 4, 4); *) OUTPUT SEND.DataRequest(frametwo); LastTxNR := VR; {' Begin of WriteSFrame(RNR,1,A) in APPENDIX C "} end; dispose(frame); end else begin if frameA.NS <> VR then begin (• sequence error • ) if SendingREJ = false then begin (' Begin of WriteSFrame(REJ,frameA.PF,A) in APPENDIX C ') new(frametwo); frametwoA.Frametype := REJ; frametwoA.PF := frameA.PF; frametwoA.NR := VR; frametwoA.Address := A; (' writestate(stn, 7, 11, 4, 4); •} OUTPUT SEND.DataRequest(frametwo); LastTxNR := VR; (' Begin of WriteSFrame(REJ,frametwoA.PF,A) in APPENDIX C ") SendingREJ := true; end else begin if frameA.PF = 1 then begin{' status request ') (' Begin of WriteSFrame(RR,1,A) in APPENDIX C ') new(frametwo); frametwoA.Frametype := RR; frametwoA.PF := 1; frametwo'.NR := VR; frametwoA.Address := A; (' writestate(stn, 7, 12, 4, 4); ') OUTPUT SEND.DataRequest(frametwo); LastTxNR := VR;  (' Begin of WriteSFrame(RR,1,A) in APPENDIX C •)^ end^  end; dispose(frame); ^ end;^ if(frameA.NS <> VR) then^ begin^ end^ else begin^ SendingREJ := false; (insequence I-frame received) ^ VR := (VR + 1) mod Modulus;^ if frameA.PF = 1 then begin(' status request ') ^ (• Begin of WriteSFrame(RR,1,A) in APPENDIX C ') ^ new(frametwo);^ frametwoA.Frametype := RR; ^ frametwo".PF := 1;^ frametwo".NR := VR;^ frametwoA.Address := A;^ (' writestate(stn, 7, 12, 4, 4); •} ^ OUTPUT SEND.DataRequest(frametwo); ^ LastTxNR := VR;^ (• End of WriteSFrame(RR,1,A) in APPENDIX C ") ^ end;^ writestate(stn, 7, 20, 4, 4); OUTPUT P.DataInd(frame".Udata); ^ end;^ end;^ end;^  endLastRxNR := (LastRxNR + 1) mod Modulus; OUTPUT P.Acklnd; Unacked := (VS + Modulus - LastRxNR) mod Modulus; end else begin if (clearrecovery = false) AND (frame".NR = x) then begin frame".NR := (frame".NR + Modulus - 1) mod Modulus; end; {In the timer recovery condition, we need at least one unacknowledged I-frame to poll with. See 2.4.5.9 ) while LastRxNR <> frame".NR do begin LastRxNR := (LastRxNR + 1) mod Modulus; OUTPUT P.Acklnd; end; VS := (frame".NR + 1) mod Modulus; (in timer recovery, Unacked is always set to 1 end; TxAttempts := 0; (one or more frames have been acked} end; f' End of ReadAck(frame".NR,clearrecovery) in APPENDIX C ')  if (frame".Address = A) AND (frameA.PF = 1) then begin (" status request ') if LocalRNR then begin (• Begin of WriteSFrame(RNR,1,A) in APPENDIX C ") new(frametwo); (• t17 ")^ frametwoA.Frametype := RNR; provided (frameA.Frametype = I) AND (IsCorrectAck(frame".NR) = false) ^ frametwo".PF := 1; to WAIT_SABM {•2.3.4.9/2.4.6•)^ frametwo".NR := VR; begin^ frametwoA.Address := A; new(frametwo);^ (• writestate(stn, 8, 8, 4, 4); ') frametwo".Frametype := FRMR;^ OUTPUT SEND.DataRequest(frametwo); frametwo".PF := 0;^ LastTxNR := VR; frametwoA.Address := A; ^ {' End of WriteSFrame(RNR,1,A) in APPENDIX C ') writestate(stn, 7, 6, 4, 5);^ end OUTPUT SEND.DataRequest(frametwo); ^ else begin OUTPUT P.Disclnd;^ (• Begin of WriteSFrame(RR,1,A) in APPENDIX C ') TxAttempts := 0;^ new(frametwo); dispose(frame)^ frametwo".Frametype := RR; end;^ frametwoA.PF := 1; frametwo".NR := VR; (' t18 ')^ frametwoA.Address := A; provided (frameA.Frametype = RR) OR (frameA.Frametype = RNR) ^ (• writestate(stn, 8, 12, 4, 4); ') OUTPUT SEND.DataRequest(frametwo); OR (frameA.Frametype = REJ) AND IsCorrectAck(frameA.NR) ^ to ABM^ LastTxNR := VR; begin^ (• End of WriteSFrame(RR,1,A) in APPENDIX C ') clearrecovery :=^ end; TimerRecovery AND (frame".Address = B) AND (frameA.PF = 1); ^end; if (frame.Frametype RNR) then begin (• remote busy condition ') (timer recovery is cleared when a supervisory response ^ RemoteRNR := true; with Final bit set is received; see 2.4.5.9 ") ^ (• Begin of ReadAck(frame".NR,clearrecovery) in APPENDIX C ') ^ TxAttempts := 0; if (frameA.NR = LastRxNR) then (no frames acknowledged)^ end begin^ else begin if (frameA.Frametype = REJ) OR end^ ((frame".Frametype = RR) AND RemoteRNR) then begin else begin^ N, RemoteRNR := false;^ if (TimerRecovery = false) then begin^ if TimerRecovery = false then begin (' retransmit ") while LastRxNR <> frameA.NR do begin ^ oldvs := VS;  ^ VS := LastRxNR; begin ^ (' set FRMRBuffer ') while VS <> oldvs do begin ^ new(frametwo); (' Begin of WritelFrame(O,B) in APPENDIX C ') ^ frametwo".Frametype := FRMR; new(frametwo); ^ frametwo".PF := 0; frametwo".Frametype := I; ^ frametwo".Address := A; frametwo".Udata := ^ RetxBuffer(VS)".Udata; writestate(stn, 8, 6, 4, 5); frametwo".NS := VS;^ OUTPUT SEND.DataRequest(frametwo); frametwo".PF := 0; ^ frametwo".NR := VR; OUTPUT P.Disclnd; ^ frametwo".Address := B; TxAttempts := 0; ^ dispose(frame) (' writestate(stn, 8, 8, 4, 4); ') ^ OUTPUT SEND.DataRequest(frametwo); end; VS := (VS + 1) mod Modulus; Unacked := (VS ^ + Modulus - LastRxNR) mod Modulus;^(• t20 • LastTxNR := VR; provided (frame.Frametype = SABM) ("2.4.7•) ^ (' End of WriteIFrame(0,B) in APPENDIX C ') to ABM ^ end; begin ^ end; new(frametwo); ^ end; frametwo".Frametype := UA; ^ if clearrecovery then begin (' clearing timer recovery ") frametwo".PF := frame".PF; ^ TimerRecovery := false; frametwo".Address := A; ^ if RemoteRNR = false then begin (' retransmit ') writestate(stn, 5, 3, 4, 4); ^ VS := LastRxNR; ^ OUTPUT SEND.DataRequest(frametwo); if VS <>^ x then Reset Window; begin OUTPUT P.ResetInd; ^ while VS <> x do begin TxAttempts := 0; ^ (' Begin of WriteIFrame(0,B) in APPENDIX C ') dispose(frame) ^ new(frametwo); end; frametwo".Frametype := I; frametwo".Udata := ^ RetxBuffer[VS]".Udata;^ (' t21 frametwo".NS := VS;^ provided (frame.Frametype = DISC) ("2.4.4.3•) frametwo".PF := 0; ^ to SEND_DM frametwo".NR := VR; begin ^ frametwo".Address := B; new(frametwo); ^ (' writestate(stn, 8, 8, 4, 4); ') ^ frametwo".Frametype := UA; OUTPUT SEND.DataRequest(frametwo); frametwo".PF := frame.PF; ^ VS := (VS + 1) mod Modulus; frametwo".Address := A; ^ Unacked := (VS ^ + Modulus - LastRxNR) mod Modulus; writestate(stn,2,3,4,2); LastTxNR := VR; OUTPUT SEND.DataRequest(frametwo); ^ (• End of WritelFrame(0,B) in APPENDIX C ') TxAttempts := 0; ^ end; dispose(frame) ^ end end; else Unacked := 0;^ (' t22 • end^ provided (frame.Frametype = UA) •2.4.6.3") ^ else begin ^ (' remote busy, don't retransmit ') to SEND_SABM VS := x; begin ^ Unacked := (VS + Modulus - LastRxNR) mod Modulus; new(frametwo); ^ end; frametwo".Frametype := SABM; ^ end; frametwo".PF := 1; ^ end; frametwo".Address := B; writestate(stn, 3, 1, 4, 3); ^ dispose(frame) OUTPUT SEND.DataRequest(frametwo); ^ end; OUTPUT P.Disclnd; TxAttempts := 0; ^ (" t19 ') dispose(frame) ^ provided ((frame".Frametype = RR) OR (frame".Frametype = RNR) end; OR (frame".Frametype = REJ)) AND (IsCorrectAck(frame".NR) = false) ^ to WAIT_SABM (' t23 ') provided (frame.Frametype = DM) (•2.4.6.4•) }  )  to SEND_SABM begin new(frametwo); frametwoA.Frametype := SABM; frametwo".PF := 1; frametwo".Address := B; writestate(stn, 4, 1, 4, 3); OUTPUT SEND.DataRequest(frametwo); OUTPUT P.Disclnd; TxAttempts := 0; dispose(frame) end; t24  •)  (• t25 •  provided (frameA.Frametype = FRMR) •2.4.6.2') to SEND_SABM begin new(frametwo); frametwo".Frametype := SABM; frametwo".PF := 1; frametwoA.Address := B; writestate(stn, 14, 1, 4, 3); OUTPUT SEND.DataRequest(frametwo); OUTPUT P.Disclnd; TxAttempts := 0; dispose(frame) end; )  provided (frameA.Frametype = BAD) (•2.4.6.1•) to WAIT_SABM begin f• set FRMRBuffer •) new(frametwo); frametwo".Frametype := FRMR; frametwo".PF := 0; frametwo".Address := A; writestate(stn, 14, 14, 4, 5); OUTPUT SEND.DataRequest(frametwo); OUTPUT P.Disclnd; TxAttempts := 0; dispose(frame) end;  (• t26 •)  provided otherwise to ABM begin (• should never happen •) end; ( • Note that because S and P have independent queues, we don't need to worry about S requests in the other states: they'll be handled when the appropriate frames arrive at P and the system enters state ABM. •)  t27  when P.DataReq •2.4.5.1•) to ABM provided ((RemoteRNR OR TimerRecovery OR (Unacked >= k)) = false) begin  (' Begin of WriteIFrame(0,13) in APPENDIX C ") (' copy frame into RetxBuffer[VS] ') new(aframe); aframeA.Frametype := I; aframe".Udata := RetxBuffer[VS]".Udata; aframe".NS := VS; aframeA.PF := 0; aframe".NR := VR; aframe".Address := 8; (' writestate(stn, 23, 5, 4, 4); •) (' w_send_data(VS, VR, aframe".Udata); •) OUTPUT SEND.DataRequest(aframe); VS := (VS + 1) mod Modulus; Unacked := (VS + Modulus - LastRxNR) mod Modulus; LastTxNR := VR; (• End of WriteIFrame(0,13) in APPENDIX C end; (' t28 ') when P.ResetReq ('2.4.7•) to SEND_SABM begin new(frametwo); frametwo".Frametype := SABM; frametwo".PF := 1; frametwo".Address := B; writestate(stn, 26, 1, 4, 3); OUTPUT SEND.DataRequest(frametwo); TxAttempts := 0 end; (• t29 ') when P.DiscReq (•2.4.4.3') to SEND_DISC begin new(frametwo); frametwo".Frametype := DISC; frametwo".PF := 1; frametwo".Address := B; writestate(stn,22,2,4,6); OUTPUT SEND.DataRequest(frametwo); TxAttempts := 0 end; f• t30 ') from ABM provided ((Unacked > 0) OR RemoteRNR) AND (TxAttempts <= N2) AND T1Running (•2.4.5.7/2.4.5.9') delay(T1) begin if Unacked = 0 then begin (' remote busy? poll with supervisory command • } if LocalRNR then begin new(frametwo); frametwo".Frametype := RNR; frametwo".PF := 1; frametwo".NR := VR; frametwo".Address := B; writestate(stn, 6, 8, 4, 4); OUTPUT SEND.DataRequest(frametwo);  end^ (PiggybackTimeout) else begin^ if LocalRNR then begin (• Begin of WriteSFrame(RNR,O,A) in APPENDIX C new(frametwo);^ frametwo'.Frametype := RR; ^ new(frametwo); frametwo'.Frametype := RNR; frametwo'.PF := 1;^ frametwo'.PF := 0; frametwo'.NR := VR;^ frametwo'.NR := VR; frametwo'.Address := B;^ frametwo'.Address := A; writestate(stn, 6, 7, 4, 4);^ (• writestate(stn, 6, 8, 4, 4); I OUTPUT SEND.DataRequest(frametwo);^ end;^ OUTPUT SEND.DataRequest(frametwo); end^ LastTxNR := VR; else begin (• timer recovery •} ^End of WriteSFrame(RNR,O,A) in APPENDIX C ') if TimerRecovery = false then begin (' enter timer recovery •)^end TimerRecovery := true; ^ else begin x := VS;^ (' Begin of WriteSFrame(RR,O,A) in APPENDIX C '} end;^ new(frametwo); frametwo'.Frametype := RR; new(frametwo);^ frametwo'.PF := 0; frametwo'.Frametype := I; ^ frametwo'.NR := VR; frametwo'.Udata := RetxBuffer[VS)".Udata;^ frametwo'.Address := A; frametwo'.NS := VS;^ frametwo".PF := 1;^ (• writestate(stn, 6, 7, 4, 4); •) frametwo'.NR :=^ OUTPUT SEND.DataRequest(frametwo); frametwo'.Address := B; ^ LastTxNR := VR; (• Begin of WriteSFrame(RR,O,A) in APPENDIX C writestate(stn, 6, 5, 4, 4);^ end; OUTPUT SEND.DataRequest(frametwo); ^ VS := (VS + 1) mod Modulus;^ end; Unacked := (VS + Modulus - LastRxNR) mod Modulus; LastTxNR := VR;^ (• t34 ') end;^ from WAIT_SABM {'2.4.7.3• TxAttempts := TxAttempts + 1^ when RECV.DataRequest end;^ provided (frameA.Frametype = SABM) (•2.4.4.1") to ABM (* t31 •)^ begin new(frametwo); provided TxAttempts > N2 (*2.4.5.9•) ^ delay(T1)^ frametwo'.Frametype := UA; to SEND_SABM^ frametwo'.PF := frameA.PF; frametwo'.Address := A; begin^ writestate(stn, 5, 3, 5, 4); new(frametwo);^ OUTPUT SEND.DataRequest(frametwo); frametwo'.Frametype := SABM; ^ frametwo".PF := 1;^ ResetWindow; OUTPUT P.Conlnd; frametwo'.Address := ^ TxAttempts := 0; writestate(stn, 6, 1, 4, 3);^ OUTPUT SEND.DataRequest(frametwo);^ dispose(frame) OUTPUT P.DiscInd;^ end; TxAttempts := 0 end;^ (' t35 ') provided (frameA.Frametype = DISC) •2.4.7.3• (* t32^ to SEND_DM provided T1Running = false^ begin to ABM^ new(frametwo); (• To restart the 11 timer, ReadAck sets T1Running to false. 1^frametwo'.Frametype := UA; begin^ frametwo'.PF := frameA.PF; T1Running := true^ frametwo'.Address := A; end;^ writestate(stn,2,3,5,2); OUTPUT SEND.DataRequest(frametwo); {• t33^ OUTPUT P.Disclnd; provided LastTxNR <> VR ("2.4.5.2.1/2.4.8.2• ^ TxAttempts := 0;^ delay(T2)^ dispose(frame) to ABM^ end; begin  N,  ^ ^  {' t36 ")^ provided (frame".Frametype = DM) (•2.4.7:3•) ^ to SEND_SABM^ begin^ new(frametwo);^ frametwo".Frametype := SABM; ^ frametwo".PF := 1;^ frametwo".Address := B;^ writestate(stn, 4, 1, 5, 3);^ OUTPUT SEND.DataRequest(frametwo);^ TxAttempts := 0; dispose(frame)^ end;^ t37 ")^ provided (frame".Frametype = FRMR) (•2.4.7.3') ^ to SEND_SABM^ begin^ new(frametwo);^ frametwo".Frametype := SABM; ^ frametwo".PF := 1;^ frametwo".Address := B;^ writestate(stn, 14, 1, 5, 3);^ OUTPUT SEND.DataRequest(frametwo);^ TxAttempts := 0;^ dispose(frame)^ end; t38 •)  to SEND_SABM begin new(frametwo); frametwo".Frametype := SABM; frametwo".PF := 1; frametwo".Address := B; writestate(stn, 6, 1, 5, 3); OUTPUT SEND.DataRequest(frametwo); TxAttempts := 0 end; (• t41 ") from SEND_DISC (•2.4.4.3•) when RECV.DataRequest provided (frame".Frametype = SABM) (•2.4.4.5.2") to SEND_DM begin new(frametwo); frametwo".Frametype := DM; frametwo".PF := frame.PF; frametwo".Address := A; writestate(stn,5,4,6,2); OUTPUT SEND.DataRequest(frametwo); TxAttempts := 0; dispose(frame) end; (•  provided otherwise (•2.4.7.3') to WAIT_SABM begin if frame".PF = 1 then begin new(frametwo); frametwo".Frametype := FRMR; frametwo".PF := 1; frametwo".Address := A; writestate(stn, 26, 6, 5, 5); OUTPUT SEND.DataRequest(frametwo); end; dispose(frame) end;  t39 ") from WAIT_SABM provided TxAttempts <= N2 (•2.4.7.3•) delay(T1) begin new(frametwo); frametwo".Frametype := FRMR; frametwo".PF := 0; frametwo".Address := A; writestate(stn, 6, 6, 5, 5); OUTPUT SEND.DataRequest(frametwo); TxAttempts := TxAttempts + 1 end; t40 ') provided TxAttempts > N2 ("2.4.7.3•) delay(T1)  t42  •)  t43 ")  (" t44 ")  (• t45 ")  provided (frame.Frametype = DISC) ("2.4.4.5.1•) to SEND_DISC begin new(frametwo); frametwo".Frametype := UA; frametwo".PF := frame".PF; frametwo".Address := A; writestate(stn,2,3,6,2); OUTPUT SEND.DataRequest(frametwo); TxAttempts := 0; dispose(frame) end; provided (frame".Frametype = UA) (•2.4.4.3•) to SEND_DM begin TxAttempts := 0; writestate(stn,3,27,6,2); OUTPUT P.Disclnd; dispose(frame) end; provided (frame".Frametype = DM) (•2.4.4.3") to SEND_DM begin TxAttempts := 0; dispose(frame) end;  provided otherwise (•2.4.4.3') to SEND_DISC begin dispose(frame) end; t46 ') from SEND_DISC provided TxAttempts <= N2 ('2.4.4.3') delay(T1) begin new(frametwo); frametwo".Frametype := DISC; frametwo".PF := 1; frametwe.Address := B; writestate(stn, 6, 3, 6, 6); OUTPUT SEND.DataRequest(frametwo); TxAttempts := TxAttempts + 1 end; (' t47 ") provided TxAttempts > N2 (•2.4.4.3') delay(T1) begin (' "initiate appropriate recovery actions" ') end; end; (•^body PLBody for aPhysicalLayer; external; modvar DCE: anSLProcedure; DTE: anSLProcedure; user0 : anMLProcedure ; userl : anMLProcedure ; initialize (DataLink) begin init DCE with SLPBody(0); snit DTE with SLPBody(1); snit user° with MLPBody(10) ; snit userl with MLPBody(11) connect connect connect connect  end; end. (DataLink)  DCE.RECV DCE.SEND DCE.P to DTE.P to  to DTE.SEND; to DTE.RECV; userO.Uu; userl.Uu;  ^  *3  /•  ^  lapb.c  Between(a, b, c) int a, b, c; { if (a <= c)&&((a <= b) && (b <= c)) then Correctack := true; else if (a > c) && ((b <= c) II (a <= b)) Correctack := true; else Correctack := false; IsCorrectAck(nr) int nr; if (TimerRecovery == false) then Between(LastRxNR, nr, VS); else Between(LastRxNR, nr, x);  /• This procedure writes out the current host,^•I I' incoming type of event or frame or command , and the I" current/initial state of host upon receival of event writestate(stn,rec_com,sends,initstate,finalstate) int stn; int rec_com; int sends ; int initstate; int finalstate ; printf("\n"); printf("\n"); switch(stn) case case case case  0: printf("DCE "); break; 1: printf("DTE "); break; 10: printf("user0 "); break; 11: printf("userl "); break;  switch(rec_com) case case case case case case case case case case case case case  1: printf("«=== Timeout ");break; 2: printf("«=== DISC Command ");break; 3: printf("«=== UA Command ");break; 4: printf("«=== DM Command ");break; 5: printf("«=== SABM Command ");break; 6: printf("«=== Timeout and N2 is MAX ");break; 7: printf("«=== Information Frame ");break; 8: printf("«=== Receiver Busy(RNR_resp) ");break; 9: printf("«=== Lost Frame ");break; 10: printf(" ");break; 11: printf("«=== Frame Rejected ");break; 12: printf("«=== RR_cmd(ACK) ");break; 13: printf("<<=== Duplicate Frame");break;  case case case case case case case case case case  14: 15: 20: 21: 22: 23: 24: 25: 26: 27:  printf ("«=== Bad Command ");break; printf ("<<=== Receiver Ready(RR_resp) ");break; printf ("«=== host_ready"); break; printf (" «=== host_busy"); break; printf (" «=== disc_req"); break; printf ("«=== data_req"); break; printf ("«=== clear_busy"); break; printf ("«=== ack_ind"); break; printf ("<<=== otherwise"); break; printf ("<<=== reset_ind"); break;  switch(sends) case 0: printf( ===» nothing"); break; case 1: printf( ===» SABM"); break; case 2: printf( ===» DISC"); break; case 3: printf( ===» UA"); break; case 4: printf( ===» DM host ready"); break; case 5: printf( ===» I"); break; case 6: printf( ===» FRMR"); break; case 7: printf( ===» RR_cmd"); break; case 8: printf( ===» RNR command Receiver Busy"); break; case 9: printf( ===» REJECT command"); break; case 10: printf( ===» RR_resp"); break; case 11: printf( ===» RNR_resp"); break; case 12: printf( ===» REJ_resp"); break; case 13: printf( ===» bad_cmd"); break; case 14: printf( ===» bad_resp"); break; case 16: printf( ===» Ti"); break; case 17: printf( ===» N2XT1"); break; case 20: printf( ===» host_ready"); break; case 21: printf( • ===» host_busy"); break; case 22: printf( • ===» disc_req"); break; case 23: printf( • ===» data_req"); break; case 24: printf( clear_busy"); break; case 25: printf( • ===» ack_ind"); break; case 26: printf( • ===.» reset_req"); break; case 27: printf( "===>> disc_ind"); break; default: printf( "none"); break ; el  ,  printf("^"); printf("From : "); switch(initstate) case 1: printf("INIT");break; case 2: printf("SEND_DM ");break; case 3: printf("SEND_SABM ");break;  case case case case case case case case  4: printf("ABM");break; 5: printf("WAIT_SABM");break; 6: printf("SEND_DISC");break; 11: printf("hostready");break; 12: printf("hostbusy");break; 13: printf("disconn");break; 14: printf("datatrans");break; 15: printf("linkreset");break;  printf("^To : ") ; switch(finalstate)  case case case case case case case case case case case  1: printf("INIT");break; 2: printf("SEND_DM ");break; 3: printf("SEND_SABM ");break; 4: printf("ABM");break; 5: printf("WAIT_SABM");break; 6: printf("SEND_DISC");break; 11: printf("hostready");break; 12: printf("hostbusy");break; 13: printf("disconn");break; 14: printf("datatrans");break; 15: printf("linkreset");break;  case 'g': printf("t-g executed!\n"); break; case 'h': printf("t-h executed!\n"); break; case 'i': printf("t-i executed!\n"); break; writetransi(tran) /•char "transi; int tran; switch(tran)  printf("\n"); ) /•End of writestate Procedure V /* A procedure to display the outgoing event /* sent from host A to host B w_send_data(Bns,Bnr,data) int Bns; int Bnr; int data;  }  case -1: printf("s-t1 executedi\n"); break; case -4: printf("s-t4 executed!\n"); break; case -2: printf("s-t2 executed!\n"); break; case -3: printf("s-t3 executed!\n"); break; case 1: printf("r-t1 executed!\n"); break; case 2: printf("r-t2 executed!\n"); break; case 3: printf("r-t3 executed!\n"); break; case 4: printf("r-t4 executed!\n"); break; case 5: printf("r-t5 executed!\n"); break; case 6: printf("r-t6 executed!\n"); break;  printf("\n"); printf(" Sending data SEQ NO = %d ACK NO = %d DATA = %d ",Bns,Bnr,data); writedatano(no) printf("\n"); int no; w_send_sup(Bns,Bnr,data) int Bns; int Bnr; int data;  printf("datano = %d \n", no);  writerecvdatano(no) int no;  printf("\n"); printf("recvdatano = %d \n", no); printf(" Sending SUP frame SEQ NO = %d ACK NO = %d ",Bns,Bnr); ^ printf("\n"); writeiframesent(no) int no; w_rece_data(Bns,Bnr,data) int Bns; printf("Iframesent = %d \n", no); int Bnr; int data; printtimeout(timer) )  printf("\n"); printf("Received data SEQ NO = %d ACK NO %d ",Bns,Bnr); printf("\n"); w_window(vs, vr, nubuffered) int vs; int vr; int nubuffered; printf("In window: vs = %d, vr = %d, nubuffered %d\n", vs, vr, nubuffered); writeinfor(infor) char infor; switch(infor) case 'd': printf("t-d executed1\n"); break; case 'e': printf("t-eeeee executed!\n"); break; case 'b': printf("send clear_busy!\n"); break;  int timer;  switch(timer) case 1: printf("timer1 is out!!!\n"); break;  exitprot(i) int i; if (i == 1) printf("you are on wrong machine!!!\n"); exit(1); disconnection() exit(1);  Appendix B  Applying Procedure 1 in Section 3.3 to X.25 LAPB  APPENDIX B. APPLYING PROCEDURE 1 IN SECTION 3.3 TO X.25 LAPB ^133  SABM,B,1 a b SABM,?,0 SABM,?,1 c d UA,A,O e UA,A,1 UA,?,? _f DISC,?,0 g DISC,?,1 h  DISC,B,1 DM,A,O DM,A,1 DM,?,1 FRMR,?,? FRMR,A,O FRMR,A,1 RR  i j k 1 m n o p  RNR _q r REJ s I BAD _ ^_ OTHER1,A,1 u OTHER2 w OTHER3 x OTHER4,?,1  ConReq ConInd DiscReq DiscInd ResetReq ResetInd DataReq DataInd^,  1 2 3 . 4 5_ 6 7 8  Appendix C  Flowchart for Example 2 in Section 3.5  134  APPENDIX C. FLOWCHART FOR EXAMPLE 2 IN SECTION 3.5^135  while LastRxNR <> frameA.NR do begin LastRzNR*LastRxNR+1) mod Modulus; OUTPUT PAcklnd ; Unacked:=(VS+Modulus-LastRxNR)mod Modulus;  frameA.NR=VrameA.NR+Modulus-Dmod Modulus; while LastRxNR <> frame^.NR LastRxIIR:=(LastRxNR+1)mod Modulus; OUTPUT P.Acklnd  VS:=(frame^.i, 1)mod Modulus;  APPENDIX C. FLOWCHART FOR EXAMPLE 2 IN SECTION 3.5^136  WriteSFrame(RNR,1A)  SendingREJ:=false; VR*VR+ Dmod Modulus;  It  Y  N  aframeA.Frametype := I;^aframeA.Address := B; aframeA.Udata := RettBuffer[VStUdata; aframeANS := VS; aframeA.PF := 0; aframeA.NR := VR;  OUTPUT SEND.DguaRequeagaframe); VS := (VS + 1) mod Modulus;^LastTzNR := VR; Unacked := (VS + Modulus - LastRxNR) mod Modulus;  APPENDIX C. FLOWCHART FOR EXAMPLE 2 IN SECTION 3.5  li  137  ^  ReadAck(fraine.NR,clearrecovery);  frame.Address = A AND frameA.PF =1  WriteSFrame(RR,1,A)  ^I  rameType(frame)=  frameType(frame)REI OR RR) AND RemoteRNR  RemoteRNR:= true;  TxAttempts:=0;  RemoteRNR :=false;  1  TimerRecovery=false; moteRNR=f. • Y VS:=LastRxNR; I  while VS<> x WritelFrame(0,B);  G  i  i  VS:=x; Unacked:VS+Modulus-LastRxNR) mod Modulus; Unacked:);  1  Appendix D  High-level Description of Implementation D.1 Preprocessing Phase In this phase, some transitions in the specification are converted into finite state machine form. Procedure 4.1 produces a list containing ISP (or OSP) parameters and their types using an  ASN.1 type tree which is the result of ASN.1 parsing. The ISP (or OSP) parameters in the list are assigned values according to the Estelle specification. Procedure 4.2 translates the EFSM form of Estelle.Y into FSM. The "PROVIDED" clause of a transition corresponds to the input condition of the transition. If the clause consists of ISP parameters with values and operators such as "EQUAL" and "AND", it is considered to be a list of input symbols of a transition of the FSM. The "input.processed" flag allows better performance in the main analysis phase of trace analysis since we can filter out some candidate transitions by matching input symbols with the traces without using symbolic simulation. In order to make the output symbols of a transition of the FSM correspond with the EFSM, the assignment statements are checked to select those consisting of OSP parameters with values. These statements are used to make a list of output symbols of a transition of the FSM. Specifically, if an assignment consists of OSP parameters in terms of ISP parameters, we cannot assign the value to the OSP parameters at this stage. The traces which contain the input values will be processed in the main analysis phase only. Procedure 4.1: for each transition do if ISP (or OSP) exists,  138  APPENDIX D. HIGH-LEVEL DESCRIPTION OF IMPLEMENTATION ^139  find pointer of the ISP (or OSP) in ASN.1 Type Tree. make list of the transitions containing all ISP (or OSP) parameters and their types. fi od Procedure 4.2: for each transition do /* construct input of FSM using "PROVIDED" clause of Estelle.Y */ if every predicate consists of ISP parameters with value and operators such as "EQUAL" and "AND", assign values to the field in the list created in Procedure 4.1. set "input.processed" flag of the field in the list to "YES". fi /* construct output of FSM using statements of Estelle.Y */ for every statement, do if an assignment consists of OSP parameters with value, assign values to the fields in the list created in Procedure 4.1. set "output.processed" flag of the field in the list to "YES ". fi od od  D.2 Main Analysis Phase For simplicity, and in order to make the implementation fast and efficient without diminishing practicality, we assume that the trace analysis starts in the initial state. In Procedure 4.3, we analyze traces with respect to the PDS of Estelle specifications. The data structure "Paths" contains information such as data structures on a number of transitions and to_state of each transition with respect to the same from_state. Also, the current pointers of traces being processed, called "numofio_processed", are kept in order to process the correct trace from the trace file. typedef struct path  APPENDIX D. HIGH-LEVEL DESCRIPTION OF IMPLEMENTATION ^140  {  int numofio_processed; PDSTATE from_state; PDTRANS trans it ion [MAX+1] ; PDSTATE to_state [MAX+1] ; } PATH, *PPATH; typedef struct ppathlist {  PPATH ppaths [MAX+1] ; } PATHLIST , *PPATHLIST; PPATHLIST Paths [2] ; The states from_state and to.state defined in "Paths" contain the environment for values of related variables and all candidate transitions at these states. For each candidate transition, the values of variables and service primitives from the trace are substituted to the symbolic representation of PDS using Procedure 4.4. If the predicate and the output primitives of a transition resulting from Procedure 4.4 are satisfied in a trace, we can say that the trace conforms to the formal specification. Procedure 4.3: initialize Paths(from.state, transition, to_state) with from_state as initial state and "numofio_processed" as "0". set variables at from_state by their types and values from PDS. find a set of transitions given by PDS at initial state excluding transitions not satisfying  ISPs, OSPs, and their parameters in the list created in the preprocessing phase with respect to a trace corresponding to "numofio_processed". while(1) do while(if there is an unprocessed path) do while(if there is an unprocessed transition at from_state) do apply Procedure 4.4 to the transition with from_state and to_state. if the above is "YES",  APPENDIX D. HIGH-LEVEL DESCRIPTION OF IMPLEMENTATION ^141  increment "numofio_processed" and log the status. fi od od copy the "Paths" containing "numofio_processed", to_state, values of variables and a set of transitions at the from.state to new "Paths". if no transitions in the new "Paths", if the "numofio_processed" is less than the number of traces in files, echo "traces not conform". stop. else echo "no more traces exist. traces conform". stop.  fi fi od Traces not conforming to the formal specifications are those whose predicates are not satisfied and/or whose inputs and/or outputs do not match with those given in the specification. Note that for spontaneous transitions, the "numofio_processed" pointer will not change. Procedure 4.4(from_state, transition, to state, numofio_processed):  assign values of ISP and OSP parameters to the transition. set to_state by "TO" state of the transition. copy values of variables at the from.state to the to.state. if symbolic simulation on predicates in the "PROVIDED" clause is false, return. fi if the values of the variables obtained from symbolic simulation are the same as the  OSP parameters, save the values to to_state. else return.  APPENDIX D. HIGH-LEVEL DESCRIPTION OF IMPLEMENTATION ^142  fi find a set of transitions given by PDS at to.state excluding transitions not satisfying ISP,  OSPs, and their parameters in the list created in the preprocessing phase with respect to a trace corresponding to "numofio_processed" and store those transitions in "Paths". if the transition is not spontaneous, return (YES). fi  Appendix E  Ada Program having Data Races procedure ex is v : integer := 1; task type one is entry connect; entry disconnect; end; o:one; task type two is entry connect; entry disconnect; end; t:two; task body one is begin loop t.connect; if ( v mod 2 > 0) then delay 1.0; end if; v:= v + 1; accept disconnect; end loop;  143  APPENDIX E. ADA PROGRAM HAVING DATA RACES ^  end one; task body two is begin loop accept connect; if ( v mod 3 > 0) then delay 1.0; end if; v:= v + 1; o.disconnect; end loop; end two; begin null; end ex ;  To  Tt Concurrency Block  V:=V+1;  V:=V+ 1;  Concurrency Block  v:=v+ 1;  v:=v+1;  Figure E.1: Time-event Sequence Diagram  144  Appendix F  ASN.1 Specification of X.25 LAPB LAPB DEFINITIONS ::= BEGIN LapbToMlp ::= CHOICE { ConReq, DiscReq, ResetReq, DataReq, Con Ind, Disclnd, ResetInd, Datalnd, Acklnd } ConReq ::= SEQUENCE {  dummy INTEGER } DiscReq ::= SEQUENCE  145  APPENDIX F. ASN.1 SPECIFICATION OF X.25 LAPB ^  dummy INTEGER } ResetReq ::= SEQUENCE { dummy INTEGER } DataReq ::= SEQUENCE { datano INTEGER Conlnd ::= SEQUENCE {  dummy INTEGER } Disclnd ::= SEQUENCE { dummy INTEGER } Resetlnd ::= SEQUENCE { dummy INTEGER }  Datalnd ::= SEQUENCE { datano INTEGER } Acklnd ::= SEQUENCE { dummy INTEGER } LapbToPhy ::= CHOICE { DataRequest, Datalndicat  146  APPENDIX F. ASN.1 SPECIFICATION OF X.25 LAPB ^  DataRequest ::= SEQUENCE { address INTEGER, frametype INTEGER, ns INTEGER, pf INTEGER, nrINTEGER, udataINTEGER } Datalndicat ::= SEQUENCE { address INTEGER, frametypeINTEGER, nsINTEGER, pfINTEGER, nrINTEGER, udataINTEGER }  Pdu ::= CHOICE { Filler } Filler ::=SEQUENCE { dummy INTEGER } END  147  Appendix G  Estelle.Y Specification of X.25 LAPB specification DataLink; CONST N2 = 6: int; k = 8: int; Modulus = 8: int; A = 0: int; B = 1: int; I = 0: int; RR = 1: int; RNR = 2: int;  REJ = 3: int; SABM = 4: int; DISC = 5: int; UA = 6: int; DM = 7: int; FRMR = 8: int; BAD = 9: int; RetxBuffer = 9: int; VAR  148  APPENDIX G. ESTELLE. Y SPECIFICATION OF X.25 LAPB^  TxAttempts: int; clearrecovery: boolean; oldvs: int; TiRunning: boolean; VS, LastRxNR, Unacked: int; VR, LastTxNR: int; SendingREJ, LocalRNR: boolean; TimerRecovery, RemoteRNR: boolean; Correctack: boolean; useless: int; x: int; tmpframetype: int; tmpnr: int; tmpns: int; tmppf: int; tmpaddress: int; ISP ConReq^mlp_lapb; DiscReq^mlp_lapb; ResetReq^mlp_lapb; DataReq^mlp_lapb; Datalndicat lapb_phy; OSP Conlnd^mlp_lapb; Disclnd^mlp_lapb; ResetInd^mlp_lapb; Datalnd^mlp_lapb; Acklnd^mlp_lapb; DataRequest labp_phy; PDU Filler sent_in lapb_phy;  149  APPENDIX G. ESTELLE. Y SPECIFICATION OF X.25 LAPB^  TIMER T1^2000; T2^1000;  STATE SEND_DM, SEND_SABM, ABM, ABMONE, WAIT_SABM, SEND_DISC;  INITIALIZATION TO SEND_DM BEGIN TxAttempts := 0; END; TRANS FROM SEND_DM TO SEND_SABM WHEN ConReq OUTPUT DataRequest BEGIN DataRequest.frametype := SABM; DataRequest.pf := 1; DataRequest.address := B; TxAttempts := 0; END; FROM SEND_DM TO ABM WHEN Datalndicat PROVIDED (DataIndicat.frametype = SABM) OUTPUT DataRequest, Conlnd BEGIN  150  APPENDIX G. ESTELLE. Y SPECIFICATION OF X.25 LAPB^  DataRequest.frametype := UA; DataRequest.pf:= DataIndicat.pf; DataRequest.address := A; VS := 0; LastRxNR := 0; Unacked := 0; VR := 0; LastTxNR := 0; SendingREJ := false; LocalRNR := false; TimerRecovery := false; RemoteRNR := false; TxAttempts := 0; END; TO SEND_DM WHEN Datalndicat PROVIDED (Datalndicat.frametype = DISC) OUTPUT DataRequest BEGIN DataRequest.frametype := DM; DataRequest.pf:= DataIndicat.pf; DataRequest.address := A; TxAttempts := 0; END; TO SEND_SABM WHEN Datalndicat PROVIDED (DataIndicat.frametype = DM) OUTPUT DataRequest BEGIN DataRequest.frametype := SABM; DataRequest.pf := 1; DataRequest.address := B;  151  APPENDIX G. ESTELLE. Y SPECIFICATION OF X.25 LAPB^  TxAttempts := 0;  END; TO SEND_DM WHEN Datalndicat PROVIDED (Datalndicat.frametype = I) AND(Datalndicat.address = A) AND (Datalndicat.pf = 1) OUTPUT DataRequest BEGIN DataRequest.frametype := DM; DataRequest.pf := 1; DataRequest.address := A; END; TO SEND_DM WHEN Datalndicat PROVIDED (Datalndicat.frametype = RR) AND(Datalndicat.address = A) AND (Datalndicat.pf = 1) OUTPUT DataRequest BEGIN DataRequest.frametype := DM; DataRequest.pf := 1; DataRequest.address := A; END;  •  FROM ABM TO ABM WHEN Datalndicat PROVIDED (Datalndicat.frametype = I) AND (Datalndicat.nr = LastRxNR) AND (LocalRNR=false) AND (Datalndicat.ns = VR) AND (Datalndicat.pf = 0) OUTPUT DataInd  152  APPENDIX G. ESTELLE. Y SPECIFICATION OF X.25 LAPB ^  BEGIN SendingREJ := false; VR := (VR + 1) mod Modulus; END; TO ABMONE WHEN Datalndicat PROVIDED (DataIndicat.frametype = I) AND (DataIndicat.nr <> LastRxNR) AND (TimerRecovery = false) OUTPUT Acklnd BEGIN LastRxNR := (LastRxNR + 1) mod Modulus; Unacked := (VS + Modulus - LastRxNR) mod Modulus; TxAttempts := 0; tmpframetype := I; tmpnr := Datalndicat.nr; tmpns := Datalndicat.ns; tmppf := Datalndicat.pf; END; FROM ABMONE TO ABMONE PROVIDED (tmpnr <> LastRxNR) OUTPUT Acklnd BEGIN LastRxNR := (LastRxNR + 1) mod Modulus; Unacked := (VS + Modulus - LastRxNR) mod Modulus; TxAttempts := 0; END; FROM ABMONE TO ABM PROVIDED (tmpnr = LastRxNR) AND LocalRNR AND (tmppf <> 1)  153  APPENDIX G. ESTELLE. Y SPECIFICATION OF X.25 LAPB^  BEGIN useless := 0;  END; FROM ABMONE TO ABM PROVIDED (tmpnr = LastRxNR) AND Loca1RNR AND (tmppf = 1) OUTPUT DataRequest BEGIN DataRequest.frametype := RNR; DataRequest.pf := 1; DataRequest.nr := VR; DataRequest.address := A; LastTxNR := VR; END;  FROM SEND_DISC TO SEND_DISC PROVIDED TxAttempts <= N2 OUTPUT DataRequest BEGIN Start(T1); DataRequest.frametype := DISC; DataRequest.pf := 1; DataRequest.address := B; TxAttempts := TxAttempts + 1 END;  END.  154  Appendix H  Estelle Specification of Dinning Philosophers  /* this Estelle specification was written by Limin Zhu, June 1991 */ MODULE philoso PROCESS (id : lable); IP Rp: phil_fork(ch_phil) INDIVIDUAL QUEUE; Lp: phil_fork(ch_phil) INDIVIDUAL QUEUE; T: room_phil(ph) INDIVIDUAL QUEUE;  END; BODY philoso_body FOR philoso;  TRANS WHEN T.ok FROM Room_Enter TO Left_Pick BEGIN OUTPUT Lp.pick; printleft_pick(id); END; TRANS WHEN Lp.fork_provided  155  APPENDIX H. ESTELLE SPECIFICATION OF DINNING PHILOSOPHERS^156  FROM Left_Pick TO Right_Pick BEGIN OUTPUT Rp.pick; printright_pick(id); END; TRANS WHEN Rp.fork_provided FROM Right_Pick TO Eating BEGIN printeating(id); End;  MODULE fork PROCESS (f_id : lable); IP R: phil_fork(ch_fork) INDIVIDUAL QUEUE; L: phil_fork(ch_fork) INDIVIDUAL QUEUE; END; BODY fork body FOR fork;  TRANS WHEN R.pick FROM Available TO Taken BEGIN OUTPUT R.fork_provided; END;  TRANS WHEN L.pick FROM Available TO Taken  APPENDIX H. ESTELLE SPECIFICATION OF DINNING PHILOSOPHERS ^157  BEGIN OUTPUT L.fork_provided; printleftforktaken(f_id); END;  

Cite

Citation Scheme:

        

Citations by CSL (citeproc-js)

Usage Statistics

Share

Embed

Customize your widget with the following options, then copy and paste the code below into the HTML of your page to embed this item in your website.
                        
                            <div id="ubcOpenCollectionsWidgetDisplay">
                            <script id="ubcOpenCollectionsWidget"
                            src="{[{embed.src}]}"
                            data-item="{[{embed.item}]}"
                            data-collection="{[{embed.collection}]}"
                            data-metadata="{[{embed.showMetadata}]}"
                            data-width="{[{embed.width}]}"
                            async >
                            </script>
                            </div>
                        
                    
IIIF logo Our image viewer uses the IIIF 2.0 standard. To load this item in other compatible viewers, use this url:
http://iiif.library.ubc.ca/presentation/dsp.831.1-0051350/manifest

Comment

Related Items