Trace Analysis of Protocols based onFormal Concurrent SpecificationsbyMYUNGCHUL KIMB.Sc. Ajou University, Korea, 1982M.Sc. Korea Advanced Institute of Science and Technology, Korea, 1984A THESIS SUBMITTED IN PARTIAL FULFILLMENT OFTHE REQUIREMENTS FOR THE DEGREE OFDOCTOR OF PHILOSOPHYinTHE FACULTY OF GRADUATE STUDIES(DEPARTMENT OF COMPUTER SCIENCE)We accept this thesis as conformingto the required standardTHE UNIVERSITY OF BRITISH COLUMBIADecember 1992©MyungChul Kim, 1992In presenting this thesis in partial fulfilment of the requirements for an advanceddegree at the University of British Columbia, I agree that the Library shall make itfreely available for reference and study. I further agree that permission for extensivecopying of this thesis for scholarly purposes may be granted by the head of mydepartment or by his or her representatives. It is understood that copying orpublication of this thesis for financial gain shall not be allowed without my writtenpermission.(Signature) Department ofThe University of British ColumbiaVancouver, CanadaDate )e c 22 - /1j2 DE-6 (2/88)AbstractTo increase the probability of computers communicating reliably with one another, protocolimplementations must be tested for conformance to the standards on which they are based. Testcase generation and trace analysis are two important topics in protocol testing research. Mostof 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 traceanalysis in a unified framework is presented. The model, which is based on single moduleextended finite state machines, handles both control and data flows for single module specifica-tions. 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 ordermessage sequences, are also addressed. A prototype implementation of the unified model wascompleted. The application of this method to X.25 LAPB shows that it can manage framecollision and control and data flows of the protocol rigorously.The model is extended to study the trace analysis of concurrent specifications based onmulti-module extended finite state machines. This is done by introducing two additional models- concurrency and traceability. The concurrency model deals with concurrent properties suchas concurrent events, concurrency blocks, global states, concurrency measures, deadlocks anddataraces which do not arise in sequential or single module specifications. The concurrencymodel allows a high-level abstraction to be used for understanding and analyzing concurrentbehaviors. We also show how concurrency measures can be computed efficiently based on theconcept of concurrency blocks. The traceability concept is needed to obtain the precise orderof input/output messages of a module without state space explosion. This model for the traceanalysis of concurrent specifications without translating them into their sequential equivalenceis formalized and proposed for application to multi-module specification, multi-party testingand interoperability testing.The viability of the proposed methodology which can be applied to any specifications basedon extended finite state machines is demonstrated using Estelle specifications in the thesis.iiContentsAbstract^ iiContents iiiList of Tables^ viList of Figures viiTerms and Acronyms^ viiiAcknowledgement ix1 Introduction 11.1 Motivation ^ 21.2 Thesis Statements ^ 41.3 Summary of Contributions ^ 51.4 Thesis Organization 62 Background 72.1 Conformance Testing ^ 72.2 Estelle ^ 102.3 Concurrency ^ 123 Trace Analysis based on Formal Specifications 153.1 Related Work ^ 163.2 Experiments on Finite State Machines ^ 193.3 Unified Model for Trace Analysis and Test Case Generation ^ 213.4 Trace Analysis in External Test Architectures ^ 283.5 A Case Study - The X.25 LAPB Protocol 303.6 Test Case Generation and Validation ^ 363.7 Chapter Summary ^ 39iii4 Implementation of Trace Analyzer 404.1 Brief Description of Tools ^ 404.1.1^Estelle.Y with ASN.1 414.1.2^Translation from Estelle to Estelle.Y ^ 424.1.3^Protocol Data Structure ^ 434.1.4^TESTGEN Parser 434.2 Implementation Issues ^ 434.2.1^Known Initial State 434.2.2^Unfolding Loops 444.2.3^Transitions with Timers ^ 474.2.4^Preprocessing Phase 494.2.5^Search Method ^ 504.2.6^Pruning Candidate Transitions ^ 514.2.7^Verdict and Location of Errors 514.3 Sample Experiments ^ 534.3.1^Cases 1 and 2 534.3.2^Case 3 ^ 564.3.3^Case 4 574.3.4^Performance ^ 604.4 Future Work ^ 615 Concurrency Model 635.1 Formal Concurrency Model ^ 635.1.1^Synchronous and Asynchronous Communications ^ 645.1.2^Concurrency Checking 675.1.3^Global Synchronization Cut ^ 695.1.4^Concurrency Measures 855.2 Application to Estelle Specifications 895.3 Application to LOTOS Specifications ^ 905.4 Application to Ada Programs ^ 905.5 Chapter Summary ^ 916 Trace Analysis based on Concurrent Specifications 936.1 The Basic Blocks ^ 946.1.1^Trace Analysis based on Single-Module Specifications ^ 956.1.2^Concurrency Model ^ 966.1.3^Traceability ^ 966.2 Formal Model 996.3 Applications ^ 1016.3.1^Trace Analysis based on Multi-module Specifications ^ 1026.3.2^Message Collisions in Multiple Party and Interoperability Testings 1036.4 Case Study ^ 105iv6.5 Chapter Summary ^ 1077 Conclusions and Future Research^ 1097.1 Summary of Results ^ 1097.2 Future Research 111Bibliography^ 112A Estelle Specification of X.25 LAPB^ 119B Applying Procedure 1 in Section 3.3 to X.25 LAPB^ 131C Flowchart for Example 2 in Section 3.5^ 133D High-level Description of Implementation 137D.1 Preprocessing Phase ^ 137D.2 Main Analysis Phase 138E Ada Program having Data Races^ 142F ASN.1 Specification of X.25 LAPB 144G Estelle.Y Specification of X.25 LAPB^ 147H Estelle Specification of Dinning Philosophers^ 154List of Tables4.1 Performance of the trace analysis (time unit: second) ^ 61viList of Figures2.1 OSI Reference Model. ^ 82.2 Abstract Test Architecture. 93.1 Sequence of Events in Traces ^ 333.2 Test Case Generation and Trace Analysis ^ 374.1 Overall Structure of Trace Analyzer 414.2 Corresponding Finite State Machine^ 504.3 Data Structure for Nondeterminism . 525.1 Time-event Sequence Diagrams and Their Corresponding DAGs^ 655.2 Examples of Global Synchronization Cuts ^ 705.3 Examples of Global Synchronization Cuts 765.4 Examples of Global Synchronization Cuts 785.5 Examples of Global Synchronization Cuts ^ 825.6 Types of Deadlocks ^ 896.1 Basic Blocks^ 956.2 Points of Observation ^ 956.3 Trace Analysis based on Concurrent Specifications ^ 1006.4 Application ^ 1036.5 Module Structure 105E.1 Time-event Sequence Diagram ^ 143viiTerms and AcronymsACE^Asynchronous Communication EventASN.1 Abstract Syntax Notation OneASP^Abstract Service PrimitiveBGSC Backward Global Synchronization CutCCITT^International Telegraph and Telephone Consultative CommitteeDAG Directed Acyclic GraphDCE^Data Circuit-terminating EquipmentDTE Data Terminal EquipmentEFSM^Extended Finite State MachineETS Extended Transition SystemFDT^Formal Description TechniqueFSM Finite State MachineFGSC^Forward Global Synchronization CutGSC Global Synchronization CutISDN^Integrated Services Digital NetworkISO International Organization for StandardizationISP^Input Service PrimitiveIUT Implementation Under TestLAPB^Link Access Procedure BLOTOS Language of Temporal Ordering SpecificationLT^Lower TesterNFS Normal Form SpecificationOSI^Open Systems InterconnectionOSP Output Service PrimitivePCO^Points of Control and ObservationPDS Protocol Data StructurePDU^Protocol Data UnitPO Points of ObservationPOT^Port of Observation for TraceabilitySAP Service Access PointSCE^Synchronous Communication EventSUT System Under TestTAP^Test Access PortTTCN Tree and Tabular Combined NotationUT^Upper TesterX.25 Packet-switching protocol and standard (CCITT and ISO)viiiAcknowledgementI 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 encouragementwhich helped me in gaining confidence in myself, and their guidance which taught me how toconduct scientific research. Especially regular meetings with Dr. Chanson at every two weekshad 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 hisinsightful comments and suggestions. I appreciate Dr. Paul Amer at the University of Delawarefor his serving as the external examiner. Thanks to Dr. Gregor v. Bochmann at the Universityof Montreal and Dr. Robert L. Probert at the University of Ottawa for their valuable commentsand 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 ofProtocol Engineering Group: Antonio Loureiro, Sijian Zhang, Jadranka Alilovic-Curgus, Kai-chung 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 andinformation exchange. Thanks to Christopher Healey for carefully reading this thesis andmaking corrections. Thanks to Peter Phillips for helping installing tools and fixing problems ofthe tools during my studying.I would never become what I am without the unconditional love, understanding and supportfrom my parents and parents-in-law. Their phone calls from home have always been a constantsource of strength and encouragement. Thanks to Mr. and Mrs. David C. Lee for their guidingto be acquainted with lives in Vancouver, Mrs. Eun Soon Kim for her constant encouragementand introducing to Jesus Christ, and Mr. and Mrs. Hee Chang Choi for their emotional supportand sending magazines. Above all, special thanks to my beautiful daughter Eunah and my wifeKyung Og. It is beyond the power of words to express my debt to the person closest to myheart, Kyung Og, for her patience, her encouragement, and her endless love. I can not imaginewhat it would have been like without her.The research of this dissertation was supported by Korea Telecom Overseas Studying Fel-lowship and in part supported by the Canadian Institute for Telecommunications Researchunder the NCE program of the Government of Canada.ixChapter 1IntroductionThe International Organization for Standardization (ISO) and International Telegraph andTelephone Consultative Committee (CCITT) have been standardizing computer communicationprotocols within the framework of the Open Systems Interconnection (OSI) reference model[Tanen 881. Any systems implemented according to the same OSI protocol standard shouldbe able to communicate with one another. Unfortunately, the standards documents written inEnglish 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 confor-mance testing procedures [ISOb]. These are to be carried out on a given protocol implementa-tion to ensure that it conforms to the appropriate protocol standards. The testing proceduresare to be performed by any one of a number of recognized test laboratories. After a protocolimplementation has passed the tests, it is given a certification of approval. Customers may thenuse the protocol implementation with at least some confidence of compatibility. The client forwhom the laboratory performs the conformance tests may be the vendor of the implementation1CHAPTER 1. INTRODUCTION^ 2or a potential customer. In either case, the test laboratory has little or no knowledge of theinternal workings of the System Under Test (SUT) which contains the Implementation UnderTest (IUT). The conformance testing process treats the IUT as a black box; only its externalbehavior is observed.1.1 MotivationResearch activities in protocol testing can be roughly divided into test case generation andtrace analysis [Bochm 89]. However, as in the case for software testing, most of the work hasbeen 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 andLOTOS are designed to avoid the ambiguity of standard documents written in English. Justas there are formal description techniques for protocol specification, CCITT and ISO havejointly 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 TTCNconsists of a collection of tables defining the different aspects of the test cases such as serviceprimitives, Protocol Data Units (PDU's) and their parameters, constraints on parameter valuesand dynamic behaviors (interactions). The interaction order is defined in terms of a tree whereeach branch from the root to a leaf represents a possible execution sequence. A TTCN testcase contains the trace analysis function by expressing verdicts explicitly. This approach givesrise to issues such as how to generate, validate, and manage test suites. Currently, most of theCHAPTER 1. INTRODUCTIONtest cases in use have been created manually in an informal manner.Recently researchers have been investigating the related goals of generating test suites sys-tematically from formal protocol specifications (e.g., [Ural 87, Sarik 87]), and validating TTCNtest 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 streamsexchanged between two protocol entities conform to the formal protocol specification. Eventhough the approach is most suitable for trace analysis, it can be used for test case valida-tion [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 acommon framework.So far, few people have taken advantage of the close relationship between test case generationand trace analysis. No one has tried to apply the large body of research results in softwaretest case generation (or, for that matter, in protocol test case generation) to protocol traceanalysis. Finally, there has been no attempt to build one system to generate test cases andanalyze traces with respect to formal protocol specifications using a unified framework. Eventhough the constraints on test case generation and trace analysis procedures are different, someof the techniques used in test case generation for software testing (e.g., static data flow analysisand symbolic evaluation) can be used to augment the generality, correctness and diagnostics oftrace analysis.Until now, work on test case generation and trace analysis has mostly been performed inCHAPTER 1. INTRODUCTION^ 4a sequential context even though the specifications are concurrent. In general, formal protocolspecification languages such as Estelle and LOTOS allow one to specify multiple modulesor multiple processes. Most work on the automatic test case generation and trace analysiswith respect to Estelle [Sarik 87, Ural 87, Chun 90, Kim 91] assumes a preprocessing stageto 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 communicationsbetween modules. During this process, we may lose semantics on deadlocks and data racesand encounter the state space explosion problem. Furthermore, after the translation, it maybe difficult to relate the errors detected in trace analysis with respect to the single modulespecification to corresponding errors in the implementation. For example, a deadlock may bemistaken as an underspecification with respect to the single module specification derived froma concurrent specification. One of the main problems in analyzing multiple concurrent modulesis determining the order of events globally. This could easily lead to state space explosion. Webelieve 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 StatementsIn this thesis, we present a model that combines the functions of test case generation and traceanalysis in a unified framework. Our model handles both control and data flows. Symbolicevaluation is used to detect and delete infeasible paths which may be the results of path se-lection. Practical considerations such as out of order message sequences that may occur in aCHAPTER 1. INTRODUCTION^ 5real test environment are also addressed. The application of this method to the trace anal-ysis of X.25 LAPB shows that it can manage frame collision, control and data flows of theprotocol rigorously [Kim 91]. A prototype of the trace analyzer based on the unified modelwas implemented and applied to the X.25 LAPB protocol to demonstrate the feasibility of themodel.In order to extend trace analysis to the concurrent environment, models of concurrencyand traceability have been developed. The concurrency model [Kim 92a] deals with concur-rent properties such as concurrent events, concurrency blocks, global states, concurrency mea-sures, communication deadlocks and data races. The concurrency model allows a high-levelabstraction to be used for understanding the concurrent behaviors. We show how to computeconcurrency measures efficiently based on the concept of concurrency blocks. The traceabilityconcept is needed to obtain the precise order on input/output messages of a module in orderto avoid state space explosion. This can occur when applying single module trace analysis tomodules with multiple ports. This model for the trace analysis of concurrent specifications isformalized and proposed for application to concurrent specifications, multi-party testing andinteroperability testing.1.3 Summary of ContributionsThe major contributions of this thesis are fourfold:1. A unified model for test case generation and trace analysis based on the extended finitestate machine has been developed.CHAPTER 1. INTRODUCTION^ 62. A prototype implementation of the trace analyzer in the unified model and the applicationof the prototype to X.25 LAPB have been completed to demonstrate the feasibility ofthe model.3. A concurrency model has been developed which gives elegant definitions and computationsof concurrent events, concurrency blocks, global states, concurrency measures, deadlocksand dataraces.4. A methodology for trace analysis with respect to concurrent specifications has been devel-oped based on the trace analysis model in 1, the concurrency model in 3 and the conceptof traceability to eliminate state space explosion.1.4 Thesis OrganizationThe remainder of the thesis is organized as follows. Chapter 2 provides background informationon the notions of conformance testing, formal description techniques for protocols, and concur-rency. Chapter 3 presents a unified framework for test case generation and trace analysis basedon the extended finite state machine. A prototype implementation of the trace analyzer basedon the unified model in Chapter 3 is described in Chapter 4. A concurrency model is presentedin Chapter 5 which gives elegant and efficient definitions with respect to concurrent specifi-cations. Chapter 6 discusses trace analysis with respect to concurrent specifications. Finally,Chapter 7 concludes the thesis and outlines some future work.Chapter 2BackgroundIn this chapter, the basic concepts of conformance testing and the Estelle formal descriptiontechnique 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 Estelleformal description technique. Some basic notions of concurrency are also given.2.1 Conformance TestingThe testing process can be divided into diagnostic testing and conformance testing. Diagnostictesting is carried out by the implementor and is aimed at determining whether the implemen-tation is working correctly according to the implementor's intention. This is based on theprotocol standards and the implementation design documents. On the other hand, the mainobjective of conformance testing is to determine if an implementation conforms to the protocolstandards in order to enhance interoperability. The diagnostic testing process treats the Imple-mentation 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 behavior7(N-1)-Service Providerr(N+1)-Entity(N+1)-Entity(N)-PDUs^(N)-Entity(N)-EntityA(N-1)-ASPsA(N-1)-ASPsA (N)-ASPsVN)-ASPsCHAPTER 2. BACKGROUND^ 8is observed.The seven-layer OSI reference model has been defined by ISO to describe the interconnec-tion 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 inFigure 2.1.(N)-Service ProviderFigure 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 implementationssince the implementation details are isolated. Two peer (N)-Entities use (N)-Protocol DataUnits (PDUs) to communicate with each other through an (N-1)-Service provider. A protocolis 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-(N)Entity> JUT(N-1)-ASPsACHAPTER 2. BACKGROUND^ 91)- Abstract Service Primitives (ASPs), respectively. The points where an implementationcan be controlled and observed are called the Points of Control and Observation (PCO). Theimplementation is not accessible otherwise. During conformance testing, the ASPs and PDUsthat are defined as inputs are sent to the (N)-Entity implementation and the ASPs and PDUsgenerated by the implementation are observed and compared to the permissable outputs. Thisapproach 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 majorcomponents. An abstract test architecture (see Figure 2.2) defines the functionalities of thesecomponents without giving any implementation details.UpperTesterTest Management PDUs (N+1)-Entity(N)-ASPsLowerTester(N)-PDUs(N-1)-ASPs(N-1)-Service ProviderFigure 2.2: Abstract Test Architecture.The Lower Tester (LT) is responsible for the control and observation at the PCO belowthe 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. TheCHAPTER 2. BACKGROUND^ 10test events (i.e., atomic interactions between the IUT and an upper or lower tester) used inconformance testing are described in an abstract conformance test suite. The tests in a testsuite are organized in a hierarchical structure. The key level, called the test case, is based on anarrowly defined test purpose. The test purpose describes the objective of the test. There arethree 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 PDUexchanges needed to verify the new state of the IUT are also part of the test body. The testpostamble is used to put the IUT into a stable state after the test body is run. Also it is usedto check the destination state of the test case. An abstract test notation, called the Tree andTabular Combined Notation (TTCN) [ISOb], is defined to represent the abstract test suites ina standard fashion.2.2 EstelleEstelle is a formal description technique (FDT) for specifying distributed concurrent systems,in particular communication protocols and services. It is based on an extended state transitionmodel, specifically, a model of a nondeterministic automaton extended with elements of thePascal language.A distributed system in Estelle is composed of several communicating components calledmodules. A module is specified by a module definition which may include definitions of othermodules. When applied repeatedly, this leads to a hierarchical tree structure of module defini-CHAPTER 2. BACKGROUND^ 11tions. There are attributing principles that play an important role in defining the behavior ofa 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 calledinteraction points. A channel which defines two sets of interactions is associated with eachinteraction point. These two sets consist of interactions which can be sent or received throughthis interaction point.There are two communication mechanisms in Estelle: message exchange and restrictedsharing of variables. First, a module instance can always send an interaction. This principleis called asynchronous communication. An interaction received by a module at its interactionpoint 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 tobe 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 theexecution of the parent's actions always has priority.The internal dynamic behavior of an Estelle specification is characterized in terms of a non-deterministic state transition system. The execution of a transition by a module is consideredto be an atomic operation. A state in Estelle is, in general, a complex structure composed ofmany components such as value of the control state, values of variables and contents of FIFOqueues associated with the interaction points.CHAPTER 2. BACKGROUND^ 122.3 ConcurrencyConcurrent behaviors in distributed systems are difficult to specify and analyze. The ISOhas developed two formal description techniques, Estelle and LOTOS [ISOc, ISOd], for thespecification 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 specificationconsists of nested processes. The processes may share gates through which communication oc-curs. 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 interac-tion. This occurs when they specify the same gate and compatible sorts. A process that offersto receive will wait for a matching send to occur. Similarly, a process that offers to send mustwait until the matching receive is executed. Unlike Estelle, there is no other communicationmechanism in LOTOS.Since Lamport's pioneering work [Lampo 78], there has been considerable research on con-currency, logical clocks and global states in distributed systems. Charron-Bost[Charro 89] pro-posed concurrency measures based on a logical clock[Matte 89, Fidge 91]. The logical clock isused to determine whether or not two events are concurrent. A concurrency relation is thenused to compute global states and concurrency measures. The concurrency measure is definedas the ratio of the possible number of concurrent events in the system over the number ofCHAPTER 2. BACKGROUND^ 13concurrent events in a similar system where all the tasks are totally concurrent (i.e. no taskshave communication events) [Charro 89]. This scheme can be extended to detect data races. Adata race occurs when two or more concurrent events, at least one of which is a write, accessthe same shared variable. In this case, the value of the variable is not predictable since it isdependent on the order of execution.With the emergence of concurrent languages such as Ada, Modula II and Occam, therehas been growing interest in concurrent program debugging. Debugging concurrent programsis 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 relatedwith lower level parallel programs such as Parallel Fortran, which deal with parallel opera-tions or instructions [Choi 91, Mille 88], have focused on shared memory accesses. The formeraims to determine whether the number, order, and semantics of communication statements areproper. The latter tries to detect data race conditions in the interactions of communicatingtasks through shared memory.The classes of communication deadlocks that can occur depend on the communicationparadigms supported by the programming system. The classification of deadlocks is impor-tant in measuring the coverage of deadlock detection algorithms. For example, Cheng showedthat a number of proposed techniques [Helmb 85, Young 88] could not detect the complete classof synchronous communication deadlocks in Ada [Cheng 90]. Cheng's classification is based onCHAPTER 2. BACKGROUND^ 14five different types of waiting relations among tasks in Ada [Ada 83].It is interesting to compare debugging of concurrent programa[Mcdow 89] with trace anal-ysis based on concurrent specifications. The former works on white box representation of theimplementation to detect and locate errors and the latter works on a black box or grey boxrepresentation of an implementation for ensuring conformance of external behaviors (traces) tospecifications.Other related work includes static concurrency analysis of a path selection mechanism forsymbolic execution as a pruning mechanism for concurrency analysis[Young 88]. Also, Weissprovided a formal foundation for a theory of concurrent program testing by representing aconcurrent program as a set of sequential programs [Weiss 88].Chapter 3Trace Analysis based on FormalSpecificationsIn this chapter, we describe the design of a unified model for test case generation and traceanalysis. The unified model can be applied to any formal description techniques (FDTs) basedon extended finite state machines (EFSMs). The trace analysis of the unified model is performedusing a two phase scheme: a path selection phase based on the control flow (with or withoutdata flow) of the EFSM followed by an infeasible path detection and deletion phase usingsymbolic 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 workwith 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 generationfunctions using common functionalities and the same system view.15CHAPTER 3. TRACE ANALYSIS BASED ON FORMAL SPECIFICATIONS^16• Correctness: infeasible paths are detected and eliminated by detecting inconsistencies inthe path conditions using symbolic evaluation.• Error Identification: the analyzer should help to identify the cause of errors when theyoccur.• Practicality: the system should be able to handle real life protocols and testing environ-ments.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. InSection 3.3, our model based on extended finite state machines is presented. The relationshipbetween extended finite state machines and finite state machines is given. The model is extendedto different test architectures in Section 3.4, and illustrated using X.25 LAPB as a case studyin Section 3.5. We discuss the relationship between trace analysis and test case generation inSection 3.6 and outline how the model can be used to generate and validate test cases. FinallySection 3.7 summarizes the work.3.1 Related WorkUral presented the concepts of protocol trace analysis [Ural 86]. The work was designed tovalidate a protocol implementation, SFR_K (System Functionality Representative_K), accordingto the protocol specification SFR_K - I. The SFR_K - 1 is assumed to be acceptable as areference for consistency checking. In trace checking, SFR_K - 1 is employed as a test oracleCHAPTER 3. TRACE ANALYSIS BASED ON FORMAL SPECIFICATIONS^17which determines whether or not an observed trace of SFR_K is permissible. In trajectorychecking, all allowed responses to a stimulus are included in a tree-structured trajectory. Thepaper [Ural 86] proposes that a Prolog procedure implementing an abstract SFR_K based onEstelle can be used as a generator to produce interaction sequences and as a validator to checkobserved interaction sequences. This requires Estelle specifications to be translated into SFRsin Prolog and the SFRs to be capable of reverse execution. However, not all Prolog programsare reversible because of the arithmetic evaluation and depth first search rules of Prolog. Inorder to execute Prolog programs in reverse, the programs have to be structured properly,for example, by checking loops whenever transitions are visited. Furthermore, the automatictranslation of Estelle specifications into Prolog is quite complicated.In the paper by Bochmann [Bochm 90], a test trace analyzer called TETRA was constructedby modifying a LOTOS interpreter. TETRA takes interaction parameters into account anduses backtracking to determine whether the tree of possible execution histories defined by thespecification includes the observed trace of interactions. For nondeterministic choices which arenot directly visible, backtracking is necessary until either a correct path is located or no possiblematch exists. In order to avoid backtracking over all possible paths, the system instantiatesinteraction parameters as late as possible. It waits until their values can be determined from theconstraints of the specification and/or subsequent observed input or output values. Nonethe-less, certain features of LOTOS such as non well-guarded expressions and general CHOICEstatements can easily explode the number of paths that have to be processed. Also, currentlyTETRA cannot be used for test case generation and there are limitations when the behavioralCHAPTER 3. TRACE ANALYSIS BASED ON FORMAL SPECIFICATIONS^18tree of the protocol is too complex.Mockingbird [Gorli 90], on the other hand, can be used as both a generator - producingtest cases whose properties conform to the specification, and an acceptor - validating testcases against the specification. The specification language is a combination of context-freegrammars and constraint systems. The semantics of the specification are based on constraintlogic programming (CLP). However, not all CLPs are reversible because of the possible infiniterecursions generated by the unfair method of rule selection in CLP. The model is not suitablefor real-life protocols.In [Wvong 90] a trace analyzer is used to simplify test cases. Test cases only need to describethe expected behaviors of the protocol implementation. The unexpected behaviors are checkedby 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 symbolicevaluation [King 76, Clark 85] in software engineering. Static data flow techniques require theselection of subpaths based on particular sequences of definitions and references to the variablesin the program without execution. These techniques are used to detect suspicious or erroneoususe of data, such as referencing undefined variables and defining variables without subsequentusage. Symbolic evaluation is a program technique that derives algebraic representations, overthe input values, of the computations and their applicable domains. Thus symbolic evaluationdescribes the relationship between the input data and the resulting values, whereas normalexecution computes numeric values but loses information about the way in which they werederived. Static data flow analysis methods can be used to detect paths containing suspectCHAPTER 3. TRACE ANALYSIS BASED ON FORMAL SPECIFICATIONS^19sequences of events but cannot determine if these paths are executable. Symbolic evaluationcan be used to determine which paths are unexecutable by computing the consistency of pathconditions and thus can greatly simplify the complexity of trace analysis.3.2 Experiments on Finite State MachinesOur approach uses some principles of the finite state machine (FSM) model. The reader isassumed to have a basic knowledge of FSMs. In this section, only the principles and theoriesrelevant 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 com-bination of input symbol, output symbol, present state and next state of an FSM is describedby either a transition table or a transition diagram. An experiment performed on a finite statemachine consists of applying one or more input sequences, observing the corresponding outputsequences, and drawing a conclusion about the internal behavior of the machine. A machine isassumed to be finite, deterministic, reduced, strongly connected, and completely specified, andis available to the experimenter as a black box. This means the experimenter has access to itsinput and output terminals, but cannot inspect the internal structures.The experimenter may have to consider a class of problems, known as measurement andcontrol 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 froma known initial state to a predesignated terminal state. The measurement problem is theCHAPTER 3. TRACE ANALYSIS BASED ON FORMAL SPECIFICATIONS^20identification of the unknown initial state of the machine. The general machine control problemthat brings the machine to a specified final state from an unknown initial state can be viewedas being composed of two distinct subproblems: a measurement problem followed by a simplecontrol problem.Experiments are classified into synchronizing experiments, homing experiments, and distin-guishing experiments according to their purpose [Gill 62, Henni 68]. A synchronizing experimentconsists of the application of a fixed input sequence (or synchronizing sequence) that is guar-anteed to leave the machine in a particular final state. A homing experiment consists of theapplication of either a preset or an adaptively chosen input sequence such that the resulting out-put sequence uniquely specifies the machine's final state. A distinguishing experiment is similarto a homing experiment except that it is used to determine a machine's initial state. The homingexperiment is solvable but not all distinguishing experiments are solvable [Gill 62, Henni 68].Finally synchronizing experiments are dependent on the existence of synchronizing sequencesof machines.Typically, solutions to the measurement and control problem make use of the informationcontained 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 agraphical presentation of the results obtained when different input sequences are applied to themachine. The different paths through this tree correspond to the possible input sequences thatmight be used in an experiment. The nodes of this tree correspond to the possible states thatthe 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 2below 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 statescan always be solved by a simple preset experiment of length Lhs where Lhs < (v —1)(In — 1).The admissible states of machine M refer to the initial states of the machine. A simpleexperiment is one which is performed on a single copy of the machine, and an experiment is presetif all the input sequences are predetermined independent of the outcome of the experiment. Thehoming 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 presetexperiment of length Lhs where Lhs < k(m-1).Two states are k — distinguishable if and only if there exists an input sequence of lengthk that yields one output sequence when the machine is started in one state, and a differentoutput sequence when the machine is started in the other state.3.3 Unified Model for Trace Analysis and Test Case Genera-tionOur model is based on extended finite state machines (EFSM). The extended finite state machineis an abstract model which associates a program segment with each transition instead of simplyCHAPTER 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 inEstelle 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 respectto 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 statesfrom the observed input and output message sequences. Even for FSMs which deal withcontrol 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 anddata 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 thatcomply with the observed sequence of input and output messages. Actually, generatingall test cases can be done efficiently. The problem is in the identification of any infeasiblepaths from the set of paths produced. For example, data flow techniques that attemptto generate only feasible paths by excluding inconsistent branch predicates have beenshown to be NP-complete [Gabow 76]. However, the techniques for the restricted classof 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^233. 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 tracecontains information to determine the actual number of loop iterations, specific values ofparameters, and the outcome of conditional statements. The absence of this informationis largely responsible for the inefficiency in test case generation.We start with an Estelle specification which is supposed to be error-free and conforms tothe standards. Furthermore, the specification is assumed to be a single module, without statesets, 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 transitionexplosion problem that occurs in NFS for complex protocols.Definition 1 A single-module Estelle specification E is defined as a 5-tuple E=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 > where• S is the set of states of F,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 isdefined as eF =< A, Li,B >.Pi , contains interaction service primitives gpi, • • • ,Pn)/0(qi, • • • , qn ) 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 primitiveparameters respectively.The mapping from eE to F is given by the following:if the domain size of every interaction service primitive parameter is small, theneF =< A, Li, B > if Li = I x p l x • • • x p° / 0 x qi x • • • x q° is valid with respect to Pi ,elseSF =< A, Li, B > iff Li = I/O is valid with respect to PiIn other words, when the domain sizes of the parameters are small (i.e., the possible com-binations of parameter values are manageable), the interaction service primitives and theirCHAPTER 3. TRACE ANALYSIS BASED ON FORMAL SPECIFICATIONS^25parameters are enumerated and then included. Otherwise, they are left out to avoid state ex-plosion. In the latter case, symbolic evaluation is used to detect and discard infeasible pathsthat 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 tothe 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 iterationnumber of while loops and transition loops and conditions limiting the domain space of vari-ables and interaction service primitive parameters for Estelle. Since FSMs have no programsegments and do not deal with data and predicates, the constraints C1 of an FSM derivedfrom an Estelle specification E using Procedure 1 is a subset of the constraints Ce of E.Theorem 3 Given finite state machine F obtained from an Estelle specification E using Pro-cedure 1, AllPath(F,Si,S0 ,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 constraintsC, 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 confe X if EXT(M)ITT C EXT(X) whereEXT is the external behavior function.This definition states that an implementation M of a specification X with constraints CCHAPTER 3. TRACE ANALYSIS BASED ON FORMAL SPECIFICATIONS^26passes a conformance test using test case Tc if the external behaviors of the test is a subset ofthe allowable behaviors specified by X.Definition 6 As a generalization of conformance testing in Definition 5, the following defini-tion is useful for trace analysis: M conf X if VC VSi VS0 , M con fc XIf X in Definition 6 is replaced by F of Definition 2, then M conf F turns out to be thehoming problem discussed in Section 3.2. Theorems 1 and 2 give the bound of message lengthto uniquely identify the machine's final state. Thus, after at most Lizs messages, the state ofthe implementation is known and subsequent traces can be determined if they are legal pathsaccording to the specification. The actual length is usually much shorter than the bound givenin 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 finitestate 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 caseof trace analysis. And select from F all the paths from the given initial state to thegiven 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 differencebetween AllPath sets of F and E in Theorem 3 due to reduction of the constraints. An empiricalstudy on the number of feasible versus infeasible paths for several programs using control flowonly [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 resultis not as satisfactory because the method gives only the necessary (not sufficient) condition fordeleting infeasible paths [Podgu 90].There are three basic methods for symbolic evaluation [Clark 85]: path-dependent symbolicevaluation describes data dependencies for a path specified by the user or the system; dynamicsymbolic 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 ourcase, we use symbolic evaluation to select a set of paths with consistent path conditions fromthe set of paths matching the input and output message sequences. This can be considered anextension of path-dependent symbolic evaluation. Even though we may not know the valuesof internal variables which have an effect on the execution of the specification, they can beinferred 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 observedCHAPTER 3. TRACE ANALYSIS BASED ON FORMAL SPECIFICATIONS^28trace 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 beobtained from the specification.3. The values of the other internal variable can be inferred from the interaction serviceprimitive 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 non-ambiguous test case 7', of Definition 5, then it is possible to determine if the implementationconforms to the specification. In trace analysis where the initial state, final state and constraintsare not known as in Definition 6, what we can say about the correctness of the implementa-tion depends on the length of the observed path. For a given protocol, there is a thresholdpath length It less than or equal to that given by Theorems 1 and 2 which will differentiateevery possible ambiguity on the path (see Section 3.5 for i t for X.25 LAPB). For messagesequences of length less than or equal to It , one may conclude the implementation containserror(s) only if EXT(M) g EXT(X). However, EXT(M) C EXT(X) does not necessarilyimply conformance.3.4 Trace Analysis in External Test ArchitecturesIn the last section, we have outlined the basic technique for determining whether a trace ofinput 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 messagesCHAPTER 3. TRACE ANALYSIS BASED ON FORMAL SPECIFICATIONS^29and in the order they are generated. If the implementation under test (IUT) is to be observedexternally, it may not be possible to have access to the interaction points of both the upperand 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 assumethat a system clock will timestamp all events occurring at the IUT, and that a test architecturesuch as the Ferry [Chans 89] or Astride [Rafiq 90] is used to transfer all local observations tothe global analyzer with timing information. The problem remains as to how to organize thelocal traces into one global trace with the input and output messages ordered properly. Thisis difficult since messages may be generated spontaneously by the IUT (i.e., without externalstimuli) 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 andoutput 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, thecomposite 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, forthe IUT to send a response, and for the response to travel from the IUT to the observer. TheCHAPTER 3. TRACE ANALYSIS BASED ON FORMAL SPECIFICATIONS^30order relationship between messages pi and qi can be determined if the timestamps of inputmessage 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 possibleset 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 orderrelationship between messages pi and qi, the number of possible cases will be reduced.3.5 A Case Study - The X.25 LAPB ProtocolWe now demonstrate the feasibility of the proposed methodology by applying it to a specificprotocol, 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 FSMdiagram 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 smalldomain 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 thesequences g/j or h/k (marked with an * in the appendix). Not only are the message typesand parameter values identical, they also end in the same states. Thus, if these sequences areobserved without leading message sequences before them, it is not possible to determine thestates from which the message sequences start. Note also that transition loops such as w/_ andv/_ (marked ** in Appendix B) may make the threshold value of the homing sequence pathlength / t large. However in this example the transition loops w/_ and v/_ are used for exceptionhandling so the iteration number is likely to be small. The threshold value of path length It(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 frameand the transmitter of a response frame. Frames containing commands transferred from theDCE to the DTE contain the address A and frames containing responses transferred from theDCE to the DTE contain the address B. In the case of DTE, the address is the reverse ofthe above. In order to differentiate polling and response to polling, LAPB uses the P/F bitCHAPTER 3. TRACE ANALYSIS BASED ON FORMAL SPECIFICATIONS^32which has the value 0 or 1. Each I frame contains a send sequence number N(S). Also all Iframes and supervisory frames contain N (R), the expected send sequence number of the nextreceived I frame. For sequence numbers based on modulo 8 or higher, the possible combina-tions of N (S) and N (R) are large and will cause a large number of transitions if integrated intothe control flow. Therefore we have included only the data variables Address and PIF in thecontrol flow (for LAPB, this includes all transitions except those associated with the self loopat state ABM). This means the transitions from ABM to ABM must be handled differentlyfrom the rest. The transitions from ABM to ABM will produce infeasible paths which mustbe detected and deleted. No infeasible paths will be produced for the other transitions, sincethe data values are integrated into the interaction service primitives.We demonstrate our approach using two examples from [Wvong 90]. The first example dealswith 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 DCEthen tries to initiate link set up. Finally the DCE requests link reset by sending a FRMRresponse, and the DTE resets the link. Note that in our example, the trace analyzer is locatednear the DCE side and is observing the behavior of the DTE at the both lower and upperinterfaces. Based on the timestamps on each message (given in [Wvong 90] but not shown inFigure 3.1) and information on request and response of the messages, we obtain the messagesequences{DISC, A,1 < U A, A,1; {__ < DISC, B,1^U A, B,1 < _}} « SABM, A,1 < U A, A,1 «DIE^DCE^ DIEDISC,B,1^I,A,0,2,2UA,A,1 RR,A,0,3.&/I,B 4O,2,3DCEDISC,A,IUA,B,1SABM,A,1 .CHAPTER 3. TRACE ANALYSIS BASED ON FORMAL SPECIFICATIONS^33UA,A,1 RR,B4O,3FRMR,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 TracesFRMR, B,1 < SABM, B,1for the interaction point at the lower interface. Here "2' means the message is either null or notobservable from the trace at the lower interface. However, it can be obtained from the upperinteraction point or deduced from the specification that the first "_._" is DiscReq from the upperinteraction point. There are three transitions, namely ABM --* SEND_DM,SEND_DISC --*SEND_DISC, and WAIT_S'ABM —' SEND DM which can produce the message pairDISC < UA. From the figure in Appendix B, only one of them satisfies the constraintsof the observed trace:Transitions : ABM ► SEND_DISC 24 SENDDISC SEND_DMA^ B^ C,----"---,—.—..„ ,----".----, ,--.---,..---,Messages seqs: DiscReq < DISC, B,1 << DISC, A,1 < UA, A,1 < 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 givesus one path by rule 1, and this allows us to decide that LocalRNR=false by rule 2. AlsoWriteSFrame(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 variablessuch as RemoteRNR=false, TimerRecovery=false, aframeA.NS=VS and aframeA.NR=VR byrule 2. These in turn allow us to select paths which are dependent on internal variables. Forexample, 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 internalvariable VR because of the assignment statement aframeA .NR := VR just after point E inthe flow chart. Since the I frame's aframeA.NS has value 2, the predicate frameA.NS <> VRCHAPTER 3. TRACE ANALYSIS BASED ON FORMAL SPECIFICATIONS^36which appears between points C and D is inferred to be false by rule 3. Thus, the correctpath between points C and D which was marked in bold can be verified as one matching theobserved trace. Furthermore, clearrecovery in ReadSFrame just after point F is evaluated to falseusing the values of variables already known to us. The values of interaction service primitiveparameters 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 betweenpoints F and G that satisfies all the constraints. As a result we have one path satisfying theobserved input and output message trace. Therefore the trace (b) is valid according to theformal specification.3.6 Test Case Generation and ValidationEarly work on automating the selection of test cases is based on the FSM model. This modeldiscusses the control flow of a protocol and has been widely used in test case generation. Morerecently, the data flow of a protocol is being taken into consideration as well by using an EFSMmodel.As mentioned earlier, test case generation and trace analysis share some common functionswhich can be depicted using Figure 3.2. For test case generation, the Path Selection phasegenerates a set of paths whose initial and final states are equal to that of FSM F. Fortrace analysis this phase generates a set of paths whose input and output interactions matchthe observed input and output sequences as described in Section 3.3. In order to make thenumber of paths manageable, we make use of structural constraints which place limitationsCHAPTER 3. TRACE ANALYSIS BASED ON FORMAL SPECIFICATIONS^37Initial and Final StatesConstraints ^ Formal Specification Back End of Passive MonitoringDataSelectionPathSelectionVTracePathSelectionSymbolic EvaluationTest Case Generation Trace AnalysistiTest Case ValidationFigure 3.2: Test Case Generation and Trace Analysison transition loops, while statements, and intermodule communication. We have describedAllPath, the most powerful criterion in data flow analysis. For test case generation, the DataSelection 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 messageordering and/or loss of test data. In the Data Selection phase, in order to make the number oftest cases finite, we make use of data constraints which place limitations on the variables andinput interaction parameters. The general constraint satisfaction problem is undecidable. If thedomain of variables and input parameters of the protocol is finite, the constraint satisfactionproblem 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 fortest path selection [Ural 87], a hybrid method combining the control and data flows [Sank 87],CHAPTER 3. TRACE ANALYSIS BASED ON FORMAL SPECIFICATIONS^38and Constraint Logic Programming for generating only feasible test cases with constraints onthe parameters of input interactions [Chun 90]. Podgurski compares a number of data flow pathselection criteria [Podgu 90]. One of the major weaknesses of all data flow criteria is that theyare based solely on syntactic information and do not consider semantic issues such as infeasiblepaths. The presence of a data flow anomaly does not imply that execution of the program willdefinitely 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 traceanalysis but also for test case generation. For example, if we transform the Estelle specifi-cation of X.25 LAPB into F by Procedure 1, we can generate all possible execution pathsAll P ath(F, Si, So , C). By selecting specific initial and final states with constraints for test casegeneration, the paths can be structured as a tree. All paths except those transitions from thestate ABM to ABM of LAPB cover every possible combination of data flow. Therefore, we donot need to use the Data Selection phase on them. Unfortunately, even though the domains ofvariables and input interactions are finite, paths containing the transition from ABM to ABMhave a large number of value combinations of variables and input interaction parameters. Forthese 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 environmentaleffects on traces such as uncertainty of the message order and/or loss of the test data. The testcase validation based on LOTOS was done by using TETRA[Bochm 90], a modified version ofa LOTOS interpreter, and the test case validation based on Estelle has been done [Zhou 92]CHAPTER 3. TRACE ANALYSIS BASED ON FORMAL SPECIFICATIONS^39by using the trace analyzer (this will be shown in the Chapter 4).3.7 Chapter SummaryWe have presented the basic techniques used to perform trace analysis for Estelle specifica-tions. Indeed, since the model is based on EFSMs, it will work with any specifications thatcan be translated into EFSM representations. In order to avoid transition explosion as a resultof normalization of Estelle specifications, we included conditional statements and introducedsymbolic evaluation to detect and discard infeasible paths. Some practical issues such as traceanalysis using an external test architecture were also discussed. The technique was illustratedusing X.25 LAPB to show that it can handle some of the difficult problems such as framecollisions and data flow rigorously. We also showed the relationship between trace analysis andtest case generation and briefly discussed how our framework can be extended to include testcase generation and validation.Chapter 4Implementation of Trace AnalyzerIn this chapter, a prototype implementation of the trace analyzer is described in order todemonstrate the feasibility of the unified model proposed in the previous chapter. A high-leveldescription of the implementation is given in Appendix D.4.1 Brief Description of ToolsThe tools used for developing the trace analyzer are briefly outlined below. Details can befound in [Sampl 90] (on ASN.1) and [Lu 91] (on TESTGEN parser). The specification ofX.25 LAPB in Estelle.Y and ASN.1 was hand coded and translated from an Estelle speci-fication of the protocol to be traced. The TESTGEN parser together with an ASN.1 parseris used to translate the specification in Estelle.Y and ASN.1 into an internal format knownas Protocol Data Structure (PDS). The trace analyzer consists of two phases: a preprocessingphase and a main analysis phase. It works directly on the PDS for trace analysis or test casevalidation.40....,.....,..................,-•-•""^---s.............................4._Protocol Specificationin Estelle.YASN.1 representationof Data PartTESTGEN ParserProtocol Specificationin EstelleCHAPTER 4. IMPLEMENTATION OF TRACE ANALYZER^ 41/Protocol Data StructureTrace AnalysisPreprocessing Phase^Test Suites.e'-.------,^Test Case ValidationMain Analysis PhaseTrace fromPassive MonitoringII, .-^N,Verdict^i= FileC) Dynamic Modulev1 Data StructureTrace AnalyzerFigure 4.1: Overall Structure of Trace Analyzer4.1.1 Estelle.Y with ASN.1Estelle.Y uses an Extended Transition System (ETS) to model the observable behaviors of aprotocol, and ASN.1 to model the data representations. The syntax of the behavior part of anEstelle.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 ab-stract data types and their values. It is also used as a transfer syntax. ASN.1 is standardizedby ISO[ISOe] and is widely accepted as a formal language for specifying the data structures ofCHAPTER 4. IMPLEMENTATION OF TRACE ANALYZER^ 42higher level OSI protocols.The structure of Input Service Primitives (ISPs), Output Service Primitives (OSPs) andProtocol Data Units (PDUs) in Estelle.Y specifications are also specified using ASN.1. TheASN.1 parser[Sampl 90] was developed using the UNIX Lex/Yacc tools. It produces an ASN.1type tree from an ASN.1 specification. The PDS maintains pointers into the ASN.1 type treeto allow information to be accessed.The main differences between Estelle.Y and NormalFormSpecification [Sarik 86], whichis 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 statementsin 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.YEstelle.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 inthe translation: how to handle while loops containing OSPs and how to handle transitionscontaining timers. These issues will be discussed in Section 4.2.2 and 4.2.3 respectively.CHAPTER 4. IMPLEMENTATION OF TRACE ANALYZER^ 434.1.3 Protocol Data StructureThe PDS is designed to be a machine accessible form of the ETS/ASN.1 based formal descrip-tion. 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 primitivesin ASN.1 type trees.4.1.4 TESTGEN ParserThe TESTGEN parser is designed for test case generation with respect to control and dataflows of formal protocol specifications. It parses Estelle.Y /ASN.1 specifications and generatesa corresponding PDS. The ASN.1 parser is used to convert the ASN.1 specification intoASN.1 type trees. The ASN.1 type trees are linked to the PDS by the TESTGEN parserwhen the Estelle.Y specification is being parsed. As a result, the PDS includes both Estelle.Yand ASN.1 protocol information generated from an Estelle.Y/ ASN.1 specification.4.2 Implementation Issues4.2.1 Known Initial StateOur techniques assume the initial state is known. There are two reasons for this: one is thatprotocols run reactively (i.e., they will always return to the initial state at some time), and theother 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. When-ever we interpret symbolic predicate expressions, decisions can be made without back-trackingbecause the values of variables and ISP and OSP parameters are known.CHAPTER 4. IMPLEMENTATION OF TRACE ANALYZER^ 444.2.2 Unfolding LoopsThe Estelle specification may contain while statements in some of the transitions. The whilestatements may or may not contain "OUTPUT" primitives. The latter case poses no problemsince the values of variables, including the number of loop iterations, are known. The formercase cannot be included in a transition of Estelle.Y, since Estelle.Y allows at most one inputand 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 formby using auxiliary states and variables. The transition in Estelle below is translated intofive 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 thatlast two transitions in the Estelle.Y specification are spontaneous ones and include the falsecondition of while statement in their "PROVIDED" clause./* a transition in Estelle */FROM ABMTO ABMWHEN P.DatalndicatBEGINwhile (LastRxNR <> Datalndicat.nr) do beginLastRxNR := (LastRxNR + 1) mod Modulus;OUTPUT S.AckIndicat;CHAPTER 4. IMPLEMENTATION OF TRACE ANALYZER^ 45end;if (DataIndicat.PF = 1)SendingREJ := false;elseSendingREJ := true;END;/* a set of transitions in Estelle.Y from the above */FROM ABMTO ABMONEWHEN DatalndicatPROVIDED (LastRxNR <> Datalndicat.nr)OUTPUT AcklndicatBEGINLastRxNR := (LastRxNR + 1) mod Modulus;tmppf := Datalndicat.PF;tmpnr := Datalndicat.nr;END;FROM ABMCHAPTER 4. IMPLEMENTATION OF TRACE ANALYZER^ 46TO ABMONEWHEN DatalndicatPROVIDED (LastRxNR = Datalndicat.nr)BEGINtmppf := Datalndicat.PF;tmpnr := Datalndicat.nr;END;FROM ABMONETO ABMONEPROVIDED (LastRxNR <> tmpnr)OUTPUT AcklndicatBEGINLastRxNR := (LastRxNR + 1) mod Modulus;END;FROM ABMONETO ABMPROVIDED ( tmppf = 1) AND (LastRxNR = tmpnr)BEGINCHAPTER 4. IMPLEMENTATION OF TRACE ANALYZER^ 47SendingREJ := false;END:FROM ABMONETO ABMPROVIDED (tmppf <> 1) AND (LastRxNR = tmpnr)BEGINSendingREJ := true;END:As a result of unfolding loops, one atomic transition from an Estelle specification could besplit into multiple atomic transitions in an Estelle.Y specification. This could lead to semanticinconsistency. However, this does not effect the results of trace analysis since the order oftransition execution is not changed. Unfolding loops while maintaining semantic integrity maybe useful for some other applications and is left as future research.4.2.3 Transitions with TimersPhysical global clocks in distributed systems usually do not exist. In conformance testing, twoclocks are used: one in the IUT and the other in the Tester. Some transitions of the IUT maydepend on the timer. A transition may be executed after a specific time given by the timerhas 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 matchesCHAPTER 4. IMPLEMENTATION OF TRACE ANALYZER^ 48with one from the formal specification, we include those transitions as candidate transitions tobe checked. This means the number of candidate transitions could be more than in the casewhere timers are considered. However, if there are no candidate transitions when timers are notconsidered, there will be no candidate transitions even if timers are included. For the purposeof 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 transi-tions containing timers, since this technique could produce fewer candidate transitions./* a transition in Estelle */FROM SEND DMTO SEND DMPROVIDED (TxAttempts <= N2)delay(T1)BEGINframe.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^ 49FROM SEND_DMTO SEND_DMPROVIDED (TxAttempts <= N2)OUTPUT DataRequestBEGINDataRequest.frametype := DM;DataRequest.pf := 0;DataRequest.address := A;TxAttempts := TxAttempts + 1;END;4.2.4 Preprocessing PhaseThe preprocessing phase is not considered part of the actual trace analysis. Its function isto improve the performance and efficiency of the main analysis phase. The preprocessingphase shown in Appendix D.1 translates some transitions of EFSM into FSM transitionsconsisting of input symbols and output symbols only (i.e., no internal variables). This schemeis a modification of Procedure 1 in Chapter 3. Instead of enumerating all possible combinationsof service primitives and their parameters, some parts of the enumeration are done based oncost-effectiveness. For example, the transition below is in the form of an FSM with "INPUT"and "OUTPUT" involving no internal variables.FROM SEND_DMFormat: (set of input values)/(set of output values)CHAPTER 4. IMPLEMENTATION OF TRACE ANALYZER^ 50TO SEND_DMWHEN Datalndicat^ IPROVIDED (DataIndicat.frametype = I) AND 'INPUT(Datalndicat.address = A) AND^I(Datalndicat.pf = 1)^ IOUTPUT DataRequest IBEGIN^ IDataRequest.frametype := SABM; !OUTPUTDataRequest.pf := 1;^IDataRequest.address := B;^IEND;SEND_DMFigure 4.2: Corresponding Finite State Machine.4.2.5 Search MethodAs mentioned in Section 3.6, test case generation requires the initial and terminal states tobe known but trace analysis does not. Test case generation can adopt either depth-first orCHAPTER 4. IMPLEMENTATION OF TRACE ANALYZER^ 51breadth-first search method, but it is more appropriate to use breadth-first search for traceanalysis since the terminal states are not known. This implies that breadth-first search can beused for both trace analysis and test case generation.4.2.6 Pruning Candidate TransitionsAt any state, the values of related variables are known because of the assumption in Section4.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 producedby the preprocessing phase in Procedures 4.1 and 4.2 in Appendix D to the trace. If the listdoes not match the trace, prune the transition.Step 2. For the transitions in an EFSM form, interpret the symbolic predicate expressionsby substituting the values of variables and ISP parameters. If the result of the interpretationis false, prune the transition.Step 3. Of those transitions that survive Step 2, execute the statements inside the transitionsand compare the OSP parameters with the trace. If the OSP parameters do not match thetrace, prune the transition.4.2.7 Verdict and Location of ErrorsThe trace analyzer logs the transitions of a formal specification which satisfy the given tracesin a file. If a trace does not conform to the formal specification, the trace analyzer stops atthat point with an error message displayed on the screen for the user. It also provides theCHAPTER 4. IMPLEMENTATION OF TRACE ANALYZER^ 52values of related variables just before the point of failure to help the user locate the errors inthe 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 ex-ecuted. Sometimes, more than one path may satisfy the traces due to nondeterminism. Inthis case we can follow these paths using "transition keys" given in the file. Every transitionhas 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 "parenttransition id". In the notation "(i, j)", i and j denote transition id and parent transition idrespectively. 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 pathsatisfies a given trace.(0,0)Figure 4.3: Data Structure for Nondeterminism.CHAPTER 4. IMPLEMENTATION OF TRACE ANALYZER^ 534.3 Sample ExperimentsThe prototype implementation of the trace analyzer has around 7,000 lines of C code. We testedthe trace analyzer using the X.25 LAPB protocol. The Estelle specification of X.25 LAPBin Appendix A is around 700 lines. The Estelle.Y in Appendix G and ASN.1 in AppendixF translated from the Estelle specification are around 1600 and 100 lines, respectively. Fourcases of LAPB trace analysis are documented below.4.3.1 Cases 1 and 2Case 1 checks to ensure the IUT sends a DM with F=1 in response to a DISC command withP=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 input2and output2 are to the upper interaction point. Inputl and outputl consist of "interactionprimitive", "PDU type", "address", "P/F bit", "send sequence number", "receive sequencenumber" and "data" fields. In this case, we send a DISC and wait for a DM or UA as thepreamble; 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^ 54Log file for Case 1:Transition Key = 2 From State = SEND_DM To State = SEND_DMParent_Transition_ID = 0 Transition_ID = 0Transition Key = 2 From State = SEND_DM To State = SEND_DMParent_Transition_ID = 0 Transition_ID = 1Transition Key = 5 From State = SEND_DM To State = SEND_DMParent_Transition_ID = 1 Transition_ID = 2Case 2, below, shows invalid IUT behaviors. We send a DISC and wait for a DM or UA asthe 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 analyzerproduces log information up to the point where the trace no longer conforms to the specificationand 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_DMCHAPTER 4. IMPLEMENTATION OF TRACE ANALYZER^ 55Parent_Transition_ID = 0 Transition_ID = 0Values of Variables:key = 0name = TxAttemptstype = INT_TYPint val = 0key = 1name = clearrecoverytype = BOOL_TYPbool val = false••key = 20name = tmpaddresstype = INT_TYPint val = 0CHAPTER 4. IMPLEMENTATION OF TRACE ANALYZER^ 564.3.2 Case 3In 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. Thetrace conforms to the specification.Trace for Case 3:Datalndicat DISC A 1 - - - / DataRequest DM A 1 - - - / -Datalndicat SABM A 1 - - - / DataRequest UA A 1 - - - / ConlndDiscReq ^ / 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_DMParent_Transition= 0 Transition_ID = 0Transition Key = 1 From State = SEND_DM To State = ABMParent_Transition= 0 Transition_ID = 1Transition Key = 96 From State = ABM To State = SEND_DISCParent_Transition= 1 Transition_ID = 2CHAPTER 4. IMPLEMENTATION OF TRACE ANALYZER^ 57Transition Key = 123 From State = SEND_DISC To State = SEND_DISCParent_Transition= 2 Transition_ID = 3Transition Key = 124 From State = SEND_DISC To State = SEND_DMParent_Transition= 3 Transition_ID = 44.3.3 Case 4This trace checks to ensure the IUT handles an I frame transfer and an REJ command withP=1 correctly, by sending an RR with F=1. As a preamble, the tester sends a DISC and waitsfor a DM or UA, then sends a SABM and waits for a UA. For the postamble, the tester sendsan 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 - - - / ConlndDatalndicat 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^ 58Datalndicat 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 - - - / DisclndDatalndicat DM B 1 / -Log file for Case 4:Transition Key = 2 From State = SEND_DM To State = SEND_DMParent_Transition= 0 Transition_ID = 0Transition Key = 1 From State = SEND_DM To State = ABMParent_Transition= 0 Transition_ID = 1Transition Key = 30 From State = ABM To State = ABMParent_Transition= 1 Transition_ID = 2Transition Key = 103 From State = ABM To State = ABMParent_Transition= 2 Transition_ID = 3CHAPTER 4. IMPLEMENTATION OF TRACE ANALYZER^ 59Transition Key = 94 From State = ABM To State = ABMParent_Transition= 3 Transition_ID = 4Transition Key = 30 From State = ABM To State = ABMParent_Transition= 4 Transition_ID = 5Transition Key = 103 From State = ABM To State = ABMParent_Transition= 5 Transition_ID = 6Transition Key = 94 From State = ABM To State = ABMParent_Transition= 6 Transition_ID = 7Transition Key = 30 From State = ABM To State = ABMParent_Transition= 7 Transition_ID = 8Transition Key = 103 From State = ABM To State = ABMParent_Transition= 8 Transition_ID = 9Transition Key = 94 From State = ABM To State = ABMParent_Transition= 9 Transition_ID = 10CHAPTER 4. IMPLEMENTATION OF TRACE ANALYZER^ 60Transition Key = 59 From State = ABM To State = ABMParent_Transition= 10 Transition_ID = 11Transition Key = 47 From State = ABM To State = ABMParent_Transition= 11 Transition_ID = 12Transition Key = 92 From State = ABM To State = SEND_SABMParent_Transition= 12 Transition_ID = 13Transition Key = 16 From State = SEND_SABM To State = SEND_DMParent_Transition= 13 Transition_ID = 144.3.4 PerformanceWe measured the performance of the trace analyzer running on a SUN 4/690 with 65 M Bytesof main memory for the three test cases given above.The number of traces applied, total time taken, average time per trace, and number ofcandidate 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 thepreprocessing phase. These values can be split into four groups: items corresponding to Step1, Step 2 and Step 3 as described in Section 4.2.6 and an item for processing the matchedtransitions. The fact that Cases 1 and 3 deal with control flow exclusively and Case 4 containsCHAPTER 4. IMPLEMENTATION OF TRACE ANALYZER^ 61Case 1 Case 3 Case 4(1) Number of Traces 3 5 15(2)Total Time 0.78 1.31 5.45(3)=(2)/(1)Average Time per Trace 0.26 0.26 0.36(4)Total Number of Transitions 39 95 601(5)Number of Transitions pruned in Step 1 36 90 534(6)Number of Transitions pruned in Step 2 0 0 52(7)Number of Transitions pruned in Step 3 0 0 0(8)Number of Matched Transitions 3 5 15Table 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) givesthe average time taken to process a trace. In particular, note that of the 3 steps classified inSection 4.2.6, no transitions were processed in Step 3 as shown in (7). We believe that mosttraces 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 controland data flows spends an average of 0.4 seconds per trace. Cases 1 and 3, which have no dataflow, have no data related to Step 2 as shown in row (6).4.4 Future WorkSeveral 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, andCHAPTER 4. IMPLEMENTATION OF TRACE ANALYZER^ 624. As the implementation was built upon a prototype of TESTGEN, system tuning isneeded to reduce memory requirements and to improve performance.Chapter 5Concurrency ModelIn this chapter, we present a concurrency model as an intermediate step to extend the traceanalysis model shown in Chapters 3 and 4 to a concurrent environment. Concurrent events,concurrency blocks, global states, concurrency measures, communication deadlocks and dataraces are defined based on the model. The model allows high-level abstractions to be usedfor understanding concurrent behaviors and allows concurrency measures to be computed effi-ciently. 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 ModelCommunication deadlocks and data races are silent errors which do not generate any errormessage. We will assume that time-event sequences, or traces, are available for every task thatinteracts 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 othertasks.63CHAPTER 5. CONCURRENCY MODEL^ 64Definition 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 aretotally ordered, numbered and executed sequentially.The total order of events in a task is transitive, asymmetric and irreflexive.5.1.1 Synchronous and Asynchronous CommunicationsDefinition 9 A Synchronous Communication Event (SCE) between two tasks i and j consistsof two symmetric events denoted by SCE(Ti(k), Ti(1)) where Ti(k) and Tj(1) are matchingsend/receive (or offer/accept) events.One of the tasks involved in an SCE will wait until the matching event is offered by theother task. Then both tasks will proceed simultaneously.If the communication is asynchronous, denoted as ACE(Ti(k), Ti (1)), the receiving task jwill wait for the matching send event and then proceed. The sending task i, however, canproceed as soon as the message is sent.We will adopt the 2 relation given in [Lampo 78] to specify the partial ordering of eventsin concurrent programs. The relation is transitive, asymmetric and irreflexive. Two distinctevents are said to be concurrent if there is no relation between them. The send/receiveevents of an SCE are concurrent whereas there is a relation between the two events of anACE.'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 coB".CHAPTER 5. CONCURRENCY MODEL^ 65^0 ^0 i^1 0^0^2 4)^02^20^02^ 2••2^5 0^0 5^5 0^0 54 4)^0 4^4 4o^4) 43 101 3 3 11111 3 3^3^354/4 5p4 454•^ 560^06^60^4) 6^6^6^6•60^07 7 0^0(a) synchronous (b)asynchronous (a') (b')Figure 5.1: Time-event Sequence Diagrams and Their Corresponding DAGsTo 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. Theobservable events are represented by circles, the vertical edges (arrows) denote total ordering ofthe events within each task, and the diagonal edges represent the message send/receive eventsbetween the two tasks. The origin of an arrow denotes the send event and the head of thearrow the receive event. In case (a), where the communications are synchronous, the followingrelations hold in addition to the total orders of the internal events of each task:CHAPTER 5. CONCURRENCY MODEL^ 66TA(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 anothertotal 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^ 675.1.2 Concurrency CheckingThe ordering relations for events in a time-event sequence diagram can be explicitly representedusing a graph notation shown in (a') and (b') of Figure 5.1. The algorithm to transform a time-event 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) andTj — 1) in the time-event sequence diagram respectively. There are also two outgoing arrowsfrom E to nodes corresponding to Ti (k + 1) and Ti (l + 1) in the time-event sequence diagramrespectively.)With Procedure 2, the problem of determining the concurrency relation between two eventsin a time-event sequence diagram becomes one of determining the connectivity relation betweentwo vertexes in a Directed Acyclic Graph (DAG). The asymmetric and irreflexive properties ofthe —> 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 between3 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^ 68two events in the graph, all we need to know is whether there are any directed paths betweenthe corresponding vertexes. The widely used algorithm suggested by Moore [Moore 59] fordetermining the shortest path can be adapted for our application. The complexity of Moore'salgorithm 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 algo-rithm) between them.In all other cases, the events are ordered.Note that the events in an SCE are concurrent. This algorithm works for both asynchronousand 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 labellingnodes 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 theshortest path becomes expensive. We will introduce a technique to minimize the number ofevents which have to be managed by this method to make it efficient.Definition 10 A communication deadlock 5 exists if1. in an SCE or ACE, one of the matching events never occurs, or5 The term deadlock is also used to mean blocking in this chapter.CHAPTER 5. CONCURRENCY MODEL^ 692. there is a transitive closure of relation among the synchronous send and receiveevents (i.e., circular waits).Execution of concurrent specifications (or programs) can be represented by the RendezvousGraph [Tai 86], Concurrency Map [Stone 88], or Parallel Dynamic Program Dependence Graph[Mille 88]. These representation methods focus on exhibiting potential concurrency with theemphasis 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 todescribe concurrent events, global states, concurrency measures, communication deadlocks anddata races of concurrent specifications. We shall present a new model in the following sections.5.1.3 Global Synchronization CutThe basic concept is to detect ordering of events among tasks in a system based on theircommunication behaviors. Other forms of synchronization such as those due to task activationand completion are not considered.Synchronous CommunicationLet us suppose that a set of distributed tasks interact with one another using synchronouscommunications. We observe that how far the events of a task may proceed may be limited byother 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 forthe 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-TASK A B CBGSCOBlock 1FGSC I fr^ BGSC 1TimeBlock2BGSC2-- FGSC2Block3FGSC3BGSC3Block4- FGSC4CHAPTER 5. CONCURRENCY MODEL^ 70Figure 5.2: Examples of Global Synchronization Cutsevent 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 mayback-track its events until it is limited by some SCE that has already occurred. Thus a line ofthe 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 (ForwardGSC), and the GSC of maximal regression will be called BGSC (Backward GSC). Betweenthese two extremes, there are many valid combinations of task states representing possibleglobal states of the distributed system. Note that GSC's are defined in this section only forsystems using synchronous communications. At this point, we would like to study the -4CHAPTER 5. CONCURRENCY MODEL^ 71relation on events, SCEs, and GSCs. Specifically, the --+ relation on SCEs and GSCs areextensions 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 oneother SCE in the system.To check if an SCE is concurrent with another SCE, the events that make up the twoSCE'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 arerepresented by integers, and the position of an integer in thevector 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 theevent 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 whichhave not been processed.CHAPTER 5. CONCURRENCY MODEL^ 72Notation 8 SCE_AFTER_SET_SCEMO is a function returning the next (chronological) SCEevent 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 (chrono-logical) 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 kkeeps track of the current concurrency block. The events are examined in chronological order intask 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 (lastn )} */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), Tn (0))};draw the BGSCo; ---(1)while (1)do/* the SCEs are examined in chronological order */CHAPTER 5. CONCURRENCY MODEL^ 73check_S'CEO;if the next SCE(7'p (x),Tq (y)) 0 a Concurrent SCE --(2)thenk = k + 1;add the SCE(Tp (x), Tq (y)) into the set SET_SCE;elsecheck_SCEO;add the SCE(Tp (x),Tq (y)) into the set SET_SCE;continue;fifor(i = 1; i < n; i++) /* for each task */ --(3)docase/* 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^ 74with v = SCE_AFTER_SET_SCE(T9 ).BGSCk l, = {T, (v)};with v = NEXT_EVENT_AFTER_SET_SCE(T9 )./* 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 ).esacoddraw a FGSCk and a BGSCk; --(7)check_SCEO;procedure check_SCE0 --(8)/* check whether there are unprocessed SCEs */for(i=1; i where inky and outs are the input and output messagesrespectively at interaction port j associated with the k-th event vector in trace Ti. ins and outsmay be null.Notice that we have a trace structure equivalent to the ones presented in Section 3.3 and3.4. Recall those trace structures dealt with trace analysis based on single modules of formalspecification. Therefore, an event vector consists of zero or one input, and i output messageswhere 0 < i < p.• • •S SiA• ••• •MIScAoncTconcMconcTn TI• •Mi••• •MnTI• •• •CHAPTER 6. TRACE ANALYSIS BASED ON CONCURRENT SPECIFICATIONS 100 Figure 6.3: Trace Analysis based on Concurrent SpecificationsDefinition 19 A sequential module Mi is pointwise conformant to the formal specification Sion an event vector d if the behavior of the event vector is permissible in the specification. Thisis denoted as pconf(Mi, Si , tlf).Note that even if more than one path (or transition) of the specification satisfies the eventvector, 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, tlf) for all d in Ti.The sequential trace Ti from Definition 18 consists of the external behaviors of a moduleMi with respect to its environment (i.e., the other modules). If cortf„q (Mi, Si, Ti) is valid, thetrace Ti conforms to the specification of Mi. In addition, the input/output messages to/fromthe 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 concur-rent specification Scan, of Mconc , written ascon fconc (ldconc , Sconc , Teonc) if conheq (Mi , S1, T1) A • • • A amf,"(Mi, Si ., Ti) A • . • A confseq (Mn ,Sn ,Tn ), i.e., A i_ iconfseq (Mi, Si, Ti).Note that the trace analysis proposed does not depend on the communication scheme (syn-chronous or asynchronous). The trace analysis of concurrent modules with respect to concurrentformal specifications provides verdicts based on a set of trace analyses of single modules withsequential formal specifications.Since the two unique types of errors that could arise in concurrent (or distributed) envi-ronments are deadlocks and data races, we need to show how they can be detected in theconcurrent model. To detect data races, we note that a set of con f seq (Mi, S i,Ti) - trace analy-ses with respect to single module - allows the construction of the time-event sequence diagramwhich is used by the concurrency model (see Section 6.1.2 and Chapter 5). The concurrencymodel provides a way to detect data races as shown in Section 5.2 and Appendix E. Deadlockdetection will be illustrated in Section 6.4.6.3 ApplicationsWe begin by discussing the application of our model of trace analysis based on concurrent spec-ifications 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; themodules may be implemented on the same machine or on different machines. We then show howCHAPTER 6. TRACE ANALYSIS BASED ON CONCURRENT SPECIFICATIONS 102the model can be used in specific applications such as multi-party testing and interoperabilitytesting.6.3.1 Trace Analysis based on Multi-module SpecificationsIn order to check certain properties for a set of concurrent programs, the relative order ofinteractions occurring at different ports as well as the order of operations occurring at each ofthe modules must be determined. This is a difficult problem in distributed systems. In orderto construct an order of observed and unobserved (i.e. internal) events, our model consists oftwo parts. The first obtains the order of interactions between modules from the trace using themethod given in Section 6.1.3. The second obtains the order of operations within each modulefrom 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 fromthe POT independent of the number of interaction ports. Based on the formal model in Section6.2, trace analysis of concurrent specifications could be considered as a set of trace analyses onthe 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 calledOSI POs and the other, supported by our model, will be called POTs. The OSI POs havebeen 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 theprotocol layers only. No POs (or PCOs) exist within the individual layers. In our model, wecan get the exact order of interactions among modules using the concept of POT as describedCHAPTER 6. TRACE ANALYSIS BASED ON CONCURRENT SPECIFICATIONS 103 POTPOT^POTPOTOSI Layer NFigure 6.4: Applicationin Section 6.1.3, and the order of operations inside a module using the trace analysis techniquediscussed in Section 6.1.1 and Chapter 3. Deadlocks can be detected by the method presented inSection 6.4 and Chapter 5. The concurrency model in Section 6.1.2 allows data races betweenmodules to be detected. The block structure of events which contains possible concurrentevents allows data races to be checked easily for systems or languages using synchronous orasynchronous communications.6.3.2 Message Collisions in Multiple Party and Interoperability TestingsThe need for multi-party testing arises in the situation where an action (or an instance ofcommunication) of the protocol entity to be tested causes subsequent actions at other protocolentities. Examples can be found in Message Handling System, Routing Protocol, IntegratedServices Digital Network, Distributed Transaction Processing and Directory Services. In thissituation, 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 whichmay involve multiple peer entities distributed among several systems, each communicating withCHAPTER 6. TRACE ANALYSIS BASED ON CONCURRENT SPECIFICATIONS 104the IUT through a unique association or connection.Testing OS/ protocol implementations before deployment to production fields provides ameasure of confidence in their correctness. A protocol implementation is said to conform tothe relevant standards if conformance testing yields a positive verdict. This, however, doesnot necessarily guarantee it is able to interwork properly when deployed as part of a completeworking system. Therefore, interoperability testing is needed in order to verify the end-to-endbehavior 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 analysisin 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 adistributed system.In fact, these applications are natural extensions of the general problem described in theprevious section. A message collision is said to have occurred when a message send event and amessage receive event between modules occur concurrently. This can be detected using Proce-dure 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 occursin synchronous communication, it is a deadlock. The trace analysis techniques discussed in Sec-tion 6.1.1, Chapter 3 and Chapter 4 should be able to handle message collision. Our prototypeimplementation [Kim 91] using Estelle (which supports asynchronous communication) showsthat message (in this case, frame) collision problems are correctly analyzed.CHAPTER 6. TRACE ANALYSIS BASED ON CONCURRENT SPECIFICATIONS 1056.4 Case StudyThe Five Philosopher's Dining Problem is a traditional example of concurrent systems whichrequires synchronization among the processes according to some protocol. The five philosophersspend their lives eating or thinking. Each philosopher has his own place at a round table. Onlyfive forks are provided, one between each pair of philosophers. The philosophers can only pickup the forks on their immediate left or right. The food is at the center of the table, and twoforks are needed to eat the food. Here we modify the problem description to avoid deadlocksand indefinite postponement (i.e., livelock). When a philosopher is hungry, he goes to the diningroom and sits down at his own fixed position. After eating, he leaves the room and continuesto think. The model includes a manager to monitor the five philosophers. Each philosopherhas to apply to the manager to enter the dining room. Only when he gets the permission canhe enter or leave the dining room.ManagerM2 T2Lp2 Rp2LI RIForklPhil2Figure 6.5: Module StructureFigure 6.5 shows a part of the module structure of the problem and Appendix H containsCHAPTER 6. TRACE ANALYSIS BASED ON CONCURRENT SPECIFICATIONS 106a part of the Estelle description of module instances "Phil2", "Forkl" and "Fork2". In thefigure, symbols T2, Li, Ri, Lpi and Rpi (where i is 1 or 2), are the interaction points betweenmodule instances.After the following traces:tPhil2 =^ (°k Phil2,T21 Cb) , (01 PiCkPhiI2,Lp2) , (0 0) > andtForkl =<^f ork_providecliForkl ,R1) 7 (07 4))let's say that we have the following traces from each module:tPhil2 =< (0, 0), (f ork_provide4hii2,42 61 (6^2rs• • • • 7 iCke- hil2,Rp2) > andt2Fork2 =< (ick2Fork2,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 us-ing the input message "ok" through interaction point "T2". "Forkl" responded with a "fork_provided" to the input message from "Phil2" as indicated in t lForki . The trace t2pk i12 showsthat "Phil2" sent a "pick" message to its right fork, namely "Fork2", through interactionpoint "Rp2" after receiving the message "fork_provided" from "Forkl". Now, if the systemfunctions correctly, trace ti,ork2 should be similar to t lForki . However, the trace from MFork2(i.e., 4,042 ) shows that the output message "fork_provided" through L2 is missing. There-fore, the trace t2Fork2 from MFork2 does not conform to the specification S Fork2. As a result ofCHAPTER 6. TRACE ANALYSIS BASED ON CONCURRENT SPECIFICATIONS 107this 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 specifi-cation 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 MFork2ork will never come.A third type of error occurs when the message sent conforms to the specification of thereceiver module but not that of the sender module. In this case, there is no blocking ordeadlock but the sender module is incorrectly implemented nevertheless.6.5 Chapter SummaryUntil now most work on trace analysis based on formal specifications has been studied in asequential context, even though the specifications are concurrent. In this chapter, we have pre-sented an approach to perform trace analysis of concurrent specifications without translatingthem into their equivalent sequential specification. The concurrency model and the concept oftraceability through the use of Port of Observation for Traceability (POT) and output state-ments 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 interoperabilityCHAPTER 6. TRACE ANALYSIS BASED ON CONCURRENT SPECIFICATIONS 108testings were also briefly discussed.Chapter 7Conclusions and Future ResearchWe conclude this thesis by summarizing the major results and listing some future research.7.1 Summary of ResultsThis thesis has four parts: The first part describes trace analysis with respect to a single-modulespecification based on extended finite state machines. The second part describes a prototypeimplementation of the first part. The third part presents concurrency models to describe anddeal with concurrent properties; and the fourth part examines the trace analysis of concurrentspecifications based on multi-module extended finite state machines.Protocol Trace Analysis based on Single-Module SpecificationsWe have presented a unified model to perform trace analysis and test case generation us-ing single-module Estelle specifications. Indeed, since the model is based on single-moduleextended finite state machines, it will work with any specifications that can be translated intoextended finite state machine representations. In order to avoid transition explosion as a re-sult of normalization of Estelle specifications, we include conditional statements and introduce109CHAPTER 7. CONCLUSIONS AND FUTURE RESEARCH^ 110symbolic evaluation to detect and discard infeasible paths. Some practical issues such as traceanalysis using an external test architecture were also discussed. The technique was illustratedusing X.25 LAPB to show that it can handle some of the difficult problems, such as framecollisions and data flow, rigorously. We have also shown the relationship between trace analysisand test case generation, and briefly discussed how our framework could be extended to in-clude test case generation and validation. Using our model, we implemented a prototype traceanalyzer based on Estelle specifications. It can handle both control and data flows of Estellespecifications with respect to traces or test cases. In addition, the tool can be used to debugEstelle specifications with respect to traces or test cases.Concurrency ModelIn order to extend trace analysis to the concurrent environment, we introduced a concur-rency model. The model transforms the concurrency-checking problem into a path-detectionproblem in graph theory. This method is general enough to be used for both synchronousand asynchronous communications. The concept of Global Synchronization Cuts is presentedto provide an elegant model for defining concurrency blocks, global states and concurrencymeasures. This model allows high-level abstractions to be used for understanding and ana-lyzing concurrent behaviors in formal description techniques for protocols such as Estelle andLOTOS. The model is also applicable to languages such as Ada, Modulo II and Occam whichuse synchronous or asynchronous message passing and/or shared variables as communicationmechanisms.CHAPTER 7. CONCLUSIONS AND FUTURE RESEARCH^ 111Furthermore, based on the model, we have proposed concurrency measures W and M forprogramming systems that support synchronous or asynchronous communications. These mea-sures are extensions of w and m which can be computed much more efficiently.Trace Analysis based on Concurrent SpecificationsAs an approach to investigate the trace analysis of concurrent specifications without trans-lation into the equivalent sequential specification, we have proposed a model consisting of threebasic building blocks: trace analysis with respect to a single-module extended finite state ma-chine, concurrency model, and traceability. This model is formalized and proposed to apply tomulti-module specifications, multi-party testing and interoperability testing. A case study ofthe model on the five philosopher's dining problem was also presented.7.2 Future ResearchThere 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 ourapproach, the following work would be useful:—how to implement the Point of Observation for Traceability given in the specificationin a systematic (or a standard) way,—how to augment OUTPUT statements for a subset of the transitions instead of forall transitions in order to improve performance without loosing information on theprecise order of input/output messages,CHAPTER 7. CONCLUSIONS AND FUTURE RESEARCH^ 112—how to automate the translation phase from Estelle specifications to Estelle.Y andASN.1 specifications, and—how to merge trace analysis of concurrent systems with testers (e.g. Ferry ClipApproach [Chans 92]).• In order to make the trace analyzer simple and efficient, we have assumed that the initialstate 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 DecisionDiagrams [Burch 92]. This technique is popular for hardware verification and is worthinvestigating for application in trace analysis.• For improved performance, it would be useful to investigate building the trace analyzeron a multiprocessor system (e.g., Transputers) [Mohr 92].• An investigation of the use of the trace analyzer in distributed program debugging systemswould 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 Con-current Programs, The 4th Int'l Workshop on Protocol Testing Systems, 1991.[Bochm 89] Gregor v. Bochmann, Rachida Dssouli, and et al, Trace Analysis for Conformanceand Arbitration Testing, IEEE Tr. on Software Engineering, pp. 1347 - 1356, Novem-ber 1989.[Bochm 90] Gregor v. Bochmann, D. Desbiens, and et al, Test Result Analysis and Validationof Test Verdicts, 3rd Intl Workshop on Protocol Test Systems, October 1990.[Bolog 87] Tommaso Bolognesi and Ed Brinksma, Introduction to the ISO Specification Lan-guage 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 inProtocol Conformance Testing: from Theory to Implementation, Computer Networksand ISDN Systems 22, pp. 7-33, 1991.[Bryan 89] Doug Bryan, An Algebraic Specification of the Partial Orders Generated by Con-current 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: 1020 states andbeyond, Information and Computation, p 142-170, June 1992.[CCITT 88] CCITT, CCITT Specification and Description Language (SDL) RecommendationsZ.100, CCITT Blue Book, 1988.[Chans 89] S. T. Chanson, B. P. Lee, and et al, Design and Implementation of a Ferry ClipTest System, The Ninth Intl Symposium on Protocol Specification, Testing, andVerification, June 1989.113BIBLIOGRAPHY^ 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 InteroperabilityTesting using the Ferry Clip Approach, Computer Communications, pp. 153 - 168,April 1992.[Charro 89] Bernadette Charron-Bost, Combinatorics and Geometry of Consistent Cuts: Ap-plications to Concurrency Theory, The 3rd International Workshop of DistributedAlgorithms, LNCS 392, Springer-Verlag, pp. 45 - 56, Sept. 1989.[Charro 91] B. Charron-Bost, F. Mattern, and et al., Synchronous and Asynchronous Commu-nication 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 inParallel-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 inEstelle, 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-StateConcurrent 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 andControl of Synchronous Sequential Machines, Information Sciences 18, pp. 47 - 65,1979.[Dembi 89] P. Dembinski and S. Budkowski, Specification Language Estelle, The Formal De-scription Technique Estelle, Elsevier Science Publishers B.V.(North-Holland) pp. 335- 74, 1989.[Dssou 90] Rachida Dssouli and Reine Fournier, Communication Software Testability, The 3rdIntl Workshop on Protocol Testing Systems, 1990.[Dssou 91] Rachida Dssouli, Reine Fournier and et al., Distributed Observation and FIFOQueues, 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 inthe 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, NewYork, 1962.[Gorli 90] Michael M. Gorlick, Carl F. Kesselman, and et al, Mockingbird: A Logical Method-ology for Testing, The Journal of Logic Programming, pp. 95 - 119, January/March1990.[Helmb 85] David Helmbold and David Luckham, Debugging Ada Tasking Programs, IEEESoftware, 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 SoftwareQuality Conference, pp. 234 - 244, September 1989.[ISOa]^ISO 7776, Information processing systems - Open Systems Interconnection - Descrip-tion 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 StateTransition Model, 89-07-15.[ISOd] ISO 8807, LOTOS - A Formal Description Technique Based on the Temporal Order-ing 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 ACMSIGSOFT/SIGPLAN Software Eng. Symposium on High-Level Debugging, 1983.[Karjo 90] G. Karjoth, A Compilation of Algebraic Process Based on Extended-Action Deriva-tion, 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 basedon 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 Ap-plication 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 Concur-rent Specifications and Its Applications, submitted for publication.[King 76] James C. King, Symbolic Execution and Program Testing, CACM, pp. 385 - 394, July1976.[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 ISDNSystems, pp. 203 -219, April 1990.[Logri 88] L. Logrippo, A. Obaid, and et al., An Interpreter for LOTOS, A Specification Lan-guage for Distributed Systems, Software-Practice and Experience, pp. 365 - 385, April1988.[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 ComputerScience, Univ. of British Columbia, 1991.[Matte 89] Friedemann Mattern, Virtual Time and Global States of Distributed Systems, Par-allel 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 Sci-ence, Springer-Verlag, 1980.[Mille 88] Barton P. Miller and Jong-Deok Choi, A Mechanism for Efficient Debugging of Par-allel 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 Im-plementation of Object-Independent Event Trace Monitoring and Analysis SystemsPossible?, Univ. Erlangen-Nurnberg, IMMD 7, Germany, 1992.[Moore 59] E. F. Moore, The Shortest Path Through a Maze, Proc. Internat. Symp. SwitchingTh., 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 throughData Flow Analysis, Computer Program Testing, edited by B. Chandrasekaran andS. 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 andIts Implications for Software Testing, Debugging, and Maintenance, IEEE Tr. onSoftware Engineering, pp. 965 - 979, Sept. 1990.[Probe 92] Robert L. Probert, Hualong Yu, and et al, Relative-Clock-based Specification andTest Result Analysis of Distributed Systems, The 11th IEEE Intl Phoenix Conferenceon Computers and Communications, 1992.[Rafiq 90] 0. Rafiq and R. Castanet, Experience with the Astride Testing Approach, The IFIPTC6 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 Com-putations, IRISA Publication Interne 610, Oct. 1991.[Rayna 92] Michel Raynal, About Logical Clocks for Distributed Systems, ACM Operating Sys-tems Review, pp. 41 - 48, Jan. 1992.[Saleh 92] Kassem Saleh, Testability-directed Service Definitions and their Synthesis, The 11thIEEE Int'l Phoenix Conference on Computers and Communications, 1992.[Sampl 90] M. Sample and G. Neufeld, Support for ASN.1 within a Protocol Testing Environ-ment, The Third Int'l Conference on Formal Description Techniques, Nov. 1990.[Sarik 86] Behcet Sarikaya and G. v. Bochmann, Obtaining Normal Form Specifications forProtocols, Computer Networks Usage: Recent Experiences, pp. 601 - 612, ElsevierScience Publishers, 1986.[Sarik 87] Behcet Sarikaya, Gregor V. Bochmann, and et al, A Test Design Methodology forProtocol Testing, IEEE Tr. on Software Engineering, pp. 518 - 531, May 1987.[Stone 88] Janice M. Stone, A Graphical Representation of Concurrent Processes, ACM SIG-PLAN 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 Pro-grams, 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 Protocolsand Services , Computer Networks and ISDN Systems 11, pp. 183 - 202, 1986.[Ural 87] Hasan Ural, Test Sequence Selection Based on Static Data Flow Analysis, ComputerCommunications, pp. 234 - 242, Oct. 1987.[Vuong 89] S. T. Vuong, Y. L. Chan and et al., The UIOv-Method for Protocol Test SequenceGeneration, 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 Test-ing, 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 andTesting 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 TraceAnalysis, Master Thesis, Dept. of Computer Science, Univ. of British Columbia,Oct. 1990. See also LAPB Conformance Testing using Trace Analysis, 11th IntlSymposium on Protocol Specification, Testing, and Verification, pp. 248 - 261, June1991.[Young 88] Michal Young and Richard N. Taylor, Combining Static Concurrency Analysis withSymbolic 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 AEstelle Specification of X.25 LAPBprocedure writeiframesent (no: INTEGER);EXTERNAL;procedure writeinfor(infor:char);specification DataLink systemprocess;^ EXTERNAL;default individual queue;^ PROCEDURE writestate(stn,rec_com,sends,initstate,finalstate:INTEGER);timescale second;^ EXTERNAL;type^ initialize to hostreadyaFrameType = (I, RR, RNR, REJ, SABM, DISC, UA, DM, FRMR, BAD);^beginanAddress = (A, B);^ Iframesent := 0;datano := 0;ftype = RECORD TEMP := 0;Address: anAddress;^ end ;Frametype: aFrameType;NS: integer;^ transPF: integer; from hostready to datatransNR: integer; beginUdata: integer; writestate(usern,0,20,11,14);END;^ output Uu.ConReq;end ;aBufferPtr = "ftype;transchannel User_Channel(User, Provider);^ from datatrans to datatransby User:^ when Uu.ConlndConReq; beginDiscReq; 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;^ transfrom datatrans to datatranschannel aPhysicalAccess(User, Provider);^ when Uu.Datalndby User: beginDataRequest(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 ;^ transfrom datatrans to datatransvar^ when Uu.AcklndIframesent : integer;^ begindatano: integer; writestate(usern,25,25,14,14);TEMP: integer;^ end;statehostready, hostbusy, disconn, datatrans, linkreset ;procedure writedatano (no: INTEGER);EXTERNAL;transfrom datatrans to linkresetprovided (Iframesent > 3)beginwritestate(usern,26,26,14,15);output Uu.ResetReq;C . •^lapb.e^• )end;^ (• Reset flow-control variables and clear error conditions. •)begintrans VS := 0;from linkreset to datatrans^ LastRxNR := 0;when Uu.Conlnd^ Unacked := 0;begin^ VR := 0;writestate(100,27,26,15,14); LastTxNR := 0;TEMP := 100; SendingREJ := false;end; Loca1RNR := false;TimerRecovery := false;trans^ RemoteRNR := false;from datatrans to disconn^ end;provided (TEMP = 100)begin function Between(a, b, c: integer): boolean;writestate(usern,0,22,14,13);^ beginoutput Uu.DiscReq;^ if (a <= c) thenend;^ Between := ((a <= b) and (b <= c))elsetrans Between := ((b <= c) or (a <= b));from disconn^ end;when Uu.Disclndbegin function IsCorrectAck(nr: integer):boolean; (•2.3.4.9•){writestate(usern,28,0,13,13);)^ beginend;^ if (TimerRecovery = false) thenEND ; IsCorrectAck := Between(LastRxNR, nr, VS)elsemodule anSLProcedure process (stn:integer);^ IsCorrectAck := Between(LastRxNR, nr, x);ip^ end;SEND: aPhysicalAccess(User) individual queue;RECV: aPhysicalAccess(Provider) individual queue;^ PROCEDURE writestate(stn,rec_com,sends,initstate,finalstate:INTEGER);P: User_Channel(Provider) individual queue; EXTERNAL;end;procedure writedatano (no: INTEGER);body SLPBody for anSLProcedure;^ EXTERNAL;state^ PROCEDURE w_send_data(ns,nr,data: INTEGER) ;SEND_DM, SEND_SABM, ABM, WAIT_SABM, SEND_DISC;^ EXTERNAL;const (• tlT1^2; initializeT2 = 1; to SEND_DMN2 = 6; begink = 8; new(FRMRBuffer);Modulus = 8;^ for VS := 0 to Modulus - 1 donew(RetxBuffer(VS]);var^ TxAttempts := 0TxAttempts: integer;^ end;clearrecovery: boolean;oldvs: integer; t2T1Running: boolean; (• used to restart the T1 timer •)^ transFRMRBuffer, frametwo, aframe: aBufferPtr;^ from SEND_DM (*2.4.4.4•)VS, LastRxNR, Unacked: integer;^ when P.ConReqRetxBuffer: array(0..Modulus) of aBufferPtr; to SEND_SABMVR, LastTxNR: integer;^ beginSendingREJ, LocalRNR: boolean; new(frametwo);TimerRecovery, RemoteRNR: boolean;^ frametwoA.Frametype := SABM;Correctack: boolean; frametwoA.PF := 1;x: integer; {• used in timer recovery •) frametwoA.Address := 8;writestate(stn, 20,1,2,3);procedure ResetWindow;^ OUTPUT SEND.DataRequest(frametwo);TxAttempts := 0;end;t3 •}from SEND_DMwhen RECV.DataRequestprovided (frameA.Frametype = SABM) •2.4.4.4.1")to ABMbeginnew(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 ") provided (frameA.Frametype = DISC) ("2.4.4.4.1')to SEND_DMbeginnew(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;(' t5 ")provided (frameA.Frametype = DM) (•2.4.4.7')to SEND_SABMbeginnew(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;V t6 ") provided otherwise V2.4.3/2.4.4.4.1')to SEND_DMbeginif (frame".Address = A) AND (frameA.PF = 1)then beginnew(frametwo);frametwoA.Frametype := DM;frametwoA.PF := 1;frametwoA.Address := A;writestate(stn,26,4,2,2);OUTPUT SEND.DataRequest(frametwo);end;dispose(frame)end;f" t7 ')from SEND_DMprovided TxAttempts <= N2 ('2.4.4.4.2')delay(T1)beginnew(frametwo);frametwoA.Frametype := DM;frametwoA.PF := 0;frametwoA.Address := A;writestate(stn,6,4,2,2);OUTPUT SEND.DataRequest(frametwo);TxAttempts := TxAttempts + 1end;(' t8 ')provided TxAttempts > N2 ['2.4.4.4.2•)delay(T1)beginf' "initiate appropriate recovery actions" ')end;f' t9 "Ifrom SEND_SARM (•2.4.4.1')when RECV.DataRequestprovided (frameA.Frametype = SABM) (•2.4.4.5.1')beginnew(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 •)provided (frame.Frametype = DISC) (•2.4.4.5.2')to SEND_DMbeginnew(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;(' t11 ')provided (frameA.Frametype = UA) (•2.4.4.1•)to ABMbeginResetWindow;writestate(stn,3,20,3,4);OUTPUT P.Conlnd;TxAttempts := 0;dispose(frame)end;(' t12 ')provided (frameA.Frametype = DM) AND (frameA.PF = 1) ("2.4.4.1')to SEND_DMbeginTxAttempts := 0;dispose(frame)end;f' t13 ')provided otherwise (•2.4.4.1')to SEND_SABMbegindispose(frame)end;(' t14 ')from SEND_SABMprovided TxAttempts <= N2 ('2.4.4.1")delay(T1)beginnew(frametwo);frametwoA.Frametype := SABM;frametwoA.PF := 1;frametwoA.Address := B;writestate(stn,6,1,3,3);OUTPUT SEND.DataRequest(frametwo);TxAttempts := TxAttempts + 1end;f' t15 '}provided TxAttempts > N2 f'2.4.4.1")delay(T1)begin(' "initiate appropriate recovery actionsend;(' t16 ')from ABM (•2.4.5')when RECV.DataRequestprovided (frameA.Frametype^I) AND IsCorrectAck(frameA.NR)beginif (frameA.NR = LastRxNR) then (no frames acknowledged)beginendelse beginif (TimerRecovery = false) then beginwhile LastRxNR <> frameA.NR do beginLastRxNR := (LastRxNR + 1) mod Modulus;(' writestate(stn, 7, 25, 4, 4); ')OUTPUT P.Acklnd;end;Unacked := (VS + Modulus LastRxNR) mod Modulus;endelse beginif (frame'.NR = x) thenbeginframe'.NR := (frameA.NR + Modulus - 1) mod Modulus;end;(In the timer recovery condition, we need atleast one unacknowledged I-frame to pollwith. See 2.4.5.9 )while LastRxNR <> frameA.NR do beginLastRxNR := (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 1end;TxAttempts := 0; (one or more frames have been acked}end;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);beginif 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;endelse beginif 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;endelse• )(' Begin of WriteSFrame(RR,1,A) in APPENDIX C •)^ endLastRxNR := (LastRxNR + 1) mod Modulus;end^ OUTPUT P.Acklnd;end;dispose(frame);^ Unacked := (VS + Modulus - LastRxNR) mod Modulus;end; endif(frameA.NS <> VR) then else beginbegin if (clearrecovery = false) AND (frame".NR = x) thenend^ beginelse begin frame".NR := (frame".NR + Modulus - 1) mod Modulus;SendingREJ := false; (insequence I-frame received)^ end;VR := (VR + 1) mod Modulus;^ {In the timer recovery condition, we need atif frameA.PF = 1 then begin(' status request ') least one unacknowledged I-frame to poll(• Begin of WriteSFrame(RR,1,A) in APPENDIX C ') with. See 2.4.5.9 )new(frametwo);^ while LastRxNR <> frame".NR do beginframetwoA.Frametype := RR;^ LastRxNR := (LastRxNR + 1) mod Modulus;frametwo".PF := 1; OUTPUT P.Acklnd;frametwo".NR := VR; end;frametwoA.Address := A; VS := (frame".NR + 1) mod Modulus;(' writestate(stn, 7, 12, 4, 4); •}^ (in timer recovery, Unacked is always set to 1OUTPUT SEND.DataRequest(frametwo); end;LastTxNR := VR;^ TxAttempts := 0; (one or more frames have been acked}(• End of WriteSFrame(RR,1,A) in APPENDIX C ")^ end;end;^ f' End of ReadAck(frame".NR,clearrecovery) in APPENDIX C ')writestate(stn, 7, 20, 4, 4);OUTPUT P.DataInd(frame".Udata);^ if (frame".Address = A) AND (frameA.PF = 1) then beginend;^ (" status request ')end; if LocalRNR then beginend; (• 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); endOUTPUT SEND.DataRequest(frametwo);^ else beginOUTPUT 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); ')OR (frameA.Frametype = REJ) AND IsCorrectAck(frameA.NR) OUTPUT SEND.DataRequest(frametwo);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;(timer recovery is cleared when a supervisory response^ if (frame.Frametype RNR) then begin (• remote busy condition ')with Final bit set is received; see 2.4.5.9 ") RemoteRNR := true;(• Begin of ReadAck(frame".NR,clearrecovery) in APPENDIX C ') TxAttempts := 0;if (frameA.NR = LastRxNR) then (no frames acknowledged) endbegin^ else begin if (frameA.Frametype = REJ) ORend ((frame".Frametype = RR) AND RemoteRNR) then beginelse begin RemoteRNR := false;^ N,if (TimerRecovery = false) then begin^ if TimerRecovery = false then begin (' retransmit ")while LastRxNR <> frameA.NR do begin oldvs := VS;VS := LastRxNR;^ beginwhile VS <> oldvs do begin^ (' set FRMRBuffer ')(' Begin of WritelFrame(O,B) in APPENDIX C ')^ new(frametwo);new(frametwo); frametwo".Frametype := FRMR;frametwo".Frametype := I; frametwo".PF := 0;frametwo".Udata := RetxBuffer(VS)".Udata; frametwo".Address := A;frametwo".NS := VS;^ writestate(stn, 8, 6, 4, 5);frametwo".PF := 0; OUTPUT SEND.DataRequest(frametwo);frametwo".NR := VR; OUTPUT P.Disclnd;frametwo".Address := B; TxAttempts := 0;(' writestate(stn, 8, 8, 4, 4); ')^ dispose(frame)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 ABMend;^ beginend; 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;^ (' t21frametwo".NS := VS;^ provided (frame.Frametype = DISC) ("2.4.4.3•)frametwo".PF := 0; to SEND_DMframetwo".NR := VR; beginframetwo".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;elseUnacked := 0;^ (' t22 • )end^ provided (frame.Frametype = UA) •2.4.6.3")else begin (' remote busy, don't retransmit ')^ to SEND_SABMVS := x;^ beginUnacked := (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_SABMbeginnew(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;provided (frameA.Frametype = FRMR) •2.4.6.2')to SEND_SABMbeginnew(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_SABMbeginf• 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;(' 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 Cend;(' t28 ')when P.ResetReq ('2.4.7•)to SEND_SABMbeginnew(frametwo);frametwo".Frametype := SABM;frametwo".PF := 1;frametwo".Address := B;writestate(stn, 26, 1, 4, 3);OUTPUT SEND.DataRequest(frametwo);TxAttempts := 0end;(• t29 ')when P.DiscReq (•2.4.4.3')to SEND_DISCbeginnew(frametwo);frametwo".Frametype := DISC;frametwo".PF := 1;frametwo".Address := B;writestate(stn,22,2,4,6);OUTPUT SEND.DataRequest(frametwo);TxAttempts := 0end;(• t25 • )t24 • )t27when P.DataReq •2.4.5.1•)to ABMprovided ((RemoteRNR OR TimerRecovery OR (Unacked >= k)) = false)begin(• t26 •)provided otherwiseto ABMbegin(• should never happen •)end;( • Note that because S and P have independent queues, we don'tneed to worry about S requests in the other states:they'll be handled when the appropriate frames arrive at Pand the system enters state ABM. •)f• t30 ')from ABMprovided ((Unacked > 0) OR RemoteRNR)AND (TxAttempts <= N2) AND T1Running (•2.4.5.7/2.4.5.9')delay(T1)beginif Unacked = 0 then begin(' remote busy? poll with supervisory command • }if LocalRNR then beginnew(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 beginnew(frametwo);^ (• Begin of WriteSFrame(RNR,O,A) in APPENDIX Cframetwo'.Frametype := RR;^ new(frametwo);frametwo'.PF := 1; frametwo'.Frametype := RNR;frametwo'.NR := VR; frametwo'.PF := 0;frametwo'.Address := B; frametwo'.NR := VR;writestate(stn, 6, 7, 4, 4);^ frametwo'.Address := A;OUTPUT SEND.DataRequest(frametwo); (• writestate(stn, 6, 8, 4, 4); Iend;^ 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 •)^endTimerRecovery := true;^ else beginx := VS;^ (' Begin of WriteSFrame(RR,O,A) in APPENDIX C '}end;^ new(frametwo);new(frametwo); frametwo'.Frametype := RR;frametwo'.Frametype := I;^ frametwo'.PF := 0;frametwo'.Udata := RetxBuffer[VS)".Udata;^ frametwo'.NR := VR;frametwo'.NS := VS; frametwo'.Address := A;frametwo".PF := 1;^ (• writestate(stn, 6, 7, 4, 4); •)frametwo'.NR := OUTPUT SEND.DataRequest(frametwo);frametwo'.Address := B; LastTxNR := VR;writestate(stn, 6, 5, 4, 4);^ (• Begin of WriteSFrame(RR,O,A) in APPENDIX COUTPUT SEND.DataRequest(frametwo); end;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.DataRequestend; provided (frameA.Frametype = SABM) (•2.4.4.1")to ABM(* t31 •)^ beginprovided TxAttempts > N2 (*2.4.5.9•)^ new(frametwo);delay(T1)^ frametwo'.Frametype := UA;to SEND_SABM frametwo'.PF := frameA.PF;begin frametwo'.Address := A;new(frametwo);^ writestate(stn, 5, 3, 5, 4);frametwo'.Frametype := SABM;^ OUTPUT SEND.DataRequest(frametwo);frametwo".PF := 1; ResetWindow;frametwo'.Address := OUTPUT P.Conlnd;writestate(stn, 6, 1, 4, 3); TxAttempts := 0;OUTPUT SEND.DataRequest(frametwo);^ dispose(frame)OUTPUT P.DiscInd;^ end;TxAttempts := 0end;^ (' t35 ')provided (frameA.Frametype = DISC) •2.4.7.3•(* t32^ to SEND_DMprovided T1Running = false^ beginto 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;^ N,delay(T2)^ dispose(frame)to ABM end;begin^{' t36 ")^ to SEND_SABMprovided (frame".Frametype = DM) (•2.4.7:3•)^ beginto SEND_SABM^ new(frametwo);begin frametwo".Frametype := SABM;new(frametwo);^ frametwo".PF := 1;frametwo".Frametype := SABM;^ frametwo".Address := B;frametwo".PF := 1; writestate(stn, 6, 1, 5, 3);frametwo".Address := B; OUTPUT SEND.DataRequest(frametwo);writestate(stn, 4, 1, 5, 3); TxAttempts := 0OUTPUT SEND.DataRequest(frametwo);^ end;TxAttempts := 0;dispose(frame)^ (• t41 ")end;^ from SEND_DISC (•2.4.4.3•)when RECV.DataRequestt37 ")^ provided (frame".Frametype = SABM) (•2.4.4.5.2")provided (frame".Frametype = FRMR) (•2.4.7.3')^ to SEND_DMto SEND_SABM^ beginbegin new(frametwo);new(frametwo);^ frametwo".Frametype := DM;frametwo".Frametype := SABM;^ frametwo".PF := frame.PF;frametwo".PF := 1; frametwo".Address := A;frametwo".Address := B; writestate(stn,5,4,6,2);writestate(stn, 14, 1, 5, 3); OUTPUT SEND.DataRequest(frametwo);OUTPUT SEND.DataRequest(frametwo);^ TxAttempts := 0;TxAttempts := 0;^ dispose(frame)dispose(frame) end;end;(• t42 • )t38 •)provided otherwise (•2.4.7.3')to WAIT_SABMbeginif frame".PF = 1 then beginnew(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_SABMprovided TxAttempts <= N2 (•2.4.7.3•)delay(T1)beginnew(frametwo);frametwo".Frametype := FRMR;frametwo".PF := 0;frametwo".Address := A;writestate(stn, 6, 6, 5, 5);OUTPUT SEND.DataRequest(frametwo);TxAttempts := TxAttempts + 1end;t40 ')provided TxAttempts > N2 ("2.4.7.3•)delay(T1)provided (frame.Frametype = DISC) ("2.4.4.5.1•)to SEND_DISCbeginnew(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;t43 ")provided (frame".Frametype = UA) (•2.4.4.3•)to SEND_DMbeginTxAttempts := 0;writestate(stn,3,27,6,2);OUTPUT P.Disclnd;dispose(frame)end;(" t44 ")provided (frame".Frametype = DM) (•2.4.4.3")to SEND_DMbeginTxAttempts := 0;dispose(frame)end;(• t45 ")provided otherwise (•2.4.4.3')to SEND_DISCbegindispose(frame)end;t46 ')from SEND_DISCprovided TxAttempts <= N2 ('2.4.4.3')delay(T1)beginnew(frametwo);frametwo".Frametype := DISC;frametwo".PF := 1;frametwe.Address := B;writestate(stn, 6, 3, 6, 6);OUTPUT SEND.DataRequest(frametwo);TxAttempts := TxAttempts + 1end;(' t47 ")provided TxAttempts > N2 (•2.4.4.3')delay(T1)begin(' "initiate appropriate recovery actions" ')end;end;(•^body PLBody for aPhysicalLayer; external;^*3modvarDCE: anSLProcedure;DTE: anSLProcedure;user0 : anMLProcedure ;userl : anMLProcedure ;initialize (DataLink)begininit DCE with SLPBody(0);snit DTE with SLPBody(1);snit user° with MLPBody(10) ;snit userl with MLPBody(11)connect DCE.RECV to DTE.SEND;connect DCE.SEND to DTE.RECV;connect DCE.P to userO.Uu;connect DTE.P to userl.Uu;end;end. (DataLink)case 14: printfcase 15: printfcase 20: printfcase 21: printfcase 22: printfcase 23: printfcase 24: printfcase 25: printfcase 26: printfcase 27: printfswitch(sends)case 0: printf(case 1: printf(case 2: printf(case 3: printf(case 4: printf(case 5: printf(case 6: printf(case 7: printf(case 8: printf(case 9: printf(case 10: printf(case 11: printf(case 12: printf(case 13: printf(case 14: printf(case 16: printf(case 17: printf(case 20: printf(case 21: printf(case 22: printf(case 23: printf(case 24: printf(case 25: printf(case 26: printf(case 27: printf(default: printf(break ;===» nothing"); break;===» SABM"); break;===» DISC"); break;===» UA"); break;===» DM host ready"); break;===» I"); break;===» FRMR"); break;===» RR_cmd"); break;===» RNR command Receiver Busy"); break;===» REJECT command"); break;===» RR_resp"); break;===» RNR_resp"); break;===» REJ_resp"); break;===» bad_cmd"); break;===» ,bad_resp"); break;===» Ti"); break;===» N2XT1"); break;===» host_ready"); break;• ===» host_busy"); break;• ===» disc_req"); break;• ===» data_req"); break;clear_busy"); break;• ===» ack_ind"); break;• ===.» reset_req"); break;"===>> disc_ind"); break;"none");el("«=== Bad Command ");break;("<<=== Receiver Ready(RR_resp)("«=== host_ready"); break;(" «=== host_busy"); break;(" «=== disc_req"); break;("«=== data_req"); break;("«=== clear_busy"); break;("«=== ack_ind"); break;("<<=== otherwise"); break;("<<=== reset_ind"); break;");break;printf("^");printf("From : ");switch(initstate)case 1: printf("INIT");break;case 2: printf("SEND_DM ");break;case 3: printf("SEND_SABM ");break;case 4: printf("ABM");break;case 5: printf("WAIT_SABM");break;case 6: printf("SEND_DISC");break;case 11: printf("hostready");break;case 12: printf("hostbusy");break;case 13: printf("disconn");break;case 14: printf("datatrans");break;case 15: printf("linkreset");break;printf("^To : ") ;switch(finalstate)/ •^lapb.cBetween(a, b, c)int a, b, c;{if (a <= c)&&((a <= b) && (b <= c)) thenCorrectack := true;else if (a > c) && ((b <= c) II (a <= b))Correctack := true;elseCorrectack := false;IsCorrectAck(nr)int nr;if (TimerRecovery == false) thenBetween(LastRxNR, nr, VS);elseBetween(LastRxNR, nr, x);/• This procedure writes out the current host,^•II' incoming type of event or frame or command , and theI" current/initial state of host upon receival of eventwritestate(stn,rec_com,sends,initstate,finalstate)int stn;int rec_com;int sends ;int initstate;int finalstate ;printf("\n");printf("\n");switch(stn)case 0: printf("DCE "); break;case 1: printf("DTE "); break;case 10: printf("user0 "); break;case 11: printf("userl "); break;switch(rec_com)case 1: printf("«=== Timeout ");break;case 2: printf("«=== DISC Command ");break;case 3: printf("«=== UA Command ");break;case 4: printf("«=== DM Command ");break;case 5: printf("«=== SABM Command ");break;case 6: printf("«=== Timeout and N2 is MAX ");break;case 7: printf("«=== Information Frame ");break;case 8: printf("«=== Receiver Busy(RNR_resp) ");break;case 9: printf("«=== Lost Frame ");break;case 10: printf(" ");break;case 11: printf("«=== Frame Rejected ");break;case 12: printf("«=== RR_cmd(ACK) ");break;case 13: printf("<<=== Duplicate Frame");break;case 1: printf("INIT");break;case 2: printf("SEND_DM ");break;case 3: printf("SEND_SABM ");break;case 4: printf("ABM");break;case 5: printf("WAIT_SABM");break;case 6: printf("SEND_DISC");break;case 11: printf("hostready");break;case 12: printf("hostbusy");break;case 13: printf("disconn");break;case 14: printf("datatrans");break;case 15: printf("linkreset");break;printf("\n");) /•End of writestate Procedure V/* A procedure to display the outgoing event/* sent from host A to host Bw_send_data(Bns,Bnr,data)int Bns;int Bnr;int data;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)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;}= %d ACK NO = %d DATA = %d ",Bns,Bnr,data); writedatano(no)int no;printf("datano = %d \n", no);writerecvdatano(no)int no;printf("recvdatano = %d \n", no);NO = %d ACK NO = %d ",Bns,Bnr);^)writeiframesent(no)int no;printf("Iframesent = %d \n", no);printtimeout(timer)int timer;printf("\n");printf(" Sending data SEQ NOprintf("\n");w_send_sup(Bns,Bnr,data)int Bns;int Bnr;int data;printf("\n");printf(" Sending SUP frame SEQprintf("\n");w_rece_data(Bns,Bnr,data)int Bns;int Bnr;int data;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;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 BApplying Procedure 1 in Section3.3 to X.25 LAPBAPPENDIX B. APPLYING PROCEDURE 1 IN SECTION 3.3 TO X.25 LAPB^133SABM,B,1 a DISC,B,1 i RNR q_ ConReq 1SABM,?,0 b DM,A,O j REJ r ConInd 2SABM,?,1 c DM,A,1 k I s DiscReq 3 .UA,A,O d DM,?,1 1 BAD _ ^_ DiscInd 4UA,A,1 e FRMR,?,? m OTHER1,A,1 u ResetReq 5 _UA,?,? f_ FRMR,A,O n OTHER2 ResetInd 6DISC,?,0 g FRMR,A,1 o OTHER3 w DataReq 7DISC,?,1 h RR p OTHER4,?,1 x DataInd^, 8Appendix CFlowchart for Example 2 in Section3.5134APPENDIX C. FLOWCHART FOR EXAMPLE 2 IN SECTION 3.5^135while LastRxNR <> frameA.NR do beginLastRzNR*LastRxNR+1) mod Modulus;OUTPUT PAcklnd;Unacked:=(VS+Modulus-LastRxNR)mod Modulus;frameA.NR=VrameA.NR+Modulus-Dmod Modulus;while LastRxNR <> frame^.NRLastRxIIR:=(LastRxNR+1)mod Modulus;OUTPUT P.Acklnd,VS:=(frame^.i 1)mod Modulus; APPENDIX C. FLOWCHART FOR EXAMPLE 2 IN SECTION 3.5^136WriteSFrame(RNR,1A)SendingREJ:=false;VR*VR+ Dmod Modulus;ItaframeA.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;YNAPPENDIX C. FLOWCHART FOR EXAMPLE 2 IN SECTION 3.5 137li ^ReadAck(fraine.NR,clearrecovery);frame.Address = AAND frameA.PF =1WriteSFrame(RR,1,A)^IrameType(frame)=frameType(frame)REI OR RR)AND RemoteRNRRemoteRNR:= true;TxAttempts:=0;RemoteRNR :=false;1 TimerRecovery=false;moteRNR=f. •YVS:=LastRxNR; I VS:=x;Unacked:VS+Modulus-LastRxNR)mod Modulus;Unacked:);while VS<> xWritelFrame(0,B); 1G iiAppendix DHigh-level Description ofImplementationD.1 Preprocessing PhaseIn 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 anASN.1 type tree which is the result of ASN.1 parsing. The ISP (or OSP) parameters in thelist 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 consistsof ISP parameters with values and operators such as "EQUAL" and "AND", it is considered tobe a list of input symbols of a transition of the FSM. The "input.processed" flag allows betterperformance in the main analysis phase of trace analysis since we can filter out some candidatetransitions by matching input symbols with the traces without using symbolic simulation. Inorder to make the output symbols of a transition of the FSM correspond with the EFSM, theassignment 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, wecannot assign the value to the OSP parameters at this stage. The traces which contain theinput values will be processed in the main analysis phase only.Procedure 4.1:for each transitiondoif ISP (or OSP) exists,138APPENDIX D. HIGH-LEVEL DESCRIPTION OF IMPLEMENTATION^139find 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.fiodProcedure 4.2:for each transitiondo/* construct input of FSM using "PROVIDED" clause of Estelle.Y */if every predicate consists of ISP parameters with value and operatorssuch 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,doif 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 ".fiododD.2 Main Analysis PhaseFor simplicity, and in order to make the implementation fast and efficient without diminishingpracticality, we assume that the trace analysis starts in the initial state. In Procedure 4.3, weanalyze 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 eachtransition with respect to the same from_state. Also, the current pointers of traces beingprocessed, called "numofio_processed", are kept in order to process the correct trace from thetrace file.typedef struct pathAPPENDIX 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 valuesof 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 symbolicrepresentation of PDS using Procedure 4.4. If the predicate and the output primitives ofa transition resulting from Procedure 4.4 are satisfied in a trace, we can say that the traceconforms 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 satisfyingISPs, OSPs, and their parameters in the list created in the preprocessing phase withrespect to a trace corresponding to "numofio_processed".while(1)dowhile(if there is an unprocessed path)dowhile(if there is an unprocessed transition at from_state)doapply Procedure 4.4 to the transition with from_state and to_state.if the above is "YES",APPENDIX D. HIGH-LEVEL DESCRIPTION OF IMPLEMENTATION^141increment "numofio_processed" and log the status.fiododcopy the "Paths" containing "numofio_processed", to_state, values of variables and a set oftransitions 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.elseecho "no more traces exist. traces conform".stop.fifiodTraces not conforming to the formal specifications are those whose predicates are not sat-isfied 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.fiif the values of the variables obtained from symbolic simulation are the same as theOSP parameters,save the values to to_state.elsereturn.APPENDIX D. HIGH-LEVEL DESCRIPTION OF IMPLEMENTATION^142fifind 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 respectto a trace corresponding to "numofio_processed" and store those transitions in "Paths".if the transition is not spontaneous,return (YES).fiAppendix EAda Program having Data Racesprocedure ex isv : integer := 1;task type one isentry connect;entry disconnect;end;o:one;task type two isentry connect;entry disconnect;end;t:two;task body one isbeginloopt.connect;if ( v mod 2 > 0) thendelay 1.0;end if;v:= v + 1;accept disconnect;end loop;143To TtConcurrency BlockV:=V+1; V:=V+ 1;Concurrency Blockv:=v+ 1; v:=v+1;APPENDIX E. ADA PROGRAM HAVING DATA RACES^ 144end one;task body two isbeginloopaccept connect;if ( v mod 3 > 0) thendelay 1.0;end if;v:= v + 1;o.disconnect;end loop;end two;beginnull;end ex ;Figure E.1: Time-event Sequence DiagramAppendix FASN.1 Specification of X.25 LAPBLAPB DEFINITIONS ::=BEGINLapbToMlp ::= CHOICE{ConReq,DiscReq,ResetReq,DataReq,Con Ind,Disclnd,ResetInd,Datalnd,Acklnd}ConReq ::= SEQUENCE{dummy INTEGER}DiscReq ::= SEQUENCE145APPENDIX F. ASN.1 SPECIFICATION OF X.25 LAPB^ 146dummy INTEGER}ResetReq ::= SEQUENCE{dummy INTEGER}DataReq ::= SEQUENCE{datano INTEGERConlnd ::= SEQUENCE{dummy INTEGER}Disclnd ::= SEQUENCE{dummy INTEGER}Resetlnd ::= SEQUENCE{dummy INTEGER}Datalnd ::= SEQUENCE{datano INTEGER}Acklnd ::= SEQUENCE{dummy INTEGER}LapbToPhy ::= CHOICE{DataRequest,DatalndicatAPPENDIX F. ASN.1 SPECIFICATION OF X.25 LAPB^ 147DataRequest ::= 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}ENDAppendix GEstelle.Y Specification of X.25LAPBspecification DataLink;CONSTN2 = 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;VAR148APPENDIX G. ESTELLE. Y SPECIFICATION OF X.25 LAPB^ 149TxAttempts: 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;ISPConReq^mlp_lapb;DiscReq^mlp_lapb;ResetReq^mlp_lapb;DataReq^mlp_lapb;Datalndicat lapb_phy;OSPConlnd^mlp_lapb;Disclnd^mlp_lapb;ResetInd^mlp_lapb;Datalnd^mlp_lapb;Acklnd^mlp_lapb;DataRequest labp_phy;PDUFiller sent_in lapb_phy;APPENDIX G. ESTELLE. Y SPECIFICATION OF X.25 LAPB^ 150TIMERT1^2000;T2^1000;STATESEND_DM, SEND_SABM, ABM, ABMONE, WAIT_SABM, SEND_DISC;INITIALIZATIONTO SEND_DMBEGINTxAttempts := 0;END;TRANSFROM SEND_DMTO SEND_SABMWHEN ConReqOUTPUT DataRequestBEGINDataRequest.frametype := SABM;DataRequest.pf := 1;DataRequest.address := B;TxAttempts := 0;END;FROM SEND_DMTO ABMWHEN DatalndicatPROVIDED (DataIndicat.frametype = SABM)OUTPUT DataRequest, ConlndBEGINAPPENDIX G. ESTELLE. Y SPECIFICATION OF X.25 LAPB^ 151DataRequest.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_DMWHEN DatalndicatPROVIDED (Datalndicat.frametype = DISC)OUTPUT DataRequestBEGINDataRequest.frametype := DM;DataRequest.pf:= DataIndicat.pf;DataRequest.address := A;TxAttempts := 0;END;TO SEND_SABMWHEN DatalndicatPROVIDED (DataIndicat.frametype = DM)OUTPUT DataRequestBEGINDataRequest.frametype := SABM;DataRequest.pf := 1;DataRequest.address := B;APPENDIX G. ESTELLE. Y SPECIFICATION OF X.25 LAPB^ 152TxAttempts := 0;END;TO SEND_DMWHEN DatalndicatPROVIDED (Datalndicat.frametype = I) AND(Datalndicat.address = A) AND(Datalndicat.pf = 1)OUTPUT DataRequestBEGINDataRequest.frametype := DM;DataRequest.pf := 1;DataRequest.address := A;END;TO SEND_DMWHEN DatalndicatPROVIDED (Datalndicat.frametype = RR) AND(Datalndicat.address = A) AND(Datalndicat.pf = 1)OUTPUT DataRequestBEGINDataRequest.frametype := DM;DataRequest.pf := 1;DataRequest.address := A;END;•FROM ABMTO ABMWHEN DatalndicatPROVIDED (Datalndicat.frametype = I) AND (Datalndicat.nr = LastRxNR)AND (LocalRNR=false) AND (Datalndicat.ns = VR) AND (Datalndicat.pf = 0)OUTPUT DataIndAPPENDIX G. ESTELLE. Y SPECIFICATION OF X.25 LAPB^ 153BEGINSendingREJ := false;VR := (VR + 1) mod Modulus;END;TO ABMONEWHEN DatalndicatPROVIDED (DataIndicat.frametype = I) AND(DataIndicat.nr <> LastRxNR) AND (TimerRecovery = false)OUTPUT AcklndBEGINLastRxNR := (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 ABMONETO ABMONEPROVIDED (tmpnr <> LastRxNR)OUTPUT AcklndBEGINLastRxNR := (LastRxNR + 1) mod Modulus;Unacked := (VS + Modulus - LastRxNR) mod Modulus;TxAttempts := 0;END;FROM ABMONETO ABMPROVIDED (tmpnr = LastRxNR) AND LocalRNR AND(tmppf <> 1)APPENDIX G. ESTELLE. Y SPECIFICATION OF X.25 LAPB^ 154BEGINuseless := 0;END;FROM ABMONETO ABMPROVIDED (tmpnr = LastRxNR) AND Loca1RNR AND(tmppf = 1)OUTPUT DataRequestBEGINDataRequest.frametype := RNR;DataRequest.pf := 1;DataRequest.nr := VR;DataRequest.address := A;LastTxNR := VR;END;FROM SEND_DISCTO SEND_DISCPROVIDED TxAttempts <= N2OUTPUT DataRequestBEGINStart(T1);DataRequest.frametype := DISC;DataRequest.pf := 1;DataRequest.address := B;TxAttempts := TxAttempts + 1END;END.Appendix HEstelle Specification of DinningPhilosophers/* this Estelle specification was written by Limin Zhu, June 1991 */MODULE philoso PROCESS (id : lable); IPRp: 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;TRANSWHEN T.okFROM Room_Enter TO Left_PickBEGINOUTPUT Lp.pick;printleft_pick(id);END;TRANSWHEN Lp.fork_provided155APPENDIX H. ESTELLE SPECIFICATION OF DINNING PHILOSOPHERS^156FROM Left_Pick TO Right_PickBEGINOUTPUT Rp.pick;printright_pick(id);END;TRANSWHEN Rp.fork_providedFROM Right_Pick TO EatingBEGINprinteating(id);End;MODULE fork PROCESS (f_id : lable); IPR: phil_fork(ch_fork) INDIVIDUAL QUEUE;L: phil_fork(ch_fork) INDIVIDUAL QUEUE;END;BODY fork body FOR fork;TRANSWHEN R.pickFROM Available TO TakenBEGINOUTPUT R.fork_provided;END;TRANSWHEN L.pickFROM Available TO TakenAPPENDIX H. ESTELLE SPECIFICATION OF DINNING PHILOSOPHERS^157BEGINOUTPUT L.fork_provided;printleftforktaken(f_id);END;