UBC Theses and Dissertations

UBC Theses Logo

UBC Theses and Dissertations

Structuring requirements specifications Khanna, Vittu 1998

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

Item Metadata

Download

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

Full Text

STRUCTURING REQUIREMENTS SPECIFICATIONS by Vittu Khanna B.Sc. (Physics), Panjab University, India, 1991 M.Sc.(Physics), California Institute of Technology, 1993 A THESIS SUBMITTED IN PARTIAL FULFILLMENT OF THE REQUIREMENTS FOR THE DEGREE OF MASTER OF SCIENCE in THE FACULTY OF GRADUATE STUDIES DEPARTMENT OF COMPUTER SCIENCE We accept thjfsljhesis as conforming to the required standard THE UNIVERSITY OF BRITISH COLUMBIA July 1998 ©Vittu Khanna, 1998 In presenting this thesis in partial fulfilment of the requirements for an advanced degree at the University of British Columbia, I agree that the Library shall make it freely available for reference and study. I further agree that permission for extensive copying of this thesis for scholarly purposes may be granted by the head of my department or by his or her representatives. It is understood that copying or publication of this thesis for financial gain shall not be allowed without my written permission. Department of CQMPUT££ CC J^AJCL^ The University of British Columbia Vancouver, Canada Date f c P DE-6 (2/88) Abstract S^tructure is used to enhance the understandability of source code comprising a software-system. To study whether structure may enhance the understandability of software requirements specifications, this thesis investigates the application of two source code comprehension tools, Software Reflexion Models and Rigi, to requirements specifications. Two example specifications are studied using the tools. Further, a component (or scope) primitive for the Z specification language is proposed to help add structure to requirements. The example specifications in the extended Z have been rewriten using the component primitive. We conclude that this extension may not only help in increased comprehension but also in the prevention of some errors. ii TABLE OF CONTENTS Abstract ii Table of Figures v i Acknowledgments vi 1. INTRODUCTION 8 1.1 Motivation 8 1.2 Overall Method 4 1.3 The example specifications 5 1.3.2 The Radiation Therapy Machine 6 1.3.3 Why we used these particular specifications 6 1.4 The Tools 7 1.5 Thesis Outline 8 2. REQUIREMENT ANALYSIS: SPECIFICATION AND STRUCTURE 9 2.1 Introduction 9 2.2 Requirement Analysis and Specification 10 2.2.1 Requirement Analysis 10 2.2.2 Requirements Specification 11 2.3 Different Types of Specifications 12 2.3.1 Ad-Hoc Natural Language Specification Approach 13 2.3.2 Semi-Formal Methods 13 2.3.2.1 Structured Analysis 13 2.3.3 .2 Threads-Based Technique 14 2.3.3 Object-Oriented Methods 14 iii 2.3.4 Formal Notation 15 2.4 Formal methods 15 2.4.1 Formal Specification Language, Z 16 2.5 Structuring Requirements 19 2.5.1 The Change Process 19 2.5.2 Structure of a System 20 2.5.2.1 Modularity 20 2.5.3 Structuring Primitives 22 2.5.3.1 Refinements 22 2.5.3.2 Abstraction 23 2.5.3.3 Summarization 23 2.6 Summary 24 3. STRUCTURE COMPREHENSION TOOLS 2 5 3.1 Introduction 25 3.2 RIGI 27 3.3 Software Reflexion Models 29 3.4 Using Source Code Comprehension Tools for Requirements 33 3.5 Experimentation 33 3.6 Summary 34 4. COMPREHENDING SOFTWARE REQUIREMENTS SPECIFICATIONS 3 5 4.1 Introduction 35 4.2 Rigi 36 4.2.1 The Different Levels 37 4.3 Software Reflexion Model 59 4.1.1 Observations and their Implication 62 4.3 Software Reflexion Model and Rigi: A comparison 71 4.3 Summary 72 5. STRUCTURED SPECIFICATIONS 74 5.1 Introduction 74 5.2 The two structured specifications 76 5.2.1 The Telereg specification 77 iv 5.2.2 The Radiation Therapy Machine specification 77 5.2 Summary 77 6. R E L A T E D W O R K 7 9 7 . C O N C L U S I O N 8 2 7.1 Future Work 84 B I B L I O G R A P H Y 8 5 APPENDIX A Source model for telereg in the Software Reflexion Model 89 APPENDIX B The mapping file for the Software Reflexion Model f 0 APPENDIX C The high level model for the Software Reflexion Model <?'/ APPENDIX D Telereg - structured specification 92 APPENDIX E Radiation therapy machine - " ' Structured specification v Table of Figures Figure 2.1: Uses of a Requirement Specification[7, p. 14] .—12 Figure 3.1: Software Reflexion Model[25-p.20] 30 Figure 4.1 : Level 1 39 Figure 4.2: the source model for the call relation 40 Figure 4.4: Level 2 41 Figure 4.5: Level 3 42 Figure 4.6: Level 4 43 Figure 4.7: Level 5 4 4 Figure 4.8: The entire 'structured' telereg specification 45 Figure 4.9: Unstructured Telereg specification 47 Figure 4.20: Level 1 45 Figure 4.11: Level 2 50 Figure 4.12: Level 3 51 Figure 4.13: Level 4 52 Figure 4.15: The Delta relation in the Telereg specification 54 Figure 4.16: The call/include relation - Radiation Therapy Machine . 55 Figure 4.17: The Xi relation-Radiation Therapy Machine 56 Figure 4.18: The Delta relation- Radiation Therapy Machine 57 Figure 4.19: Telereg specification viewed syntactically 58 Figure 4.20: The Include relation in the Telereg specification 59 Figure 4.21: Reflexion Model of Telereg Specification . 60 Figure 4.22: Reflexion Model of Radiation Therapy Machine Specification 61 Figure 4.23: Division of the Telereg 63 Figure 4.24: A more detailed view 63 Figure 4.25: The most detailed specification of the Telereg system. As expected there are no relations between telereg_state and globaljypes. _65 Figure 4.26: The Telereg System - Typed Reflexion Model 67 Figure 4.27: Typed Reflexion Model - Radiation Therapy Machine 69 Figure 4.28 70 vi Acknowledgments I would like to thank Dr. George Tsiknis for his help and guidance at the various stages of research and for his invaluable comments and criticisms on the thesis. I would also like to thank Dr. Gail Murphy for carefully going through this document and for her helpful comments as well as useful answers to my numerous questions on the Software Reflexion Model tool. In addition, I am grateful to Jonathan Jacky, Johannes Martin and Kenny Wong for their prompt replies to my email queries on the Radiation Therapy Machine and the Rigi tool. Finally. I would like to express my gratitude to my family and friends, who made this possible for me. I would like to thank my parents for always believing in me and my brother who helped me tremendously. I would like to express my deep gratitude to my spouse, Yogesh, not only for his precious bits of advice, but also for the nights he spent in the lab, helping me in my thesis work. I could not have done it without his help. vii Chapter 1 Introduction "Where shall I begin, please your majesty?" he asked. "Begin at the beginning", the king said gravely, and go on till you come to the end: then stop." -Lewis Carroll, Alice's Adventures in Wonderland, Ch. 11 1.1 Motivation More than 50% of software evolution work is devoted to system understanding[32]. As the overall system becomes large and complex, system structure becomes an issue[32]. For a large system, understanding the structural aspects of the system's architecture is more important than understanding any single algorithmic component. Documentation that exists for these large systems usually describes isolated i parts but not the overall architecture. An overall view of the system structure helps in system understanding and, therefore, may ease the other software engineering phases. Software structure may be defined as follows: "Software structure is the collection of artifacts used by software engineers when forming mental models of software systems. These artifacts include software components such as procedures, modules, interfaces and subsystems; dependencies among components such as client-supplier, inheritance and control-flow; and attributes such as component-type, interface size, and interconnection strength. A system's structure is the organization and interaction of these artifacts"[34, p.47]. In order to structure the system, some concepts used are subsystem structures; layered structures; aggregation, generalization, specialization and inheritance hierarchies; resource-flow graphs; component and dependency classification; event-handling strategies; and client-server and distributed architectures[2]. At the beginning of most software projects, the customer provides the contractor with a statement of requirements. Typically, the customer statement of requirements is expressed in natural language using technical terms of the customer application domain. The contractor will derive a requirement specification from the customer statement of requirements that describes the requirements in more detail. The process of identifying and understanding the customer requirements is called requirements analysis. This analysis phase also requires that the contractor determine the feasibility of the proposed system. The Requirement Specification is the end product of the requirement analysis phase in the software development cycle. The need to state the requirements of a system correctly, precisely and completely early in the software development cycle is essential to successful software development. Boehm[2] reports that there are quantitative benefits gained from resolving requirement problems in the early phases of the software life cycle. The later 2 defects are found in the development cycle, the more expensive is the cost of the software development. As this initial task of specifying and deriving the requirements drives the later stages of the software development process, it is crucial to establish the requirements correctly and precisely. Establishing the correctness and precision of requirements is difficult: structure may be helpful to enable a better analysis and understanding of the system under development. It is not yet well understood what in structure may be important for the requirements and which techniques may apply. Structure in requirements may play two roles. First, structure may help in comprehension of requirements. Second, it may help reduce errors when specifying requirements. In terms of comprehension, as the requirement specification document becomes large, it gets more and more involved and complicated. Such a document is very difficult to understand and analyze to produce good effective software. To understand such a large specification, it is useful to be able to view the structure of the requirements from different points of view. Structure may also help prevent errors that creep in when a developer writes a specification. In a paper by Betrand Meyer , these errors are referred to as the seven sins of the specifier and are as follows[22, p.7]: • Noise: The presence in the text of an element that does not carry information relevant to any feature of the problem. • Silence :The existence of a feature of the problem that is not covered by any element of the text. • Over Specification: The presence in the text of an element that corresponds not to a feature of the problem but to features of a possible solution. 3 • Contradiction: The presence in the text of two or more elements that define a feature of the system in an incompatible way. • Ambiguity. The presence in the text of an element that makes it possible to interpret a feature in at least two different ways. • Forward reference: The presence in the text of an element that uses features of the problem not defined until later in the text. • Wishful thinking: The presence in the text of an element that defines a feature of the problem in such a way that a candidate solution cannot realistically be validated with respect to this feature. Some of these errors may be detected by structuring the specification. For example, a part of the specification that shows no relation or dependencies on any other part may be considered as noise. Thus, the structure of the specification helps detect noise. Similarly, it can help detect ambiguity, over specification, forward references, etc. 1.2 Overall Method This research investigates the concept of structure and structure comprehension in requirement specifications. Two structure comprehension tools, the Software Reflexion Model tool [26] and Rigi [24], that are promising for source code analysis and comprehension, are applied to two sample requirement specifications and the results are analyzed. The two specifications used were a specification of the telephone registration system(Telereg) of the University of British Columbia[7] and a specification of a Radiation Therapy Machine[15]. Both specifications were written in the formal specification language, Z[31]. Z specifications were chosen because of their formal syntax and the 4 increasing popularity of the Z language in academia as well as industry. Our goal is to understand what structural concepts are important in the software specification domain and to determine if tools can help identify, comprehend and manipulate the relevant structural concepts. 1.3 The example specifications 1.3.1 The SIS-Telereg system The Student Information System (SIS) at UBC is designed to establish a single database for student information[7]. It allows decentralized update and inquiry access with appropriate access controls, and provides convenient interfaces to other centralized administrative systems. Support of comprehensive reporting and analysis is also provided as well as the flexibility to implement new policies and to support the changing needs of the University faculties and departments. Telereg is a telephone registration system, introduced in 1988. It is the student's interface to the SIS. It allows students to register for their courses from any touch-tone phone. The students use the buttons on the telephone keypad to enter requests and the computer's voice guides them through their registration. The students may request one or many operations concerning fee, confirmation of registration , etc. Further, details of each section are also provided such as adding a course, dropping a course, changing a course section, confirming a section, switching a section, canceling an entire registration, listing all of a student's courses and other related requests. The specification for this system, when written in the formal language Z, offers a precise, comprehensive and accurate description comprising 82 schemas. 5 1.3.2 The Radiation Therapy Machine People suffering from certain ailments find radiation therapy quite effective and helpful in alleviating many of their medical problems. The operator's console of a computer controlled radiation therapy machine supports administration of accurate doses of the right kind of radiation at a particular spot[15] . A wrong amount or improper radiation is not only a waste of time and money, more importantly, it might cause irreversible damage to parts of the body and even help in the progress of the disease instead of hindering it. Further some radiation can even cause serious defects and problems in future generations. Thus radiation, which has many benefits, if not administered properly, can be very detrimental. For this reason, it is very important to apply the correct amount of radiation to the right spot. A radiation therapy machine to be developed in conjunction with the University of Washington Radiation Department was partially formally specified. This formal specification[14], rather than a prose specification, serves as the primary reference source for programming and test planning for the software in the machine. The specified functions include selecting treatment setups from a database of stored prescriptions, setting up prescriptions on the treatment machine manually or semi-automatically, checking that the setup conforms to the prescription, safety interlocking and essential user interface features. This specification supports the concepts of physics and experimental procedures along with patient treatments and consists of approximately 100 schemas. 1.3.3 Why we used these particular specifications We used these two specifications in our study for the following reasons. 6 Both specifications are fairly large and cover a wide range of relations and operations. The specifications are written in the formal language, Z. This is a precise specification language that helps the user define the operations and other transformations clearly, precisely, accurately and in detail. Also, using this language, the variables and their types as well as functions can be well understood. This formal language is very similar to a programming language and since both the tools, Software Reflexion Model tool and Rigi, have been designed for programming languages, they can be adapted for the Z environment. Each specification has many instances of the containment as well as other component which we wanted to study in detail. The different occurrences of these relations give us an opportunity to study the different forms and ways in which they may be used. Furthermore, both of these specifications are very conducive to structuring. Segregations and divisions among the operations are well defined and usually follow a hierarchical pattern. 1.4 The Tools Both of the tools used, the Software Reflexion Model tool and Rigi are described in Chapter 3. Both of these tools help, in different ways, to investigate the structure of the system. Software Reflexion Model tools form a mapping between the high level model and source code [26]. On the other hand, Rigi uses the concept of reverse engineering in the identification of software artifacts in the subject system and the aggregation of these artifacts to form more abstract system representations [24]. These tools have been applied to source code and have been found useful for program comprehension. 7 1.5 Thesis Outline This thesis describes and analyzes the use of two structure comprehension tools, Software Reflexion Models and Rigi, in requirements specification. Chapter 2 discusses the concept of software structure, its importance in programs and how extending this structure to requirement specifications may be beneficial. Chapter 3 describes the two structure comprehension tools, Software Reflexion Model tool and Rigi. The application of the two tools to the two specifications is discussed in chapter 4. Chapter 5 discusses how structure imposed on the two specifications may enhance the understanding of requirements specification. Chapter 6 discusses some of the previous work done in this area and finally, Chapter 7 concludes and summarizes the work. 8 Chapter 2 Requirement Analysis: Specification and Structure "The hardest single part of building a software system is deciding precisely what to build. No other part of the conceptual work is as difficult as establishing the detailed technical requirements, including all the technical interfaces to people and machines, and to other software systems. No other part of the work so cripples the resulting system if done wrong. No other part is more difficult to rectify later." - Brooks, " No silver bullet: Essence and accidents of Software Engineering.", IEEE computer, Apr. 1987, p. 17 2.1 Introduction As the quote from Brooks above suggests, the most difficult and critical step in software development is the first one, understanding what the project is all about. Software requirement errors have been found to account for a majority of production software failures[4,10], and have been implicated in a number of accidents [20]. Errors introduced during the requirements phase can cost up to 200 9 times more to correct than errors introduced later in the life cycle [6]. Therefore, techniques to provide adequate requirements specifications and to find errors early are of great importance. The goal is to identify and understand the problem for which a solution is sought and to determine what is to be done. This stage is called the requirement analysis and specification stage. This stage has two components. The first, requirement analysis, involves stating the problem to be solved and the constraints that exist, on a successful solution to the problem. The second component is requirements specification that involves stating what is expected of the software to be built. 2.2 Requirement Analysis and Specification 2.2.1 Requirement Analysis One of the most challenging aspects of gathering and specifying requirements is to understand and analyze the sponsor's problem. Requirement Analysis deals mainly with the following questions[26,p. 45]: • Who is involved in the situation to be analyzed? Who will actually be using the proposed software? Will the users be highly trained individuals, computer novices, or both? • What is the current situation? What is it about the current situation that is posing a problem? What is the proposed system to be ? What functions are to be performed by the proposed system? • When must the new system be in place? When will the sponsor be ready to install and test the new system on site? 10 • Where will the new system fit into the old environment? • Why is a new system being sought? Why do users want to change the current system to a new system? • How will the new system function? Are there constraints on how the proposed system can operate? Once these important questions have been answered, we are naturally led to the requirements specification stage. 2.2.2 Requirements Specification The requirements specification describes both the functional and non-functional requirements of the system. The functional requirements describe the services that the system is expected to provide by specifying how the inputs to the systems are transformed into outputs. The requirements detail the inputs and their validation as well as the system changes to both normal and error conditions. Non-functional requirements describe the constraints under which the system must operate and any design restrictions imposed on the system, or more specifically, they include details on specific response times, memory requirements, hardware limitations, programming language to be used and any mandatory standards. The requirements specification describes what a system must do as opposed to how the tasks must be accomplished. This is an extremely important part of the software lifecycle because it is often seen as a contractual agreement between the customer and the contractor. Software specifications can be used for different purposes, including as: • a statement of user needs, 11 • as a statement of requirements for the implementation, and • as a reference point during product maintenance. Above all, the requirements specification is the base document, used for all subsequent developmental activities(Figure 2.1). Customer Requirements Specification Figure 2.1: Uses of a Requirement Specification^, p.14] This figure shows the relation of the requirements specification to other of the software lifecyle. 2.3 Different Types of Specifications Many methods can be used to specify requirements in a software system. They differ in terms of expressiveness, features and ease of use. Some of the different methods may be classified as ad-hoc natural language, semi-formal, object-oriented, or formal. 12 2.3.1 Ad-Hoc Natural Language Specification Approach This is an informal type of specification that is the most commonly used in industry today. This approach organizes requirements into certain predefined sections, and each section is written in natural language using a free-style format. Writing requirements in natural language is ad-hoc and open-ended. This approach is subject to ambiguity and imprecision because these properties are inherent in natural language, which is used for the specification. 2.3.2 Semi-Formal Methods 2.3.2 .1 Structured Analysis This is a semi-formal type of specification technique that combines the use of natural language and graphical symbols with some semantics [8]. This methodology describes a system as a function from inputs to outputs. This has a well-defined syntax and loosely defined semantics. Structured Analysis offers a top down specification of the system structured mostly in terms of a set of hierarchical data-flow diagrams. 13 2.3.3 .2 Threads-Based Technique This is a structured informal specification technique, that is a refinement of the natural language approach. Its basis is the concept of a thread, defined as a "path through a system that connects an external event or stimulus to an output event or response[9]. This technique focuses on external stimuli and responses, and is a method for writing requirements in natural language in a structured manner where the stimuli and responses are made explicit. This method applies only to the functional requirements section of a system requirements document. It consists of a series of statements, each relating an external stimulus to an external response. The threads-based approach partitions the functional requirements of a system into basic specification units called threads, capabilities and conditions. 2.3.3 Object-Oriented Methods In object-oriented methods, like Objectory[16] and UML [5], the system requirements are specified in terms of domain objects, their relations and their interactions. In the Objectory method, the different "use cases" of the system are first identified , and the functional requirements for each such case are modeled using a mixture of diagrams and English text. After a series of analysis and transformations, the requirements are evolved into a design specification. 14 2.3.4 Formal Notation Webster's Dictionary defines formal as definite, orderly, and methodical. Thus, to be formal does not necessarily require the use of formal logic, or even mathematics. But in computer science, the phrase "formal methods" has acquired a narrower meaning, referring specifically to the use of a formal notation to represent system models during program development. An even narrower sense refers to the formalism of a method for system development. Typically, first a specification is written in a formal notation and then refined step4?y-step into code[21]. Formal methods include the use of mathematical notations such as logic and set theory to describe system specifications and software design together with techniques of validation and verification based on mathematics. These provide very accurate and unambiguous specifications. Hall gives an account of the use of formal methods to eliminate errors: "In an informal software specification, it is hard to tell what is an error, because it is not clear what is being said. When challenged, people try to defend their informal specification by reinterpreting it to meet the criticism. With a formal specification, we found that errors are much more easily found - and once they are found, everyone is more ready to agree that they are errors."[12, p. 13] 2.4 Formal methods The use of formal methods to "write specifications can help minimize errors and can help in precision[21]. Large systems are difficult to develop because they 15 are conceptually complex and because they are likely to contain errors. Formal specifications give some control over both these problems. First, formal specifications allow the use of abstractions to design large systems, thus reducing their conceptual complexity. Second, formal specifications enable computer-aided design tools to be based on rigorous methods, which can reduce the incidence of errors; this reduces the effort spent on detailed design and implementation of faulty requirements. Informal specifications, on the other hand, are often ambiguous, requiring direct communication between programmers and designers for clarification. Formal methods are very precise and for this reason they are gaining in popularity. One formal language in use is Z. 2.4.1 Formal Specification Language, Z One of the most popular formal specification notations that has been used successfully in several industrial applications is the formal specification language, Z[31]. Z is a machine readable mathematical notation with set theory and first order logic as its basis. A specification written in Z consists of formal mathematical statements that give a precise description of the system. These statements describe the operations performed on data objects. They specify the system state before processing an event (initial state) and after processing the event (final state). This is interspersed with informal text that describes in natural language the meaning of the mathematical statements to make the specification more readable. Z is used to specify a mathematical model of the system consisting of objects and their relationships. The interactions between the various objects 16 describe the requirements. The objects are made of elements called basic types. The building blocks for the basic types are sets and functions. Tools are available to provide automatic checking for type consistency across the specification. Thus, the requirements of a system are described in terms of logic expressions that define sets that describe the data objects of the model, their relationships and the operations performed on them. A Z specification is structured so that it can be developed incrementally and consists of mathematical statements that are packaged together in schemas. Schemas define states and transitions among the states. The top line of the schema introduces the schema name and the part between this and the dividing line is called the signature. The signature sets out the names and types of the entities used in the schema. The schema predicate (the bottom part of the schema) sets out the relationships between the entities in the signature by defining a predicate over the signature entities. A schema may be expressed in terms of other schemas and is accompanied by explanatory text that explains the mathematical statements. For example, consider a schema, PrescribedPatients, in the Radiation Therapy Machine specification: this schema is used to select a prescribed patient for the use of the machine. 17 PrescribedPatient SessionVars patient ;*no_patient patiente names field = no_field v field e dom fields if mode = therapy then Prescribedpatient else Presetpatient mode = therapy => counters = Accumulated patient This schema includes another schema calledSessionVars and describes some operations performed on variables that are defined in SessionVars. The signature is the part above the dividing line and the predicate is the part below the line. The signature part declares the variables used in the schema's operation and the predicate part describes the operations. The predicate consists of statements. In this example, the predicate has five statements defining the operations of the machine depending on the status of the patient. Z allows many operations to be performed on the schemas. A few of these are Delta(indicating use of and a change to variables), Xi(indicating use but no change to variables), schema inclusion, schema disjunction, schema conjunction, schema negation, schema composition etc. A detailed description of the Z language may be found in [28]. 18 2.5 Structuring Requirements 2.5,1 The Change Process Any useful software system continually evolves [19]. Changes in such a system are the result of many factors. Some of these may be requests by clients to add more functionality to the system or to improve the maintainability or quality of the code. To help the software engineer perform the above tasks effectively, it might help the engineer to have some understanding of the structure of the system. In a process that evolves continuously, the software developers and managers must deal with various requests for change. Some of these affect the resulting behavior of the system whereas others affect the non-functional characteristics of the system. As the structure of the system plays such an important role in the cost of change, information about the structure may be beneficial to an engineer reasoning about a system during the change process [25]. Structuring is a good way of organizing complicated information to make easier to learn. Error detection and correction is typically easier to locate the effects of the error ( and thus more errors are located) in a structured system. It is much more difficult to detect omissions or overlaps in a system without structure. If a system is unstructured, the whole system has to be learnt, a daunting process. On the other hand, structured systems are easier to update, to test, and to visualize. Structure may also reduce the overall size of the system. Just as it is the case in programming, structuring may be of great use in writing specifications. 19 2.5.2 Structure of a System Requirements specification plays an important part in requirements understanding. Structuring help ease the understanding of the requirements specification by using views, perspectives and abstractions. Views represent partial descriptions of the information system focusing on the requirements of a single group of users[12]. Perspectives specify the requirements concentrating on different aspects and abstractions allow the developer to describe the system at different levels [12]. These three structural mechanisms have mostly been studied in isolation. The need to support views, perspectives and abstractions has increased for many reasons: to support communications between developers in large projects, to reuse previous artifacts as well as, to organize requirements of legacy systems to re-engineer them. In order to achieve these goals, tools are needed to manage these different aspects and to provide static and dynamic links between them [12]. Like a program, a specification is comprised of various parts or components. These components may be parts of the static view or may also extend to the system's dynamic view. In each view, interactions, commonly known as relations may occur between the components. These are examples of the aspects of the specification that define the structure of the specification. One principle that has been adopted in the area of software design that is also important for the field of requirement specification is modularity. 2.5.2.1 Modularity Modules are the basic building blocks of the software structure. A well-structured system that follows the basic principles of software design should exhibit a logical and 20 modular structure and support information hiding [8]. Design decisions should be isolated from one another in a way that minimizes the impact of changes in those decisions. Of the various qualities of software design, none has proven over time to be more significant than modularity. A system can be structured into a collection of modules, where each module has a well-defined interface to other modules, carries out a well-defined function, hides a design decision and can be independently tested and verified. For modularity, there are several partitioning approaches, including: • functional decomposition which is based primarily on assigning functions to modules, • data-oriented decomposition which is based on external data structures, • event-oriented decomposition which is based primarily on events that the system must handle, • outside-in design which is based on user inputs to the system, and • object-oriented design which is based on classes of objects and their interrelationships One or more of these approaches are typically used in conjunction[23]. Modules should be cohesive, loosely coupled and modules should be black boxes. In requirements specification as well, modularity is important because: • duplication of declarations can be avoided by declaring items in only one interface and importing them from there, • information hiding is encouraged. • key structural decisions are emphasized, and • the visibility of structure in the specification is increased. A requirements engineer wanting to make a change may spend a lot of time sifting through the specification to obtain information to help make the decision. Modularity increases the visibility of the system, so the requirements engineer can spend more time understanding and deciding, rather than gathering, the information on which to base the decision. 21 2.5.3 Structuring Primitives Along with modularity, some other primitives have been proposed as structuring mechanisms. The primitives that are more likely to be used in requirements specification include[12]: 1. refinement, view and integration, 2. abstraction, and 3. summarization. 2.5.3.1 Refinements Refinements allow modeling the same piece of reality in terms of several schemes at different levels of abstraction. The refinement is the typical paradigm used in so called top-down methodologies developed for functional analysis. The different levels are called refinement planes since they refer to the same piece of reality at different levels of abstraction [30]. Refinement planes are a fundamental documentation tool since they allow to perceive a complex reality to be perceived step-by-step, through a generative approach; each step focusing on a limited set of details. In the case of requirements specification, this construct may be explained taking the specification of a birthday book in Z as an example[31]. The birthday book specification records a set of the birth dates, matching the dates with respective names. Further, birth dates may be added, deleted or changed. In such a specification, one schema may depict the overall picture of the birthday book. Another schema that is included in the above schema may detail the mechanism of adding a birthday, yet another may exclusively 22 concentrate on deleting a birthday, and a third schema on changing a birth date. The specification thus follows a hierarchical structure based on refinement. 2.5.3.2 Abstraction In computer science, abstraction generally refers to the process of creating a construct that represents selected information in a more compact form than the information itself [31]. When the details of the underlying information are hidden, this process is also referred to as information hiding. In the case of requirements specification, taking the example above, the first schema gives an overall view of the birthday book, including schemas that are described below. These schemas are not defined in the initial schema in which they are included: this is an example of the concept of information hiding. 2.5.3.3 Summarization "Using summarization, an engineer can flexibly explore the structure of a large system at a reasonable cost. Summarization involves the production of overviews of vast amounts of user-selected information in a timely manner. An overview produced by a summarization process lets detail of the underlying information show through as compared to an overview produced by an abstraction process that hides the underlying detail"[25, p. 186]. The technique of summarizing is one commonly used to aid in understanding a problem as well as remembering it. An overview produced by summarization in the case of requirements specification can allow the details of relations to be depicted. For example, in Z, the various relations may include Delta and Xi relations. 23 We explore, in this research, an appropriate combination of refinement, abstraction and summarization to help understand requirements specification. 2.6 Summary Specifying requirements is a very important part of the software process. It constitutes analysis of the requirements as well as specifying them accurately and in accordance with the customer's needs. For a reasonably large system, there may be a large number of requirements. Understanding these requirements not only enhances understanding of the system, but also helps in the later stages of software development. Further, maintenance of the requirements is important; it is a necessary aspect of software development. Changes in the software, such as additions and deletions, require a change in the requirements specification. Improving the support for structure in specifications may help ease understanding and maintenance tasks. In this chapter, we have discussed some of the different ways of specifying requirements as well as the constructs used to structure them. The comprehension tools we use to bring out the structure and help in understanding the requirements, and the significance of these tools are discussed in the next chapter. 24 Chapter 3 Structure Comprehension Tools "Designing the software structure is the most critical step in creating a good, working software system. The software structure is the framework or skeletal structure of the software system. If the software structure is not well designed, the system will be difficult to build, test and maintain." - Mills, H.D., Structured Programming: Retrospect and Prospect" IEEE Software. Nov. 1986 p. 58. 3 . 1 I n t r o d u c t i o n It has been suggested that more than 50 percent of software evolution work is devoted to program understanding [34]. Program structure is imperative for program understanding and consequently, maintenance. For the same reasons, it is likely that this argument is also valid for the requirement specification process. Specifying requirements in a structured manner may increase the understandability of the system, which can improve and expedite the process of change, maintenance, and many other activities in software development. 25 Program structuring has reduced much of the unnecessary complexity of programming. Unlike a spaghetti program, a structured system defines, among other things, a hierarchy among its components: components may be repeatedly nested into larger and larger parts of the system according to the concept of top-down programming. For large legacy systems, understanding the structural aspects of the entire system's architecture is typically more important than understanding any one small component. Documentation usually describes isolated parts of the system but not the whole architecture. The different kinds of the components and relations comprising the source, as well as their distribution over a program makes it difficult for a software engineer to gain an understanding of a system's structure and also complicates the construction of tools to support the engineer in the understanding process. Another problem faced by both the engineer and the tool provider is the amount and the complexity of structural information that must be considered. This obvious diversity increases the need for techniques and tools necessary to support an engineer during the "comprehension of the system" process. We need tools that are flexible in handling a variety of structural information and that are also able to scale to support the large amounts of structural information embedded in most software systems. Based on these observations, various tools have been developed. These tools or techniques may be classified into three categories: program visualization, reverse engineering and (design) conformance tools. Although, a lot of work has occurred in studying the role of structure in programs, not much work has occurred on the importance of structure in requirements. We study this area and try applying the various ideas used in programming to requirement specifications. The program understanding tools when effectively used in requirement specification may increase understanding, may reduce errors, and may help in building the system 26 effectively. Consider a large system whose specification constitutes hundreds, in terms of the specification language Z, of schemas. Such a specification would be very difficult, if not impossible, to understand. Using the tools described in the next sections, a graphical representation of the specification can be created that may greatly help understand the specification. The focus of the thesis is on the use of two of these tools (described ahead) in requirement specifications. Are there any differences between their use in programs and requirements specifications? What are the advantages and disadvantages of using these tools for requirement specifications? How can further research be done in this area? As an attempt to answer the above questions, we explore this area. Before describing the study done in this area, we will give a brief overview of the tools and the two example specifications. 3.2 RIGI The term software visualization is used to describe many different processes. To visually present software artifacts and structure, graphs are particularly suitable. Nodes in the graphs typically represent system components and directed arcs represent the dependencies among these components. However, as the size of software systems increases, so to do their representations as graphs. Advanced graphics and abstraction techniques are needed to manage the visual complexity of these large graphs. The Rigi reverse engineering system is designed to extract, navigate, analyze and document structure of large software systems[32]. This interactive, visual tool was designed at the University of Victoria to help a software engineer better understand and redocument software1. 1 Details may be obtained from http://www.rigi.csc.uvic.ca/ 27 The process of reverse engineering is concerned with the analysis of existing software systems so that they are better understood for maintenance, reengineering and evolution purposes[24]. The system is represented in a form where many of its structural and functional characteristics can be visible. This knowledge is then used to improve subsequent development, ease maintenance, re-engineer and aid project management. The reverse engineering process involves two distinct phases [24]. Parsing the software and storing the extracted artifacts constitutes the first phase. This phase is usually fully automatic. The next phase is typically semi-automatic and helps a developer obtain a model of the structure of the software system. The second phase involves pattern recognition skills and features subsystem composition techniques to generate multiple, layered hierarchies of higher-level abstractions. In this phase, the engineer employs various visualization aids to help recognize patterns, identify candidate subsystem, and to understand software structures in the graph. The Rigi tool has been developed and used for program understanding, software analysis, reverse engineering and programming-in-the-large. It focuses on querying, representing, visualizing, and evaluating the structure for large, evolving systems. The structure of the system is the organization and interaction between these modules. The methodology used in Rigi is that of subsystem composition which generates layered hierarchies of subsystems and thereby reduces the complexity of a large specification. Some of the features that promote the use of this tool include: [35] • an easy-to-use visual interface, • selection, filtering, and editing operations, • dependency and change reports, 28 • standard, overview, and projection perspectives, • metrics for cohesion and coupling, • views to capture interesting perspectives, • scripting language and command library, and • a customizable user interface. In an attempt to study and analyze structure in requirement specifications, we applied Rigi to two specifications. One of these, the radiation therapy machine specification, is a reasonably large specification consisting of about a hundred schemas. In studying Rigi in the context of requirement specification and we were interested to see how it depicts, among other things, the containment relation among schemas. Is it helpful in studying the system in varying levels of detail? Does it help in the understanding of the structure of the system? For example, can this tool help in detecting containment relations? How can requirement components be classified together using this tool? Can this tool be used for a more detailed analysis of the system? If so, how? 3.3 S o f t w a r e R e f l e x i o n M o d e l s This tool, developed by Gail Murphy at the University of Washington, gives a graphical representation of the high level model of a program and compares it with the source using the relations and interactions between the modules of the source model. This comparison is visualized as a reflexion model[25]. As shown in the Figure 3.1 below, this method basically involves four steps: 29 defining a high level model, extracting a source model, defining a map, and computing a reflexion model. 0 II Kj T l Software System Artifacts Source Model Extraction Tool Sou ice Made I © Figure 3.1: Software Reflexion Model[25-p.20] 30 The reflexion model, basically, provides a comparison between the source model and the high level model. This cost-effective and lightweight technique can help an engineer explore the structural aspects of a system in various levels of detail. Instead of requiring high-level models to be updated continuously, the software reflexion model technique reduces the risk associated with reasoning in terms of these modules by bridging the gap between the models and the source. Basically, the engineer uses a high-level model as a framework on which to summarize structural information extracted or collected from the software system's artifacts. The information provided in the reflexion model helps the engineer selectively investigate aspects of the system's source. Reflexion Models are used in programs not only to analyze and understand the source code, but also for confirming that a program matches the design. Therefore, they ease the understanding of the system by an analysis of the source code and also help in conforming the program to the system design. A series of reflexion models may be computed by an engineer to investigate the structure of the system. Thus, the high level model, the mapping and/or the source model may be varied between the computations. As these three inputs are varied, more detail can be added to produce a more detailed reflexion model. Further different 'views' may be studied. For example, different levels of detail of the Telereg System were examined and this lead to a more detailed and clearer understanding. Consider an example which depicts the use of this tool for source code. "An engineer, who has no experience with the NetBSD2 implementation is asked to estimate the cost of changing the virtual memory subsystem of the NetBSD Unix operating system to page across a network rather than to a file system, in five days" [25, p.29]. To provide such an estimate, the engineer needs to understand the basic structure of the virtual memory 2 NetBSD is a public-domain implementation of a Unix operating system available for a variety of platforms. 31 subsystem of the NetBSD implementation. This consists of about 250,000 lines of C source code spread over approximately 1900 source files. Due to the complexity and huge amount of code, direct perusal of the code is impossible within the given short time limit. However, the engineer might reason about the task in terms of a high-level model that is based on the engineer's experience with the Unix virtual memory subsystem. Based on such a model, the engineer might reason that the desired change is easy to accomplish by cloning the file system module and migrating it to a module that accesses the network. The reflexion model technique provides a means of increasing the engineer's confidence in producing estimates for the change task by comparing the earlier model and the structural information extracted from the NetBSD implementation, using the four basic steps outlined earlier. A series of reflexion models may be computed, that describe and study the different levels of detail and the different aspects of the system. A series of reflexion models, computed for the NetBSD virtual memory subsystem provided valuable information about the conformance of the engineer's mental model with the actual structure of the system, thus helping in estimating the cost of changing the virtual memory system to page over a network rather than paging to a file system. The Software reflexion model may be similarly used in specifications. We used this tool with specifications that use the formal language, Z. Variations in the high level model, depending on the different ways a system may be viewed according to needs and requirements, included in the study. For example, the telereg system is considered from the administrators perspective as well as from the students perspective using high-level models. An overall study of these various views further helps in clarifying the structure of the specification. 32 3.4 U s i n g S o u r c e C o d e C o m p r e h e n s i o n T o o l s f o r R e q u i r e m e n t s Both Rigi and Software Reflexion Model tools may also be used with other kinds of specifications. However, the use of informal specs with tool may be difficult for the reason that the various relations between the components are not stated precisely and therefore, it would be difficult extract the relations. Other techniques like Data-Flow Diagrams and Structure charts[27] may be used as well with these tools. These particular techniques differ from Z as they are graphical techniques but they use inputs, outputs and various component relations represented by arrows pointing to and from the nodes of the graph, which usually represent components. If these arrows and the nodes of the graph are fed appropriately into the tool, the result would be similar to that when we use the language, Z. However, this might be challenging for the reason that Z is a precise, formal language and thus easier to handle in the required way. 3.5 E x p e r i m e n t a t i o n The work done with the tools is described in detail in the next chapter. Using two specifications, that of Telereg and the Radiation Therapy Machine, we investigate use of the Software Reflexion Model and Rigi tools to display information on the call and containment relation specifically, we specify and highlight the schemas that call another schema. 33 3 . 6 S u m m a r y Program understanding is essential in creating an efficient, working software system. Structuring the source code for the system facilitates this process. Some tools have been developed that bring out structure in software. Two of these are the Software Reflexion Model tool and Rigi. Similarly, understanding the structure of a requirements specification is very important. As we have seen, requirements structure differs from the source code structure. Our aim is to investigate how source code program comprehension can a software developer tools help comprehend and analyze requirements specification. Such an analysis, along with experiments conducted, the results obtained, and their implications of the results are described in the next chapter. 34 Chapter 4 Comprehending Software Requirements Specifications "We fall into error if we attribute to strategy a power independent of tactical results - Karl Von Clausewitz 4 . 1 I n t r o d u c t i o n Software requirements specification is an early activity in the software cycle that affects all the other development phases as well as the evolution of an artifact. Understanding the software requirements and their dependencies is of paramount importance whether we deal with the initial development or an update of a software system. In this section we investigate how certain tools used for source code comprehension can help in understanding the structure of the software requirements specification when they are specified in a formal language like Z. 35 In this work, we use two comprehension tools: a conformance tool, the Software Reflexion Model tool, as well as a reverse engineering tool, Rigi. We compare and contrast these two tools using two requirements specifications: the Telereg specification and the Radiation Therapy Machine specification. Various features of both tools are exploited in an attempt to study the structure of the requirements and identify their deficiencies. For instance, we explore how these tools can help to see how one requirement uses another and how certain requirements are grouped together or separated. The observations made by the tools are described in the following sections. 4 . 2 R i g i Initially we used Rigi to examine and understand the two specifications. With Rigi, a developer can produce a layered representation of the specification using the concept of abstraction. The tool allows the users to study the structure of the system, by grouping schemas together as they see fit. Grouping or isolation is done to visualize the structure more clearly. We investigated a parent-child relationship where the child schemas use the parent schemas; more specifically, the child schemas uses some or all of the variables or operations defined in the parent schema. The use of abstraction is intended to facilitate the grouping of schemas into components, which helps in a better understanding of the system. In the Rigi pictures shown in the following subsection, boxes represent the various components and the arcs represents relations between the components. For example, a high level view of the telereg system(shown in Figure 4.1) shows that it may be viewed as comprised of four components. Relations between these 36 components are shown but the contents of these components are hidden. Clicking on one of these boxes (shown in Figure 4.4, for example), another window pops up to show the contents of the component and the interactions between them. This structured representation helps to clarify and understand the system. 4.2.1 The Different Levels Rigi outputs of the different levels of the telereg system are shown in Figure 4.1 and 4.4-4.7. In these cases, the Telereg system is depicted in a structured manner where the different levels are shown. In the first view a high level model (Figure 4.1) is depicted. Clicking on any one of the "boxes" takes us to a lower level: for example, the contents of the box named sessions and the relations are shown in Figure 4.4. In this manner, lower and lower levels may be studied and a clear picture of the structure of the system may be obtained as in Figure 4.8. To obtain the initial boxes, the user needs to collapse related schemas manually and label them appropriately. Such grouping is usually based on some component property. The user may choose an attribute and use that to collapse components with that attribute into one unit. Once this collapsing is done, the box may be expanded by clicking on it. This process of collapse and expansion results in a simplified view of the structure of the system. In this study, we used Rigi with two requirements specifications written in Z. We were particularly interested in three relations, Delta, Xi and Include, that are common to most Z specifications. We studied these relations using features of Rigi to isolate one kind of relation from the other. We say that a schema A uses another schema B, if B appears in the predicate of A. In this case A and B are the first and second operands of the use relation. In the picture we 37 see an arrow going from A to B. We also say that schema A uses a delta(or Xi) instance of schema B if B appears in a delta (or Xi) expression in the signature of A. In this case, A is the first and B is the second operand of the delta (or Xi) relation. To show these relations, we need to define the appropriate source model for the specification. Schemas related semantically are grouped together. For example, all the schemas involved in the processing of an application are clustered together in a box called Processing. Similarly, all operations in the Telereg system pertaining to logging in were put together in a box called Logging-in. Actions involving registration and fee checks are in Preprocessing and all the definitions that are used in the specification are in Definitions. An entire operation, say if a user wants to change a section he/she is registered in, requires schemas from more than one box. For instance, the Telereg operations in Preprocessing would be used to check whether the user is a valid registered student, then the system would allow the user to log in after which the user may process his/her request by entering the box called sections, ongoing into Processing. Full details on operations require following a downward course through the various levels by choosing the appropriate box in each section. 38 Si General; - 1 Root « A C T I V E » DEFIN TIONS\ PROCESSING \ \ \ PREPROCESSING LOGG\NG_IN j / FT~ i Node "PROCESSING" (1050689) selected | Figure 4.1 : Level 1 We are mainly interested in two types of relations, the call relation and the Delta /Xi relation, between the Z schemas. A part of the source model used for Rigi is shown in Figure 4.2-4.3. There are different files for the call relation and the Delta/Xi relation. Each of the files consists of three columns. The first column describes the type of the relation. The second column gives the name of the first operand schema, whereas the third column names the second operand schema. The specification of the LSME patterns [26] to extract the source model is attached in Appendix A. 39 Call ISTTS Telereg_State Call IRS Telereg_State Call TAO Telereg_State Call MCNETelereg_State Call SEIS Telereg_State Figure 4.2: the source model for the call relation delta ATCL Telereg_State delta RFCL Telereg_State delta EO Telereg_State delta IO Telereg_State delta ATS Telereg_State Figure 4.3: the source model for the delta relation The line starts at bottom of the box that uses the schema and ends at the top of box where the schema is defined. As explained before, Figure 4.1 is a view of the system at the highest level. It shows that the Telereg system is composed of four components and that 'Definitions' is used in all the other components 'Processing', 'Preprocessing' and 'Logging-In'. 40 HI Children - 2 PROCESSING « A C T I V E » sections cftnc eert hhup cvrc Node "sect ions" (1050679) selected Figure 4.4: Level 2 Figure 4.4 shows the second level of the Telereg system. It consists of five independent components. These components contain the specifications of the various requests and are as follows: • sections: the processing of a request to add a section, drop a section, and change a section. • eert: execute exit request thread. This box consists of two schemas involved in exiting Telereg. One schema defines the request and the other outlines the response. 41 • hhup: handle hangup process. This box consists of a schema that handles the conclusion of a Telereg session, that is, hanging up the phone system. • cftnc: checks if fee for transaction must be charged • cvrc: check valid request condition. Checks if the request is valid and if an appropriate amount of fee has been paid. X] Children - 3 sections « A C T I V E » 1311 loist lact ast csst aast est Node "aast" (1048985) selected Figure 4.5: Level 3 4 2 Component "sections", which is at the third level, is comprised of six boxes: 'loist', Tact', 'ast', 'csst', 'aast' and 'est'. All of these operations involve a course in a section. Clicking on 'aast' takes us to a still deeper level(shown in Figure 4.6), while picture 4.7 shows the components of 'aast' which is at the lowest level of this specification. X| Children - 4 aast MAS rlmt AASF AASR Node " r lmt" (1048979) selected Figure 4.6: Level 4 Further, rlmt has two parts: RIRR(PvLMT_input_repeat_request) and RRF. 43 The path: processing -> sections -> aast -> rlmt takes a user through one "thread" in the specification. A thread in the specification is a series of actions which lead us from the highest level to the lowest level. § Chi ldren -5 rlmt « A C T I V E » H ArcType: level Fil tered: 0 nodes, 0 arcs Figure 4.7: Level 5 So far we have shown how the different levels of a specification can be observed separately using Rigi. Additionally, a complete picture of the structure of the entire system 44 may be obtained using a feature of Rigi's called Simple Hierarchical Multi-Perspective (SHriMP) views.3 TELEREG DEFINITIONS PRE-PROCESSING A IAS RRF rlmt RIRR AASF Level3 Level4 Level5 Figure 4.8: The entire 'structured' telereg specification 3 This information was obtained in a conversation with Margaret Anne Storey. Information about this feature of Rigi may be obtained from [24] 45 Such a view is shown in Figure 4.8. Each block is one 'view' in Rigi. Clicking on the required block gives details of that box( i.e, a lower level of the system). In our examples, only the first block in each level was shown in detail. This overall view of the system is important because it highlights the overall structure. Thus using Rigi, an engineer may obtain a high-level view of the system or may conveniently click on a part of the requirement specification and obtain the details of that particular area. To realize the importance of structuring, we tried to study the 'unstructured ' specification (Figure 4.9) and compare it to the structured specification. The unstructured view is just a collection of boxes that represent the schemas arranged randomly. As the reader can see, it is quite messy even for small specifications and it is almost impossible to understand and figure out the structure of the system. This makes the design and implementation of the system a challenging task. 46 X ] G e n e r a l - 1 R o o t « A C T I V E » CCAF AISR CCAR CRES LLAF LILA COSFC DIDS CST AVSC  Q LLSF • ACT D a* DDSR LLSF DDSF LILS DST IO \ CVRC RLMT TAG EERT • • • . • MCNE ACT WSFf> C33T 5EIS CCFAT HHUP- LOIST PRT AST LACT CERT RFS TMTE ATS TRRVC ReFrSe \ IRRVC DO CCTFC ReFrCI CCSR inOp CCSF AA.SF CIC3, AASR * ICAC C.RR CTAR PRAR CFTLF PIS IMTE CNCC " -CFCF " . PSF o-CMCFR CP.R-./C VMAEC PSR VIFC PSVC VCR PNSC VHOBR CMCFE: "Ci j!FT,C;, V;R ' CD FT s . \ < if, VOFR EIER ISHS VIIR VSIA CNAC CFBF AdToCi PdToSc • .".GIS TJ W H O B C — IRS COFC AIA3 VI31 " .RRF- =- -~DeOp - HlRR EEF Telereg_Stat. CIFBR R FCL ATCL VIT CI CA Wl St Fr Sc AASTR HHC ;;::^ |^ *:i'=':'::^:j"::'=-:'-:.! I'i'i :'='i-i;S;^ Ss: S= A r c T y p e : l e v e l F i l t e r e d : 0 n o d e s , 0 a r c s Figure 4.9: Unstructured Telereg specification Similar work was done with the radiation therapy machine specification, which is a much more elaborate specification. The results are shown in Figures 4.10 to 4.14. Figures 4.10 to 4.13 show the structure of some nodes at various levels while Figure 4.14 shows the whole specification without any structuring. 47 l i p Ijjjllf ^ ^ ^ ^ ^ U ArcType: level Filtered: 0 nodes, 0 arcs Figure 4.20: Level 1 The radiation therapy machine specification at the highest level consists of six units/boxes; that is, this specification is divided into the following six parts at the highest level: • Session • User_Interface • System_Configuration • Field 48 • Combining_the_subsystems • Software_interlocks Here again, the blocks were grouped semantically. The operations used for grouping were those used in the specifications. Using the Z language, these operations were Delta, Xi, and includes schemas. All schemas involving a particular kind of operations were grouped together. The prescriptions for the patients are all in one block called Trescription_Database'. The entire session of the machine is in 'Session_state' and all the operations performed are in a block called 'Operations'. 49 H Children - 12 Session « A C T I V E » 'rescriptio^Database / Ses3ion_state •persons Figure 4.11: Level 2 On going into "session", we find that it consists of three boxes: • Prescription_Database, • Session_state, and ArcType: level Fi l tered: 0 nodes, 0 arcs / Operations. 50 X] Children - 13 Prescription_Database « A C T I V E » Field State Login confirm F " - : ArcType: level Filtered: 0 nodes, 0 arcs Figure 4.12: Level 3 Prescription_Database may be further divided into: • Field_state, • Login, and • Confirm. 51 X] Children - 14 confirm « A C T I V E » Confirm Op Menu Op ME MSC GMA F _ ™ _ _ ArcType: level Filtered: 0 nodes, 0 arcs / Figure 4.13: Level 4 On going into "confirm", we find five further states: ConirmOp, MenuOp, ME, MSC, and GMA. 52 In contrast, a view of the unstructured specification is shown in Figure 4.14. X] General - 1 Root <<ACTTVE» : la] • [ j U •verF IF Ses3ionVar3 PP • • • • • Available' I. - Op ..Event • ' • • -k Reid 3essi(?°T ready Session IS NP ..i—I • • • • • • [ J confirm dialog Intlk IC IFS Console r~i r~i TT r~\ r ' ~ "~ SD • NoReldF ETF New Reid fNo Reid' EDF SEFF WherapvRelfil SCFF TSI swlntlk - SS Siatus'EPF • ' • • • Q - Q.ri n 0^"" AvailStAjntUnlockecGS Field SessionField\ • • G • • I DC! n SSSnot "ready)) FWI override> OD i ! r" i T . • • s • NFF SPF i . L J ECF 5TFF DoseT&JtseCallntlkEclitF Status' L J • • • • • • PTI NTF P select field EMS message PatierMaf-collirnstartutjantryjosaloqin,.; r i i— 1 • i—1 i • i ' i L J LJ . LA LJ -LJ store field auto setup AS C Select List 3PL I I l_ J I i ! I 1 i i ! Select Name N FC G USonsole SfeAiBiiDisplav S L j j | j !_J I I l_J |__,J, Editing Select - l^{i' ; \Sfl Continue Table U .wtpp.'.,.;,.. ± Newupei • • -n • • • SFL SCR Flunnin^ onfirmOp TM L l l l j 1 T L ' L J L J M ME MSG Menu Op GMASelectTtenf c c e p t M e n ilit • • x i l l G LJ • L i MO - Confirm' Menu' "Table*-.--.ST GSA • • - B - ^ G G G . E e  Operator cancel run r~T~7 i SpG-Continuue; H i L _ J A I • D • i——i. L J L I Done tupL.J . l i l y CS D Simple Op EMGNewReldMverrideF SFO • • • • • LI • LC Repro5«! aConstfteSisolel SO SEF SCFC • • ' C l co-rn G Dialog' i ' GC Dialog ESC - R DialogOp DE Accept Engaged L J [i r Ci OvemdeC ODF SSFC DDO • • [Ii • SelectReldOpEU OC - L , L T C2 j ^ j | j | j cept Confirm FC WMC ' Riter Wedge Intlk' Dose Dialog Op Therapy Sum Intlk' Wop^jentedit_do3e_reg KJ". " __ Node "edi t_dose_reg" (1048762) selected Figure 4.14 Clearly, a structured specification shows more promise to be easier to understand and implement than an unstructured one. A structured specification shows the different levels of the requirements and specifies the interactions within a level and between the levels. In the following sequence, we study some other aspects that are important for requirements specifications. First we explore how a user can isolate a specific relation 53 between the specification components and how the tools can be used to show the component layout with respect to that relation. Figure 4.15 shows the telereg specification with the delta relation only. X | G e n e r a l - 1 R o o t « A C T I V E » •«i n pmniiiiii vvw". S C F C E U " C o n 3 o l e 2 S F L -LC • F S F F S P F S l I n t l k S L N F F Field S e s s i o n D I , " • E F - S P F S E - ND"' S e s s i o n S F S E M S C o r sole -•" Fi Console S e s s i o n E M C D D O S P L List G C " Dialog - J C U f I-G L A - - Menu G S A " Table — G M A III if ArcType: level Filtered: 0 nodes, 0 arcs Figure 4.15: The Delta relation in the Telereg specification In Figure 4.15, the lines between the different components show that one component (the component where the line starts at the bottom of the box) uses the other component (the one where the line ends at the top of the box) in a Delta relation. In Z, this indicates that there is a transition between the first and a second components. 54 Similarly, in the radiation therapy machine specification, we isolated several relations. Figure 4.16 shows the "include" schema relation . Figure 4.17 shows the Xi relation indicating a transition relation between the initial and final component of a schema where the initial component is equal to the final component. Finally, Figure 4.18 shows the Delta relation. X ] G e n e r a l - 1 R o o t « A C T I V E » is • EL L J L J •verF IF Se33ionVars PP • • • • Available' I Op Event SD • • • • h Field Sessi_*°T ready Session c:: n ••• • No Held F ETF New FieldINoField' EDF SEFF Eli •[_] !~j • • cn confirm diaioa Intlk IC IFS Console ^ n r f n r T Q • s J L QJ NP _0r- - Avail^ jntUnlockecOS Field SessionHeid \ II • Li , • .DC!.- SSSnotjready))FWI override > OD NFF SPF • L WherapvFielfil • ' n • • • SCFF TSI sw intlk L ; _J L_j LI ECF 3TFF DoseTE'JBeCallntlkEditF Status' [ 1 1" I I "1 IJ LJ U L~l SS sTatus'EPF pfi' NTF P select fieldEtVlS i T l i—i !—i r - - - - - -messaged PatierkSaf eollimstartuHajitrv psaloqiri II L. i -I ._ . —I U'5"t«'PF* E New Operator cancel run 3tore field auto_isetupNASC Select List SPL SFL SCR Runnin'JonfirmOp TM \SBE--Continuue • • • • • • TJ Q r r i j [J in select NameNFC GLOonsoleS^ KiiDisplavSL"" ME MSC. Menu Op GMASelectttenAcceptMeni/ii3t L J L J L. 1 ! J _ _ L . J : LIT ' i I rr \ J LJ U ' L Editing Select DO *-SN Continue Table CO MO Confirm'Menu' Table' - ST GSA DL? • L L I J M--"C] L Done Setup A .r" Dialog 'Continue' GC _ DiaJoq ESC - R DialogQp' DE Accept Engaged LTJ • • El • L_vD LI • - U t . CS D SimpleOp EMCNewRelcfllVerrideF SFO Ci OverrideC JDF SSFC DDO CU LLl G • • U LI • "G G G G L LC Repro^ aConstffeffisolel SO .SEF SCFC SelectFJeldOpElJ OC- L C2~ n . • cept Confirm FC WMC RlterWedgelntlk' Dose Dialog Op Tnerapy Sum Intlk' N o pitientedit_dose_reg Node "edi t_dose_reg" (1048762) selected Figure 4.16: The call/include relation - Radiation Therapy Machine 55 X | G e n e r a l - 1 R o o t « A C T I V E » ASC- SPL ^ Console Session Console \ s 0 EMC SFL ^ ^  N \ \ Reid Session N re** ArcType: level Fil tered: 0 nodes, 0 arcs IV/ Figure 4.17: The Xi relation-Radiation Therapy Machine Isolating a relation helps the user determine the manner in which components use other components. Thus, for example when a change is made in a component we can determine which components will be affected and in what way. Further, it may show that certain components do not interact in certain ways and that they may be isolated. We can also note that not all schemas participate in all kinds of relations with other schemas. 56 M General - 1 R o o t « A C T I V E » s " N.GT Session CU LC GC Dialog vEMS Reid Session EMC NFF Console Sessior GSA List -\ ——.. \ \ i | I Reid \ SPL OF —li.^— SFL „EF DDO \ SQFC Console1. \ SPF H E U - ' \ Intlk \ Console2 """"---.SI / \ \ \ \ \ SPT Table SFF Menu GMA GLA SL" Console SFS ArcType: level Filtered: 0 nodes, 0 arcs Figure 4.18: The Delta relation- Radiation Therapy Machine We also investigate whether a different criteria for classification can be useful. Using the syntactic rules of Z, we grouped together all schemas that included other schemas in a certain way. Schemas involving the Delta relation were all in one group, schemas involving the Xi relation were in another and a third group consisted of schemas that use another in its predicate. The result for Telereg is shown in Figure 4.19. 57 X) General - 1 Root Telereg_State Include H Node "Include" (1048871) selected • Figure 4.19: Telereg specification viewed syntactically The boxes in Figure 4.19 represent the different types of interactions in the specification and clicking on a particular box gives details of that interaction only (as done in the manual isolation of the relations in the specification). For example, Figure 4.20 depicts only the boxes involved in the Include (or call) relation. 58 U Children - 2 Include « A C T I V E » COSFC TMTE AIAS LILA IRRVC TAO SEIS MCNE CCTFC M ArcType: level Fil tered: 0 nodes, 0 arcs CICS m CRRVC LILS CLTTFTC RIRR TRRVC PIS CNEC CNAC PNSC CMCFE IRS ISTTS EIER DIDS CICA PSVC VIFC CIFBR VMAEC ICAC IMTE VISI COFC WHOBC HHC AVSC Figure 4.20: The Include relation in the Telereg specification 4 . 3 S o f t w a r e R e f l e x i o n M o d e l As it was indicated in the previous chapter, the Software Reflexion Model tool produces a reflexion model that provides a comparison between a high level model and a source model of the system. This tool may prove useful for specifications as it checks the accuracy of the structure of the requirements specifications if the engineer has some idea of the structure. We studied the scope and flexibility of the tool and various operations 59 allowed by the tool. Different levels of detail of the specification were observed which helped us to get a clear picture, not only of the structure of the system at the highest level, but also of the inner depth of the system. Further, the different types of relations in the specification are studied in isolation and their contribution in determining the structure of the system is studied. For each study performed, we present a brief explanation and show the reflexion model produced. The reflexion models of the two example specifications, the telereg specification and the radio therapy machine specification, are shown in Figures 4.21 and 4.22. Statistics: Nodes: 4 Convergences: 3 Divergences: 1 Absences: O Figure 4.21: Reflexion Model of Telereg Specification 60 Sy ste m Configuration 0 Pre s cri pti onDatabase O O Statistics: Nodes: 7 Convergences: 2 Divergences: 9 Absences: 9 0 U serin terface • O 1 35 O Session CombineSubsystcms Figure 4.22: Reflexion Model of Radiation Therapy Machine Specification In both the cases, we chose a level that showed enough detail to understand the structure of the specification, but was not too involved or complicated. In these models, the boxes represent the components of the specification and the arrows show the relations between the components. The number on the arrows depicts the number of times one component uses another. The solid lines show the convergences (where the source model agrees with the high level model). The dashed arrows are the divergences (where arcs not predicted by the high-level model appear in the source model) and the dotted lines are the absences (where the source model does not include arcs predicted by the high level model) [25]. The reflexion model of the Telereg specification 61 shows that this specification consists of four components, 'Loggingln', 'Preprocessing', 'Processing' and 'Definitions'. Each component is involved in a group of related operations. Three of these components use the fourth and this is depicted by the arrows. Further 'Definitions' uses itself 19 times by defining a variable that is later used in another definition. In order to obtain this model, we wrote a source file, a mapping file, and a high level model file. On inputting these files into the tool, the reflexion model is obtained. Details on the language used to write these files may be obtained from [25]. Appendices B and C show the mapping and high-level model used for Telereg. Using the reflexion model, knowledge of the structure of the system is obtained. A similar reflexion model is shown for the radiation therapy machine specification. It can be seen that this specification is much more complicated and the model is even more useful in this case. Absences in the source model, that are predicted in the high level model, are shown in the Software Reflexion Model and, therefore; a user can determine what needs to be added to a source model in order to complete it. A complex and involved specification is harder to understand. The Software Reflexion Model tool can give a simplified high-level view and enable a detailed study of the relations and interactions at different levels, allowing us to study parts of the specification as well as to obtain its overall structure. 4.1.1 Observations and their Implication Having an appropriate high-level model is very important in the Reflexion Model technique. We first used the Telereg specification and changed the high-level model and the source model input file, and found some interesting results. 62 Different levels or views of the telereg specification are observed. First a very high-level model was used. The Telereg system was divided into two parts, one that is accessed directly by the students and the other contained the administrative requirements(Figure 4.23). Stati sti c s: Nodes: 2 Convergences; 1 "Divergences: I Absences: O S t u d e n t s 71 Deti niti ons Figure 4.23: Division of the Telereg Specification using only two units, the highest level As this did not give us too much useful information about the specification, we changed the model to give a more detailed view(one step lower). The Student operations was divided into more detail and the reflexion model, shown in Figure 4.24, was obtained. Statistics: Nodes : 4-Convergences: 3 Divergences: .1 Absences: O Figure 4.24: A more detailed view To get a clearer picture, a yet more detailed view was obtained. Thus, in any specification, for a more and more detailed view it is possible to refine the reflexion model till the desired detail is achieved. We divided each of the sections, 'Loggingln', 'Preprocessing', and 'Processing' to obtain more detail and we obtained a still deeper level 63 that gives the following structure These refinements help identify the structure of the system. As more and more detail is studied, the hierarchical structure of the system is observed in more depth. 64 Figure 4.25: The most detailed specification of the Telereg system. As expected there are no relations between telereg_state and global_types. 65 These different refinements give a picture of the structure of the specification and help ease the understanding of the specification. For example in the Telereg specification, on studying the three refinement levels, an idea of the structure of the specification can be formed. We can deduce that at the highest level there are two components, that of Students and that of Definitions. Students may be further divided into three kinds of processes. • processes which concern logging into the system (Loggingln) • preprocessing (Preprocessing) and • finally, processing the required function (Processing). These three components may further broken down. Loggingln consists of axiomatic_definitions. • Preprocessing consists of WSRC (Withhold student From Registration Condition) and VRR (Validate Registration Request). Processing consists of five parts: • fee(fee), • Execute Exit Request thread(EERT), • sections(sections), • Add Specialization Thread(AST), and 66 • Handle hangup condition(HHUP). Analyzing the specification using such high-level models can reveal some interesting properties . By studying the include, Delta and Xi relations we can see that each substructure ("block") depends on only one "block", telereg_state. This conclusion helps in identification of the structure of the system and will help in the later stages of software development. The Typed Reflexion Model: There is a feature in the reflexion model tool to differentiate between the various types of relations. Such a 'typed' reflexion model can help isolate a particular relation. Isolation and detection of these relations is essential in studying the structure of the system. Figure 4.26 shows the typed reflexion model for the Telereg specification. In this figure, the two arrows going from one box to another represent the 'Delta" and the "Includes" relation. In Figure 4.26, the lines on the left hand side between each pair of boxes represents the "Delta" relation, whereas the lines on the right hand side represents the "Includes" relation. Loggingln Preprocessing Processing Nodes: 4 Convergences: 6 Divergences: 2 Absences: 0 Definitions P i 11^  8 Figure 4.26: The Telereg System - Typed Reflexion Model 67 A typed Reflexion Model of the Radio Therapy machine was also studied and is shown in Figure 4.27. As the Radio Therapy Machine specification is more complicated, we can see that the typed reflexion model helps in gaining an understanding of the specification as different layers of the specification can be separated. The top layer, which is less complicated, gives a clear view of the overall structure of the system. The isolation of the different interactions and relations enables us to study each one independently and in detail, providing a clear picture of the structure of the system. This specification is very involved and complicated and isolation simplified it. 68 SystemCorifigxiraxion PrescxiptionDatabase •. 0 0 •• Statistics: Nodes: 7 Convergences: 3. Divergences: 18 'Absences: 9 Figure 4.27: Typed Reflexion Model - Radiation Therapy Machine 69 Figure 4.27 shows three different relations used in this specification. The relations may be isolated by using three different figures instead of this one. Different figures for each prove useful in a complicated specification where many relations shown together may result in confusion. Further, we thought that different criteria may be used to group together the various schemas and thus a clearer understanding of the structure of the specification may be obtained. For example the schemas may be grouped syntactically: all the schemas with the "Delta" relation may be grouped together and are represented by the box labeled Delta and all those with the "includes" relation form another cluster (the box labeled Include). The schemas which are members of these two clusters may be put in another cluster (box labeled Common). The arc is from "Delta" to "Telereg_State" shows that there are 41 schemas that have the interaction "Delta Telereg_State" , meaning they involve a change in "Telereg_State". Although this was a very good summarization of the specification based on syntactic properties and allowed us to observe the different relations and their interactions, we found that this syntactic view does not help in identifying the actual structure of this particular specification. « v . \ 1 \ 6 1 C o m m o n Figure 4.28 Statisti cs: Nodes: 4~ Convergences: 3 Divergences: '2 Absences; O 70 4 . 3 S o f t w a r e R e f l e x i o n M o d e l a n d R i g i : A c o m p a r i s o n Although the Rigi and the Reflexion model tools are fundamentally different techniques, our study showed that both can be used to highlight the structure of specifications. A high-level model is created of the specification and in this way both of these techniques can help in gaining an understanding of the system. Various relations and the interactions between the modules can be identified. Both of these techniques provide insight to the structure of the specification, though in different ways. One difference is that the Software Reflexion Model tool is a design conformance tool whereas Rigi is a reverse engineering tool. Another difference is the views supported by the techniques. The Software Reflexion Model technique shows the interactions between different modules. Different levels of the specification can be viewed by changing the source model and the high-level model (refinement). In the case of Rigi, module interactions are used to build a detailed, layered model of the specification. Different levels may be viewed by clicking on the required subsystem. The way in which views are created also differs. The Software Reflexion Model uses a combination of top-down and bottom-up processes. This helps this tool handle complexity and scale in the source model. However, Rigi uses the top down process for structuring the specification. Using Rigi, an engineer can express the desired clustering of requirement entities, either manually or automatically based on the source model. The same can be done with the Reflexion Model tool. As a final example, in the case of Rigi, even when significant clustering has been performed to derive a high-level model, this model may not necessarily comprise of a view 71 of interest to the engineer. The entire system participates in this view. A particular view may be isolated using domains in this tool [24]. However, in the case of the Software Reflexion Model, a particular relation may be selected and the entire specification may be viewed with respect to that relation only. Using these tools, the specifier can easily identify the components of a specification. For this purpose, the Software Reflexion Model tool requires the use of a source model, a high-level model and a mapping file to produce a pictorial, easy-to-understand representation of the specification. Rigi produces a pictorial representation from the source model. The software reflexion model tool needs an intuitive picture of the high level of the specification and information on how the detailed parts map to the high level. It produces a reflexion model that shows whether the high level model is a correct representation of the specification. 4 . 3 S u m m a r y Requirements specifications are different from source code as requirements may have different structure as compared to the structure of a program. For instance, the requirements components (or units) may be different from the traditional source code modules, and relations between the components may be different as well. Nevertheless, there is a similar need to structure the requirements as to structure programs as a way of comprehending their structure. The use of a formal specification technique greatly enhances that possibility. We have shown that program comprehension tools can be used with requirements specified in the formal language, Z , in a similar way to how they are used with source code. The results show that these two tools can be effective in gaining an understanding of a specification. Different levels of the system are understood by using refinement in the 72 Software Reflexion Models and by studying the different levels of abstraction in Rigi. We see that both these tools help in an identification of the structure in requirements. The process of modularity helps identify and separate the different functions performed in the specification. Modularity helps in the simpler process of understanding parts of the system separately which may then be combined to give the whole system. We found these two tools were effective in identifying the structure of requirement specifications. This structure recognition of the specification may be extremely beneficial to ease comprehension and thus reduce errors in system development. 73 Chapter 5 Structured Sspecifications "In the specification notation known as Z, schemas are used to structure mathematical descriptions" -Woodcock, J.C.P. "Structuring specifications in Z", Software Engineering Journal, January 1989. 5 . 1 I n t r o d u c t i o n We have seen that structure in specifications can help in understanding, and possibly maintaining, th this chapter, we show how Z can be extended to include a grouping (or scope) primitive. This extension provides an explicit means of specifying structure similar to packages or modules in modern programming languages. Structuring allowed us to break the system into many smaller components. We chose to collect the "semantically grouped" components and study each in isolation. These components can be further arranged in different levels. For example, components that "use/contain" schemas can be in one level and the schemas they "use" can be at a lower level. 74 Certain languages may be more conducive to structuring as compared to others. For example These formal constructs have unambiguous semantics which cannot be violated by the user. A structuring an extension for Z can help the user define a clear picture of the task each comp of a component definition. A component definition is no more than a higher level of scoping or naming space mechanism than that which exists in many programming languages like Ada and C++ . There are many ways to add component definitions to Z. We have chosen a notation similar I that appears on the first line of the definition. A typical component, with an embedded component, would thus be expressed asin Figure 5.1. variable : set variable : set •A-I I ********** *embedded_layer variable: set variable: set A Figure 5.1: A schema with embedded structure The outer component starts with the first line of *'s, which also contains the name of 75 the component. It ends with the last line and contains a number of declarations and other components. For better examples, the reader may look at the structured schemas of the two example specifications, the Telereg system and the Radiation Therapy Machine, which are attached in the appendix D and E, respectively. A specification can be divided into various modules depending on functionality or other cri together or all schemas involing a Delta relation may be grouped togther. Here we consider semantic differences only. Forcing the designer to make the requirements specification more structured may not only ease understanding of the system, thus making software development easier, but also may help in detecting errors and easing the maintenance of the requirements in the long run. Finally, the component definition can be used as a convenient scoping mechanism. We can use the same name in different components to mean different things. The above example uses two different schemas, both called A, in two different subsections. By adding a scoping operator :: , we can distinguish between these. One is referred to as Uses::A whereas the other is referred to as embedded _layer::A. 5 . 2 T h e t w o s t r u c t u r e d s p e c i f i c a t i o n s In this sections we provide some explanation about the structuring of the two example specifications used in the thesis using the new Z concept. 76 5.2.1 The Telereg specification Consider the telereg specification. Using the new construct, the specification is divided into four sections: Definitions, Loggingln, Preprocessing and Processing. Each is further divided into smaller parts. The number of layers and the position of a schema may be identified by counting the lines on the left-hand side or right-hand side. For example, consider the construct Try_Again_Request_Condition. This box is comprised of two schemas: TARC_maximum_timeouts_exceeded and TARC_register_request_valid_condition. We can easily see that it is in the third layer. This entire structured specification is shown in appendix D. 5.2.2 The Radiation Therapy Machine specification The radiation therapy machine specification is divided into six sections: Session, User-interface, System-Configuration, Field, Combining_the _subsystems, and Software_Interlocks. Again each section is further divided into smaller parts. The number of layers and the position of a schema may be identified by counting the lines on the left -hand side or right-hand side. For example consider the construct Session. This section is further divided into five sections. Each section contains one or more schemas. This entire structured specification is shown in appendix E. 5 . 2 S u m m a r y Because of the importance of structure in specifications, an attempt is made to force structure in specifications from the initial stage. For this purpose, certain features are 77 added to the specification language, Z, that allow the user to structure the specification into components or sections. The two example specifications are written including these structural features to depict how these features help in understanding the specification. 78 Chapter 6 Related Work Much work has been done on structuring in source code, but not much work has been done on structuring requirements and on tools for requirements specification. Some concepts for structuring requirements are discussed by Francalanci et al [12]. They describe three dimensions of requirements engineering, focusing on structuring requirements using views, perspectives and abstractions. They claim that usually all the artifacts produced during requirments specifications should be organised using these structured dimensions. Efforts are being made to provide methods and tools that allow the organization of requirements combining all these dimensions. Further they discuss the concept of reuse in requirements and how a structured specification supports reuse more than an unstructured specification.Various tools that allow control of relations in a specification are studied and their features are outlined. We used the different structuring approaches in our study. Using Rigi and the Software Reflexion Model, different views of 79 the two specifications are studied. Using Rigi, we are able to look at the different levels of both systems. Another approach that concentrates on the use of views in Z specifications is presented in a paper by Daniel Jackson[17]. A view may be described as a partial specification of a program, consisting of a state space and a set of operations. The full specification may be obtained by composing several views and linking them through their states and through their operations. View structuring lends clarity and terseness to the specification as it encourages multiple representations of a program's state. Jackson claims that the structure of most of the published Z specifications mostly follows the structure of an implementation [17]. Even though at this low-level the structures diverge (predicates over sets replace loops, pointers and so on), the gross organisation often retains the flavor of a program: the global variables are placed in a common area and the operations are packaged into modules. As a view is a partial specification of the entire system, it may be evaluated directly against the perceived requirements and can be constructed and analyzed independently of other views. Thus, the complexities of the dependencies may be deferred until a later stage, when the views are connected. This makes a view specification easier to construct and maintain. Features of Z, such as implicit preconditions, explicit frame conditions and uniform set representation, are conducive to this technique of view structuring [17]. In other languages, pervasive use of invariants and redundancy, that is used in Z, is not encouraged. For this reason, view structuring is rarely seen in V DM or Larch. We used detailed descriptions of the dependencies between schemas in a particular view to help structure a specification. Our views were imposed on existing specifications rather than being used in constructing a specification. Different kinds of views may be necessary depending n whether a developer is trying to construct or understand a specification. 80 Another construct that may be used with the Z notation is that of box structures[l 1]. This method proposes developing a two stage specification: a top level black-box specification followed by a state-box specification. The black-box and the state box describe identical external behavior. The difference is that the black-box behavior is described using stimulus histories, whereas the state box behavior is described by referencing the internal system state. Before we split the two specifications wee studied into detailed views, we roughly estimated the boundaries of the black box and the state box. This helped in the detailed analysis of the specification. 81 Chapter 7 Conclusion "Unlike a mechanical engineer who can often take a device apart and see how the parts fit together, a software engineer is faced to comprehend systems that are pure thought-stuff and infinitely malleable." Brooks, F. No silver bullet-essence and accidents of software engineering in Information Processing 86. Elsevier Science Publishers, Amsterdam, Netherlands, p. 1070. Specifications have little explicit structure. This lack of structure can make it difficult to understand and evolve the specification. For example, in particular it can be difficult for a software engineer to understand the affected parts of a specification when a change is made to a specific group of requirements. The same problems appeared in programs long ago and forced the language designers to provide explicit structuring mechanisms. For instance package/module concepts were introduced in Modula3 and Ada to manage complexity and limit the effects of change. The introduction of structure in programs greatly helped to reduce errors and avoid redundancies. As requirement specifications are even more basic than programs and as they are the first and probably most crucial part of the software life cycle, the introduction of structure at this level may prove even more beneficial. This study investigated the use of the existing structure determination techniques written for source code to the problem of 82 deterrnining structure in requirement specifications. More specifically we studied how Software Reflexion Models and Rigi can be used with requirements specified using the Z specification language. We conducted various experiments on these tools to study their functionality in some special cases. Their features were examined and studied in the context of requirements specification. The concepts of modularity, abstraction and refinement allow a programmer to break down a large, complex program into smaller and more manageable parts. We found that these concepts also helped to clarify understanding of requirements specifications. We used particular specifications that are written in a formal language, Z. Being mathematical and precise in nature, such specifications can be easily structured in layers or hierarchies and thus can lead to an understanding of the system. To demonstrate this point, the two specifications used were structured in a variety of ways and the benefits of such structuring were discussed. We saw that Rigi and Software Reflexion Models were helpful in detecting structure in the specifications and understanding the specification. Using the Software Reflexion Model and Rigi, we divided each of the two example specifications into a number of basic components and studied the interactions between them. The Software Reflexion Models compared the high level model with one we envisioned and specified the number of convergences, divergences and absences with our model. In the case of Software Reflexion Model among other things, the typed reflexion model and refinement proved very useful. We found that the collapse-expand feature of Rigi helped in abstraction and Shrimp Views proved very useful in obtaining a comprehensive picture of the entire specification. The use of both these tools provided us with an accurate description of the specification. We also discussed a high-level structuring mechanism for Z that allows designers to 83 structure their specifications from the start, when specifying the requirements, rather than reconstructing structure after the requirements are complete. 7 . 1 F u t u r e W o r k The structure determination techniques used may be explored further and more functionality may be added to them. Presently, work is being done on Rigi to provide an interface that may give a view of the entire program structure (Shrimp Views) as well as the substructure which would allow the parent and children nodes may be viewed together. In the Software Reflexion Model, some work might be done in the context of requirement specifications. There may be provision to extend this technique to the other different kinds of specification, some of which involve diagrammatic techniques. Other extensions to this technique may include techniques to reduce the size of the mapping file and such extension have been described by Gail Murphy[25] in the context of programming languages. 84 Bibliography [1] Arnold, R. Tutorial on Software Engineering. In Proceedings of the 1990 Conference on Software Maintenance. San Deigo, California, November 1990, pp. 26-29. [2] Boehm, B., Verifying and Validating Software Requirements and Design Specifications, Computer, 1, January 1984, pp.75-88. [3] Boehm, B.W. Software Engineering Economics. Englewood Cliffs, NJ: Prentice-Hall, Inc. 1981. [4] Boehm, B.W., Maclean, R.L., and Urfig, D.B., Some experiences with automated aids to the design of large-scale reliable software. IEEE Trans, on Software Eng Vol. SE-1, no.2, Feb. 1975. [5] Booch, G., and Rumbaugh, J., Unified Method for Object-Oriented Development, Rational Software Corporation, 1995. [6] Brooks, No silver bullet: Essence and accidents of Software Engineering, Computer, Vol.20, no.4, Apr. 1987, pp. 10-19. 85 [7] Cheng, M. I., Informal, Semi-Formal and Formal Approaches to the Specification of Software Requirements, University of British Columbia, Technical Report 94-23, MSc thesis, September 1994. [8] DeMarco, T. Structured Analysis and System Specification. Yourdon Press, Prentice Hall Inc., NJ. 1979. [9] Deutch, M.S., and Willis, R.R. Software Quality Engineering - A Total Technical and Management Approach. Prentice Hall Series in Software Engineering, Englewood Cliffs, New Jersey, 1988. [10] Endres, A., An analysis of errors and their causes in system programs, IEEE Trans. Software Eng., Vol. SE-1, no.6, pp. 140-149, June 1975. [11] Fetzer, D., and Poore, J., Using Box Structures with the Z Notation, IEEE Software, Jan., 1992, pp. 394-405. [12] Francalanci, C, Fugini, M.G., Pernici, B. Structuring requirements: existing approaches and automatic support. IEEE Software April, 1994. pp. 824-829. [13] Hall, A., Seven myths of formal methods, IEEE Software, Vol7, no.5, p.11-19, September 1990. [14]Ince, D.C., An Introduction to Discrete Mathematics, Formal System Specification and Z. Oxford University Press, Inc. New York, 1992. [15] Jacky, J., Patrick, M., Unger, J., Formal Specification of Control Software for a Radiation Therapy Machine, TR 95-12-01, University of Washington, January 1995. [16] Jacobson, I., Object-Oriented Software Engineering - A Use-Case Driven Approach. Addison-Wesley, 1992. 86 [17] Jackson, D., Structuring Z Specifications with Views. ACM Transactions on Software Engineering and Methodology, Vol.4, no.4, Oct. 1995, pp. 365 - 389. [18] Katie, N., Nevstrujev B., Vogel, D., Pendergast, M.O., Bridging the Gap between Structured requirements and Object-Oriented Analysis and Design. Proceedings of the 29th Annual Hawaii International Conference on System Sciences, 1996. [19] Lehman, M. and Belady, L., Laws of program evolution - rules and tools for programming management. In Infotech state of the Art Conference, Pergamon Press. Reprinted in M.M. Lehman, L.A. Belady editors, Program evolution: Processes of software change, Ch. 12, APIC Studies in Data Processing No. 27. Academic Press, London, 1985. [20] Leveson, N.G., Software safety: What, why and how, ACM Comput. Surveys, vol. 18, no.2, pp.125-164, June 1986. [21] Luqi, GoguenJ.A.Formal Mefhods:Promises and Problems, IEEE Software, pp.74 - 85 , January 1997. [22]Meyer, B., On Formalism in Specifications, University of California, Santa Barbara, IEEE Software, January 1985. [23] Mills, H.D.,: Structured Programming Retrospect and Prospect "JEEE Software. 1986 pp. 58 - 66. [24] Muller, H. and Klashinsky, K. A system for programming-in-the-large. In proceedings of 10th Int'l Conf. on Software Engineering, 1989, p. 80-86. [25] Murphy, G.C., Lightweight Structural Summarization as an aid to software evolution. Ph.D. thesis, University of Washington, 1996] 87 [26] Murphy, G., Notkin, D. and Sullivan, K. Software Reflexion Models: Bridging the gap between Source and High-Level Models, SIGSOFT'95, ACM 1995. [27] Mynatt, B. T., Software Engineering With Student Project Guidance, Prentice Hall, Englewood Cliffs, New Jersey. [28] Potter, B., Sinclair, J., and Till, D., Introduction to Formal Specification and Z. Prentice Hall International Series in Computer Science, University Press, Cambridge, UK, 1991. [29] Rumbaugh, J., Baha M., Premerlani, W., Eddy, F., and Lorensen W. Object-Oriented Modeling and Design. Prentice Hall, Englewood Cliffs, New Jersey, 1991. [30] SommervilleJ., Software Engineering. Addison-Wesley Publishing Company, 1992. [31]Spivey, J.M., An Introduction to Z and formal specifications, Software Engineering Journal, Jan. 1989, vol4, no.l,pp.40-50. [32] Storey, M. D., Muller, H.A., Wong, K. Manipulating and Documenting Software Structure. Paper obtained in an email communication with Hausi Muller. [33] Wasserman A.I., Toward a Discipline of Software Engineering, IEEE Software , Nov. 1996, pp. 23-31. [34] Wong, K., Tilley, S.R., Muller, H.A., and Storey, M.D., Structural Redocumentation: A Case Study, University of Victoria, IEEE Software, vol.12, no.l,pp. 46-54, January 1995. [35] Information obtained from the web site: http://tara.csc.uvic.ca/rigi/rigi.html. 88 APPENDIX A (Source patterns extracing information from the Telereg s p e c i f i c a t i o n ) schema % { - }+ <schemaname> { - }+ % schema.delta % [ \| ]Delta <deltavar> @ f write("&1&",schemaname,"&2&"," &1&" ,deltavar,"&2&") @ % schema.xi % [ \| ]Xi <xivar> @ write ( " , schemaname, "&2&", " &1&" , xivar, "&2&") @ % schema.include % \ | <ne.wvar> \ | @ write ("&1&",schemaname,"&2& &1&",newvar,"&2&") @ % APPENDIX B ( The mapping f i l e f o r the Software Reflexion Model foe the Telereg schema=Telereg_State mapTo=Definitions ] schema=InSTTSchedule mapTo=Definitions ] schema=InRegularSchedule mapTo=Definitions ] schema=AddToClassList mapTo=Definitions ] schema=RemoveFromClassList mapTo=Definitions ] schema=DecrementOpenings mapTo=Definitions ] schema=IncrementOpenings mapTo=Definitions ] •schema=AddToSchedule mapTo=Definitions ] schema=RemoveFromSchedule mapTo=Definitions ] schema=ThereAreOperiings mapTo=Definitions ] schema=MaxCreditsNotExceeded mapTo=Definitions '] schema=StudentEnrolledInSection mapTo=Definitions ] schema=WithdrawStudentFromSection mapTo=Definitions ] schema=RegisterStudentInSection mapTo=Definitions ] schema=Wsrc_Holds_Or_Blocks_Condition mapTo=LoggingIn ] schema=Cofac_Outstanding_Fee_Condition mapTo=LoggingIn ] schema=Vit_* mapTo=Loggingin] schema=Ccfat_* mapTo=LoggingIn ] schema=Cadc_* mapTo=PreProcessing ] schema=Cerc_* mapTo=PreProcessing ] schema=Prt_* mapTo=PreProcessing ] schema=Cert_* mapTo=PreProcessing ] schema=Irrc_* mapTo=PreProcessing ] schema=Tarc_* mapTo=PreProcessing j schema=Cftnc_* mapTo=Processing ] schema=Cvrc_* mapTo=Processing ] schema=Eert_* mapTo=Processing ] schema=Rlmt_* mapTo=Processing ] schema=Act_* mapTo=Processing ] schema=Csst_* mapTo=Processing ] schema=Cst_^ mapTo=Processing ] schema=Dst_* mapTo=Processing ] schema=Loist_* mapTo=Processing ] schema=Lact_* mapTo=Processing ] schema-Ast_* mapTo=Processing ] schema=Hhup_* mapTo=Processing ] 9o APPENDIX C ( The high l e v e l model for the Software Reflexion Model for the t e l e r e g speci Loggingln D e f i n i t i o n s Preprocessing D e f i n i t i o n s Processing D e f i n i t i o n s 9t APPENDIX D TELEREG - STRUCTURED SPECIFICATION D e f i r . i t — r . 3 " • * . - . » r . 'Giobal_Types* * »»***-"-""''«****»*«**».*.« [Sid] [Section] [Course] j [Session] j [3alance] .. [Da-e] [ S p e c i a l i z a t i o n ] RegistrationType ::= STT_Schedule | Regular Schedule == P Section Openings == Z C i a s s l i s t == P S i d C r e d i t s == Z "Counter = Z ?ree_Transactions == Z LockModes ::= LOCKED | UNLOCKED Register_Requests ::= ADD | DROP | LOOKUP. | | CHANGE I j EXIT j I CONFIRM | LIST j CANCEL | ADDSPEC i " i 3rimuli_Or_Responses ::= • j add_section_msg | add_section_req<<Section>> | add_spec_msg<<Specialization>> I add_spec_req<<Speciaiization>> j ask_spec_msg | j bye_msg | cancel_msg| c-an"cel_re j.ection. | cancel_reg-| cannot_add_msg ! cannot_change_msg | i cannot_confirm_msg | cannot_drop_msg \ cannot_register_msg j change_msg | char.ge_req<<Section>> j •j confirm_msg | I conf irrr._req<<Section>> | drop_msg | drop_req<<Section>> \ exit_msg<<Balance>> j exit_req<<Session>> I fee_charged_msg j fee_kickout_msg | fee_msg<<3alar.ce x Session>> i : :ee_raquest«Sessior.» \ | -. f r e e _ t r a n s a c t i c r . s _ l e f t_rr.sg<<Cour.ter>> | j hangup j j r.oid_or_block_—.sg | | i n v a i l i d _ i d _ m s g | ; ir.vaiid_reque3t_-isg<<Register_?.equests>> j j ir.valid_spec_ T.sg ] i las-_r.arae_-.sg j l i s t _sc<<Ccurse>> ; „ InSTTScheduie | Telereg_State j i d : S i d Schedule Type i d = STT_Schedule InRegularSchedule Telereg_State i d : SId Schedule Type i d = Regular AddToClassList Delta Telereg_State i d : SId s e c t i o n : Section ' newClasslist : C l a s s l i s t n e wClasslist = Class setunion {id} Class' =Class +. {Section j-> newclasslist} RemoveFromClassList Delta Telereg_State i d : SId s e c t i o n : Section n e w c l a s s l i s t : C l a s s l i s t n e w c l a s s l i s t = Class s e c t i o n \ {id} Class' = Class + { s e c t i o n |-> n e w c l a s s l i s t } DecrementOpenings Delta Telereg_State s e c t i o n : Section newopenings : Openings newopening = A v a i l a b i l i t y s e c t i o n - 1 A v a i l a b i l i t y ' ' = A v a i l a b i l i t y + { section |-> newopenings } IncrementOpenings Delta Telereg_State s e c t i o n : Section newopenings : Openings newopening = A v a i l a b i l i t y s e c t i o n + 1 A v a i l a b i l i t y ' = A v a i l a b i l i t y -i- . { section |-> newopenings } --AddToSchedule Delta Telereg_State i d : SId s e c t i o n : Section newschedule : Schedule newschedule = Registeredln i d setunion {section} Registeredln' = Registeredln + {id i-> newschedule } 93 l i s t _ r e q | lookup_msg<<Openings>> | lookup_req<<Section>> | maximum_charge_fee_msg | request_id_msg | repeat_req | say_spec_msg<<Specialization>> | session«Session» | session_msg<<Session>> | student_id<<SId>> | try_again_msg System_State ::= W a i t i n g _ f o r _ i d e n t i f i c a t i o n _ i n p u t | Waiting_for_session_input | Waiting_for_spec_input | Waiting_for_next_request_input | IDLE >= _ : Balance <-> Balance _ < _ : Date <-> Date ! ******'"elexeg State -************************************ Students : P SId Registeredln : SId -> Schedule A v a i l a b i l i t y : Section -> Openings Class : Section -> C l a s s l i s t ScheduleType : SId -> RegistrationType Blocks : P SId Holds : ? SId Outstandings : P SId Valid S e s s i o n : P Session E l i g i b l e s : SId -> Session Accessed : SId -> -Date Account' : SId -> Balance LockStatus : SId -> LockModes ChargeFeeStatus : SId ->'• Balance state : System:State count : Free:Transactions StudentSpec : SId -> S p e c i a l i z a t i o n ValidSpec : P S p e c i a l i z a t i o n MAX:TIMEOUT:COUNT : Z MAX:ID:COUNT : Z max:credits : Z j MAX:CHARGE:FEE : Balance Commands : ? Register:Requests CostlyCommands : P Register:Requests NumberCredits : Section -> Z I T o t a l C r e d i t s : SId -> Z I CourseSchedule : Section -> Course ;dom Registeredln) subseteq Students Blocks subseteq Students Holds subseteq Students Outstandings subseteq dom Account Outstandings subseteq Students ^  CostlyCommands subseteq Commands • Axiomatic_Def i n i t i o n s * * *• RemoveFromSchedule • Delta Telereg_State i d : S i d sec t i o n : Section newschedule : Schedule newschedule = Registeredln i d \ {section} Registeredln' = Registeredln + {id |-> newschedule } ThereAreOpenings Telereg_State section : Section A v a i l a b i l i t y section > 0 MaxCreditsNotExceeded Telereg_State i d : S i d sec t i o n : Section T o t a l C r e d i t s i d + NumberCredits section <= max_credits StudentEnrolledlnSection Telereg_State i d : S i d sec t i o n : Section s e c t i o n i n (Registeredln id) ' WithdrawStudentFromSection Delta Telereg_State i d : S i d s e c t i o n ': Section newschedule : Schedule n e w c l a s s l i s t : C i a s s l i s t newOpenings : Openings RemoveFromSchedule RemoveFromClassList IncremehtOpenings RegisterStudentlnSection Delta Telereg_State i d : S i d s e c t i o n : Section newschedule : Schedule n e w c l a s s l i s t : C i a s s l i s t newOpenings : Openings AddToSchedule AddToClassList DecrementOpenings * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * *Logging In**************•********************************* WSRC_Holds_or_blocks_condition [Teiereg_State I std:e' = Waitir.g_for_sessior._ir.put] j VIT_P.equiremer.tl =A = V I T _ i n p u t _ s t u d e n t _ i d e n t i f i c a t i o n and V I T _ i n _ i d e n t i f i c a t i o n _ i n p u t _ s t a t e and not VIT_id_found_condition and VIT_max_attempt_exceeded_condi ti o n ' implies VTT_connection_rejectior. and j VIT_move_to_idle state I VIT_Requirement2 = ~ = V I T _ i n p u t _ s t u d e n t _ i d e n t i f i c a t i o n and V I T _ i n _ i d e n t i f i c a t i o n _ i n p u t _ s t a t e and not VIT_id_found_condition and " not VIT_max_attempt_exceedec_condition implies V I T _ i n v a l i d _ i d e n t i f i c a t i o n _ r e j e c t i o n and V I T _ i d e n t i f i c a t i o n _ r e q u e s t VIT_Requirement3 =~= V I T _ i n p u t _ s t u d e n t _ i d e n t i f i c a t i o n and V T T _ i n _ i d e n t i f i c a t i o n _ i n p u t _ s t a t e and VIT_id_found_condition and VIT_withold_condition implies VIT_hold_or_block_re jection and VIT_move_tc_idle_state VTT_Req_ire~:_nt4 = ~ = V I T _ i n p u t _ s t u d e n t _ i d e n t i f i c a t i o n and V I T _ i n _ i d e n t i f i c a t i o n _ i n p u t _ s t a t e and VIT_id_found_condition and VIT_outstanding_fee_condition implies VIT_outstanding_fee_rej ection VIT_Requirement5 =A= V I T _ i n p u t _ s t u d e n t _ i d e n t i f i c a t i o n and V I T _ i n _ i d e n t i f i c a t i o n _ i n p u t _ s t a t e and VIT_id_found_condition and not VIT_withhold_condition implies VIT_student_identification_acceptance and VIT_move_to_session_input_state Vali'date_Identif ication_Thread =" = VTT_Requirementl and VIT_Requirement2 and VIT_Requirement3 and . VIT_Requirement4 and VIT_Requirement5 *********************************************** * *Compute_Current_Fee_Assesment_Thread* ******* -CCFAT_input_fee_balance_request Telereg_State ss : Session input? : Stimuli_Or_Responses input? = fee_request(ss) -CCFAT_fee_balance_feedback Delta Telereg_State i d : SId i ss : Session . j output! :Stimuli_Or_Responses output! = fee_msg ((Account id;,ss) 16 Telereg:State i d : Sid i d i n Holds or i d in 3iocks * * * * * * * p e e * * i * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * COFAC_outstanding_f ee_conditior. Telereg_State ! i d : Sid j i d i n Outstandings * * * * *Validate_Identi fication_Thread** ********** --VIT_input_s_udent_identi£ication Telereg_State i d : S i d input? : Stiitiiuli_Or_Responses output! = last_name_msg - V I T _ i n v a l i d _ i d e n t i f i c a t i o n _ r e j e c t i o n -Delta Telereg_State output!:Stimuli_Or_Responses output! = invalid_id_message -VIT_cpnnection_re j e c t ion Delta Telereg_State output! :Stimuli_Or_Responses output! = bye_msg -VIT_hold_or_block_rej ection Delta Telereg_State output! :Stimuli_Or_Responses output! = hold_or_block_msg i d i n Students -VIT_max_attempt_exceeded_condition--j Telereg_State id_count : Z id_count >= MAX_ID_COUNT VIT_withhold_condition ="= WSRC_holds_or_blocks_condition VIT_outstanding_fee_condition = ~ = COFAC_outstanding_fee_condition V I T _ i n _ i d e n t i f i c a t i o n _ i n p u t _ s t a t e = " = [Telereg_State | state = W a i t i n g _ f o r _ i d e n t i f i c t i o n _ i n p u t ] VIT_rnove_to_idle_state =A = [Delta Telereg_State | state' = IDLE] 97 CCF AT_ir._sess icr_.input_s;:ate = [Telereg_State I. state = Waiting_f or_ses3ior._input ] CCFAT_in_next_request_input_state = " = [Telereg_State | state = • Waiting_for_next_request_input] ! ! Compute_Current_Fee_Assessment_Thread j \ CCFAT_input_fee_balance_request and CCFAT_in_next_request_input_state or CCFAT_in_session_input_state implies CCFAT_fee_balance_feedback •**************^ +^ ******i ***•*************•***••••*•*••••* . * * * * ^ * * * * * * * * * * * * * * * * * + * ^ ^ ^ * ^ * * » * ^ ^ * ' r * * * * * i ***** * preprocessing* ***•*•**< •• • • • R e g i s t r a t i o n * * * 1 : * * • • * * * * * ! r * * * * * * * * * * i * * * * *check_Access_Dates_Condition -CADC_no_access_condition Telereg_State ss : Session currentDate : Date i d : S i d | currentDate < Accessed i d : * * * * * * * * * * * * * * * * * • * * • • * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * C h e c k _ E l i g i b i l i t y _ T o _ R e g i s t e r _ C o n d i t i o n * * ***** - C E R C _ n o _ e l i g i b i l i t y _ c o n d i t i o n Telereg_State ss : Session i d : S i d {id I-> ss} subseteq E l i g i b l e s • • * * * * * * * * * * * * • • • • * • • • ! r * * * * * * * * * * * * * * * * ^ * * * * + * ^ i * * * * *Preprocess_Registration_Thread*************** -PRT_input_session Telereg_State ss : Session input? : Stimuli_Or_Responses input? = session(ss) -PRT session feedback-D e l t a Telereg_State ss : Session output! : Stimuli_Or_Responses output! = session_msg(ss) -PRT_register_attempt_rejection Delta Telereg_State output! : Stimuli_Or_Responses output! = cannot_register_msg <f8 Delta Teiereg_State output! : Stimuli_Or_Responses output! = ask_spec_msg (StudentSpec id) -PRT_session_valid_condition Telereg_State ss : Session ss i n ValidSession -PRT_need_specialization ..condition Telereg_State i d : SId not ( f o r a l l spec : S p e c i a l i z a t i o n @ {id |-> spec} subseteq StudentSpec) PRT_move_to_spec_input_state =~= [Delta Telereg_State | s t a t e ' = Waiting_for_spec_input] PRT_move_to_idle_state = ~ = [Delta Telereg_State | stat e ' = IDLE] PRT_move_to_next_request_state = ~ = [Delta Telereg_State | stat e ' = Wa'iting_f or_next_request_input ] PRT_Requirementl =*= PRT_input_session and PRT_in_session_input_state and PRT_session_valid_condition and PRT_no_access_condition•or P R T _ n o _ e l i g i b i l i ty_c ondi t i on implies . PRT_register_attempt_rejection and PRT_move_to_idle_state PRT_Requirement2 ="= PRT_input_session and PRT_in_session_input_state and PRT_session_valid_condition and not PRT_no_access_condition and not P R T _ n o _ e l i g i b i l i t y _ c o n d i t i o n and not PRT_need_specialization_condition implies PRT_session_feedback and PRT_specialization_feedback and PRT_move_to_next_request_input_state PRT_Requirement3 ="= PRT_input_session and PRT_in_session_input_state and PRT_session_valid_condition and not PRT_no_access_condition and not P R T _ n o _ e l i g i b i l i t y _ c o n d i t i o n and PRT_move_to_spec_input_state Preprocess_Registration_Thread = " = PRT_Requirementl and PRT_Requirement2 and PRT_Requirement3 C a n c e l _ E n t i r e _ R e g i 3 t r a t i o n _ T h r e a d * * * -CERT_input_cancei_all Teiereg_State input? : 'Stimuli_Or_Responses input? = cancel_req -CERT_cancel_all_feedback Delta Telereg_State output! : Stimuli_Or_Responses output! = cancel_msg -C E R T _ c a n c e l _ a l l _ r e j e c t i o n Delta Telereg_State output! : Stimuli_Or_Responses output! - = c a n c e l _ r e j e c t i o n CERT_in_next_request_input_state ="= [Telereg_State | state = Waiting_for_next_request_input] CERT_valid_request_capability =A= Check_Validity_Of_Requests_Capability CERT_outstanding_fee_condition =A= COFAC_outstanding_fee_condition -CERT_remove_each_section Delta. Telereg_State i d : SId ne w c l a s s l i s t : C l a s s l i s t newopenings : Openings newschedule : Schedule f o r a l l s e c t i o n : Section @ StudentEnrolledlnSectipn and WithdrawS'tudentFromSection CERT_Requirementl =A= CERT_input_cancel_all and CERT_valid_request_capability and CERT_in_next_request_input_state and not CERT_outstanding_fee_condition and not InSTTSchedule implies CERT_remove_each_section and' CERT_cancel_all_feedback CERT_Requirement2 = " = CERT_input_cancel_all and not CERT_valid_request_capability or not CERT_in_next_request_input_state or CERT_outstanding_fee_condition or InSTTSchedule implies C E R T _ c a n c e l _ a l l _ r e j e c t i o n Cancel_Entire_Registration_Thread = ~ = CERT_Requirementl and CERT_Requirement2 it**************************************-** Telereg-_State Request_counc request_count > MAX_TIMEOUT_COUNT - IR?.C_reg i s ter_reques t_val id_condi t i on -Telereg_State request : Register_Requests request i n Commands -IRRC_concurrent_access_condition-Telereg_State i d : S i d LockStatus i d = LOCKED IRRC_request_rejection_condition = ~ = IRRC_concurrerit_access_condition or not IRRC_register_request_valid_condition and IRRC_ maximum_timeouts_exceeded * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * i r*********** * * * * ** *Try_Again_Request_Condition* **************** -TARC maximum timeouts_exceeded Telereg_State request_count : Z request_count > MAX TIMEOUT COUNT -TARC_register_request_valid_condition-Telereg_State request : Register_Requests request i n Commands TARC_try_again_condition = ~ = TARC_register_request_valid_condition and not TARC_maximum_timeouts_exceeded ************************************************** ********************************************************** * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * l * * * * * * * f ** + ****p2-Q^g2s ing* ************************************ + ****** + ***irir*ir'*^ Charge_fee_For_Transaction_If_Necessary_Condition* * * * CFTNC_charge_transaction_fee_condition Telereg_State request : Register_Requests output! : Stimuli_Or_Responses output! * try_again_msg r*****************i • * * * * * * * * * * * ! [ • * * * * * ! * * * * * * * Check_Validity_Of_Requests_Capability"' CVRC_free_transaetions_left_feedback-Delca Telereg_Sca.e transact_cour.: :' Counter output! : Stimuli_Or_Responses output! = free_transactions_left_msg j (transact_count) j j -CVRC_fee_charge_feedback j Delta Telereg_State output! : Stimuli_Or_Responses • output! = fee_charged_msg -CVRC_maximum-charge_fee_rejection Delta Telereg_State output! : Stimuli_Or_Responses output! = maximum_charge_fee_msg -CVRC_reg i s ter_reque s t_va1i d_c ondi t i on Telereg_State request : Register_Requests request i n Commands CVRC_charge_transaction_fee_condition = CFTNC_charge_trans ac t i on_ f ee_c ondi t i on CVRC_reque s t _ r e j ec t i on_condi t i o n = * = IRRC_reques t_ r e j ec t ion_condi t i on CVRC_try_again_conditiion = " = TARC_try_again_conditiion CVRC_less_than_ten_free_transactions_condition Telereg_State count <= 10 -CVRC_maximum_charge_fee_exceeded Telereg_State i d : SId ChargeFeeStatus i d >= MAX_CHARGE_FEE CVRC_move_to_idle_state = * = [Delta Telereg_State | state' = IDLE ] -CVRC_decrement_fee_transactions Delta Telereg_State count' = count - 1 CVRC_Requirementl = " = CVRC_request_rejection_condition implies CVRC_invalid_request_rejection and CVRC_move_to_idle_state CVRC_Requirement2 = *= • CVRC_try_again_condition implies CVF.C_trv_agair:_rea_est a n d -C V P . C _ I e 3 3 _ t r . a n _ ~ e n _ f r e e _ C r a n s a c t i Q r . 3 _ c o r . d i n o r . impl ies CY?.C_free_transaccions_left_f eedback CVRC_?.equireraent4 =n = C7RC_register_request_valid_condition CVP.C_maximum_charge_fee_exceeded implies CV?.C_maximum_charge_fee_rejection a n d CV?.C_ m o v e_to_ i d l e_state CVRC_F.equirerr.ent5 = ~ = CVRC_register_request_valid_condition and not CVRC_maximum_charge_fee_exceeded and CVRC_charge_transaction_fee_condition implies CVRC_fee_charge_feedback and CVRC_decrement_free_transactions C h e c k _ v a l i d i t y _ o f _ r e q u e s t s _ c a p a b i l i t y =~= CVRC_Requirementl and CVRC_Requirement2 and CVRC_Requirement3 and CVRC_Requirement4 and CVRC_Requirement5 * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * *_xecute_Exit_Request_Thread*********** -EERT_input_exit_request * * * * * * * * * * * * * * * Telereg_State ss : Session input? : Stimuli_Or_Responses input? = exi t _ r e q ( s s ) -EERT_exit_feedback-Delta Telereg_State i d : S i d ss : Session o u t D u t ! : Stimuli_Or_Responses ou tput! = exit_msg(Account id) EERT_in_next_request_input_state =~= [Telereg_State |. state = . -. Waiting_f or'_next_request_input] EERT_valid_request_capability = " = Check_Va1i d i ty_0 f_Reque s t s_Capabi11ty EERT_move_to_idle_state =A= [ Delta Telereg_State state' IDLE Execute_Exit_Request_Thread = " = EERT_input_exit_request and EERT_valid_request_capability and EERT_in_next_request_input_state implies EERT_exit_feedback and EERT_move_to_idie_state * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * :**«*Sections*******' ' * * *Repeat_Last_Message_Thread* * * * * * * * * * * * * * * * * * * -RLMT_input_repeat_request Telereg_State input? : Stimuli_Or_Responses input? = repeat_req ACT_?.equi r-=~en 1 1 and ACT_Requirement2 I **Confirm_A_Section_Switch_Thread* *•**•'**•*•** i -CSST_input_confirm_switch i I i i i '• Teiereg_3tate j sec t i o n : Section ! input? : StimuIi_Or_Responses ! input? = confirm_req(section) -CSST_confirm_switch_feedback Delta Telereg_State output! : Stimuli_Or_Responses output! = confiriri_msg -CSST_confirm_switch_rejection Delta Telereg_State output! : Stimuli_Or_Responses output! = cannot_confirm_msg CSST_in_next_requesu_input_state = ~ = [Telereg_State | state = Waiting_for_next_request_input] CSST_valid_request_capability =~= Check_Validity_Of_Requests_Capability CSST_outstanding_fee_condition = * = COFAC_outstanding_fee_condition CSST_Requirementl = ~ = CSST_input_confirm_switch and CSST_valid_request_capability and CSST_in_next_request_input_state and not CSST_outstanding_fee_condition and not InSTTschedule and StudenfcEnrolledlnSection implies CSST_confirm_switch_feedback CSST_Requirement2 = A = CSST_input_confirm_switch and not CSST_valid_request_capability or not CSST_in_next_request_input_state or CSST_outstanding_fee_condition or InSTTschedule•or not StudentEnrolledlnSection implies CSST_confirm_switch_rej ection Confirm_A_Section_Switch_Thread =~ = CSST_Requirementl and CSST_Requirement2 ********************************************** *Change_Section_Thread* ************************ -CST_input_change_section Telereg_State s e c t i o n : Section input? : Stimuli_Or_Responses input? = change_req(section) -RLMT_repeat_£ eedback ! Delta Telereg_State I lastmsg : Stimuli_Or_Responses | output! : Stimuli_Or_Responses output! = repeat_msg(lastmsg) Repeat_Last_Message_Thread = ~ = RLMT_input_repeat_request implies RLMT_repeat_feedback *Add_A_Section_Thread* -ACT_input_add_section Telereg_State s e c t i o n : Section input? : Stimuli_Or_Responses input? =add_section_req(section) - ACT_add_sec t ion_f eedback • Delta Telereg_State output! : Stimuli_Or_Responses output! = add_section_msg -ACT_add_section_rej e c t i o n Delta Telereg_State output! : Stimuli_Or_Responses output! = cannot_add_msg ACT_in_next_request_input_state = [Telereg_Stat'e | state = Waiting_for_next_request_input] ACT_va.lid_request_capability = ~ = Check_Validity_Of_Requests_Capability ACT_outs tanding_f ee_condi t i on = ~ = COFAC_outstanding_fee_condition ACT_Requirementl ="= ACT_input_add_section and ACT_in_next_request_input_state and ACT_valid_request_capability and not ACT_outstanding_fee_condition and not InSTTSchedule and ThereAreOpenings and MaxCreditsNotExceeded and not StudentEnrolledlnSection implies RegisterStudentlnSection and ACT_add_section_feedback ACT_Requirement2 ="= ACT_input_add_section and not ACT_in_next_request_input_state or not ACT_valid_request_capability or ACT_outstanding_fee_condition or InSTTSchedule or not ThereAreOpenings or not MaxCreditsNotExceeded or StudentEnrolledlnSection implies ACT_add_section_rejection tor -CST_change_3ect ior_feedback Delta Tele'reg_3tate output! : Stimuli_Or_Responses output! = change_msg -CST_change_section_rej e c t i o n Delta Telereg_State output! : Stimuli_Or_Responses output! = cannot_change_msg CST_in_next_request_input_state = ~ = [Telereg_State | s t a t e = Waiting_f or_next_request_.input ] CST_valid_request_capability = * = Check_Validity_Of_Requests_Capability -CST_old_section_found_condition Telereg_State s e c t i o n : Section i d : SId e x i s t s o l d _ s e c t i o n : Section @ (CourseSchedule o l d _ s e c t i o n = CourseSchedule s e c t i o n and (old_section i n Registeredln id) CST_outstanding_fee_condition =*= COFAC_outstanding_fee_condition CST_Requirementl ="= CST_input_change_section and CS T _ v a l i d _ r e q u e s t _ c a p a b i l i t y and CST_in_next_request_input_state and not CST_outstanding_fee_condition and not InSTTSchedule.and ThereAreOpenings and CST_old_section_found_condition and not StudentEnrolledlnSection implies RegisterStudentlnSection and WithdrawStudentFromSectioh[old_section /section] and CST_change_section_feedback CST_Requirement2 ="= CST_input_change_section and not C S T _ v a l i d _ r e q u e s t _ c a p a b i l i t y or not CST_in_next_request_input_state or CST_outstanding_fee_condition or InSTTSchedule or not ThereAreOpenings or not CST_old_section_found_condition or StudentEnrolledlnSection implies CST_change_section_rej e c t i o n Change_Section_Thread =~= CST_Requirementl and CST_Requirement2 • ******************************************* rj^ -Qp Section Thread************************ -DST_input_drop_section Telereg_State section : Section input? = cirop_req ( section ; -DST_drop_section_f eedback --I Delta Telereg_State ! output! : Stimuli_Or_Responses j | output! = drop_msg i \ -DST_drop_section_re j e c t i o n : j i ! Delta Telereg_State ! | output! •': Stimuli_Or_Responses .1 j output! = cannot_drop_msg DST_in_next_request_input_state =^ = [Telereg_State | state = Waiting_for_next_request_input] DST_valid_request_capability. = " = Check_Validity_Of_Requests_Capability DST_outstanding_fee_condition = ~ = COFAC_outstanding_fee_condition DST_Requirementl =~= DST_input_drdp_section and DST_valid_request_capability and DST_in_next_request_input_state and not DST_outstanding_fee_condition and not InSTTSchedule and StudentEnrolledlnSection implies WithdrawStudentFromSection and DST_drop_section_feedback DST_Reguirement2 = ~ = DST_input_drop_section or not DST_valid_request_capability or not DST_in_next_request_input_state or DST_outstanding_fee_condition or InSTTSchedule or not StudentEnrolledlnSection implies DST_drop_section_rejection Drop_Section_Thread =^ = DST_Requirementl and DST_Requirement2 Look_Up_Inquiry_On_Sections_Thread** *»«**•«****•* -LOIST_input_lookup_section Telereg_State section : Section input? : Stimuli_Or_Responses input? = lookup_req(section) -LOIST_lookup_section_feedback Delta Telereg_State section : Section output! : Stimuli_Or_Responses output! = lobkup_msg(Availability section) LOIST_in_nexc_request_input_state = * = j [Telereg_State | state = | Waicing_for_.next_request_i.nput] LOIST_valid_request_capability =A= Check_Validi ty_Of_Requests_Capabi1i ty Look_Up_Inquiry_0n_Sections_Thread = ~ = LOIST_input_lookup_section and LOIST_valid_request_capabi1i t y and LOIST_in_next_request_input_state implies LOIST_lookup_section_feedback * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * ***** * *List_All_Courses_Thread* * ******************* - L A C T _ i n p u t _ l i s t _ a l l .-. Telereg_State input? * Stimuli_Or_Responses input? = l i s t _ r e q -LACT_1ist_all_feedback Delta Telereg_State i d : S i d output! : Stimuli_Or_Responses f o r a l l s : Section @ S i n (Registeredln id) and output! = list_msg (CourseSchedule s) LACT_in_next_request_input_state =~= [Telereg_State | state = Waiting_for_next_request_input] LACT_valid_reques t_capabi1i ty = A = Check_Validity_Of_Requests_Capability LACT_outstanding_fee_condition = ~ = COFAC_outstanding_fee_condition Li'st_All_Courses_Thread =~ = L A C T _ i n p u t _ l i s t _ a l l and LACT_valid_request_capability and LACT_in_next_request_input_state and not LACT_outstanding_fee_condition implies L A C T _ l i s t _ a l l _ f e e d b a c k *********************** *•* ************************** ********************************************************** ******* *Add_Specialization_Thread************************* -AST_input_add_specialization Telereg_State spec : S p e c i a l i z a t i o n inpu_" : Stimuli_Or_Responses input? = add_spec_req(spec) -A3T_add_specialization_f eedback--Delta Telereg_State i d : S i d output! : Stimuli_Or_Responses '/Off Delta Telereg_State output! : s t i-.uli_Or_Respor.ses output! = invalid_spec_msg AST_in_next_request_input_state =~= [Telereg_3tate | state = Waiting_for_next_request_input] -AST_valid_spec_condition Telereg_State spec : S p e c i a l i z a t i o n spec i n ValidSpec AST_in_spec_input_state =~= [Telereg__State | state = • Waiting_for_spec_input] AST_move_to_next_request_input_state ="= [Delta Telereg_State | sta t e ' = Waiting_for_next_request_input] -AST_add_spec_to_record- - -Delta Telereg_State i d : S i d spec : S p e c i a l i z a t i o n | StudentSpeC = StudentSpec + {id |-> spec) AST_Requirementl ="= AST_input_add_specialization and AST_in_next_request_input_state or AST_in_spec_input_state and not AST_valid_spec_condition implies A S T _ i n v a l i d _ s p e c i a l i z a t i o n _ r e j e c t i o n AST_Requirement2 =A= • AST_input_add_speciali z a t i o n and AST_in_next_request_input_state and AST_val"id_spec_condition implies • AST_add_spec_to_record .and AST_add_specializatioh_feedback AST_Requirement3 ="= ' AST_input_add_specialization and AST_in_spec_input_state and AST_valid_spec_condition implies AST_add_spec_to_record and AST_add_specialization_feedback and AST_move_to_next_request_input_state Add_Specialization_Thread ="= AST_Requirementl and AST_Requirement2 and AST_Requirement3 ***** *Handle_Hangup_Process * ************»•"*************** -HHUP_hangup_condition Telereg_State input? : Stimuli_Or_Responses input? = hangup hi HHUP_move_to_idle_state =A= [ Delta Telereg_State state IDLE.] Handle_Hang_Up_Process = * = HHUP_hangup_condition implies HHUP move_to_idle_state • + * + * * + * * * * * • * * * * • < end s p e c i f i c a t i o n WO APPENDIX E RADIATION THERAPY MACHINE - STRUCTURED SPECIFICATION s p e c i f i c a t i o n * . * , * * * « * * s ystem_configuration* ****-**•' *.* * «* *settings_and_registers * * * * * *' r * * * * * * * * * * * * * * * * * * * ITEM := nfrac | dose_to.t | dose | wedge | w_rot • | f i l t e r | leafO | leaf39 gantry | c o l l i m - | turnt | l a t | l o n g i t | height I doseB top | pt_mode | p t _ f a c t o r | press' | temp | d_rate | t_fac c a l v o l t l | c a l v o l t 2 | p_dose | p_time j e_time | s e t t i n g , dose_reg : P ITEM <setting, dose_reg> p a r t i t i o n ITEM dose_reg = { pt_mode, p t _ f a c t o r , press, temp, d_rate, t_fac, c a l v o l t l , c a l v o l t 2 , p_dose, p_time, e_time } | scale, s e l e c t i o n , counter : P ITEM < s e l e c t i o n , scale, counter> p a r t i t i o n ITEM counter = { nfrac, dose_tot, dose } s e l e c t i o n = {wedge, w_rot, f i l t e r , pt_mode } leaves == {leafO, l e a f 39 } preset == leaves union { wedge, w_rot, f i l t e r } motion == preset union { gantry, c o l l i m , turnt, l a t , l o n g i t , height } p r e s c r i p == motion union counter prescr == p r e s c r i p \ { l a t , l o n g i t , height } sensor == s e t t i n g \ { nfrac, "dose_tot .} i cal_const == { d_rate, t_fac, c a l v o l t l , c a l v o l t 2 } * * * * * * * * * * 2_ ^  g s * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * 1 VALUE == Z blank : VALUE t o l : SCALE --> value v a l i d : ITEM --> FIVALUE * * * * * * * * * * * * * * * * * * * * * * * f o r a l l s : ITEM @ blank n o t i n v a l i d s „ * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * ***** Interlocks * * * * * * * * * * ! • * * * * * * ! • * * * * * * * * * * * * * * * * * * * ' r ***** " INTLK :: = c l e a r | set INTERLOCK ::= c o l l i s i o n | gc_cc | tmc_error | fw_cc fw_fault | l c _ c c dosim | p t _ i n t l k l c c _ e r r o r | setup_timeout l c c _ c a l dmc_cal start_timeout | dmc_error | door | console pedestal | operator | update | p l c _ e r r o r | c s _ e r r o r i proton hw_intlk = = f c o l l i s i o n , dosim, door, console, pedestal, proton } sw_intlk == INTERLOCK \ hw_intlk ************************************************************** ' * *Subsystems' r ******* • SUBSYS ::= gantry_couch | f i l t e r s | col l i m a t o r | dosimetry | i n t l k s | proton_beam , set t i n g s == { gantry_couch -> { gantry, c o l l i m , turnt, l a t , l o n g i t , height, top}, f i l t e r s -> { wedge, w_rot, f i l t e r } , c o l l i m a t o r -> {leafO, leaf39} dosimetry -> { nfrac, dose_tot, dose, doseB } i n t l k s -> {}, proton_beam -> {}} i n t e r l o c k s == { gantry_couch -> { c o l l i s i o n , gc_cc, tmc_error) , f i l t e r s -> ( tmc_error, fw_cc, fw_fault}, c o l l i m a t o r -> {lc_cc, l c c _ c a l , l c c _ e r r o r } dosimetry -> { dosim, p t _ i n t l k , dmc_cal, s e t u p _ t i m e o u t s t a r t _ t i m e o u t , dmc_error}, i n t l k s -> { door, console, pedestal, operator, update, p l c _ e r r o r , ca_error}, proton_beam -> { proton} } * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * • * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * : ********** p r e s c r i p t i o n database* * *************************************' [ NAME ] PATIENT == NAME; FIELD == NAME | no_name : NAME no_patient == no_name ; n o _ f i e l d == no_name studies, p a t i e n t s : P PATIENT no_patient n o t i n studies and no_patient notin p a t i e n t s ACCUMULATION == counter --> VALUE PRESCRIPTION == p r e s c r i p --> VALUE Preset : studies --> (FIELD +-> PRESCRIPTION) Prescribed : patients --> (FIELD +-> PRESCRIPTION) Accumulated : .patients --> (FIELD +-> ACCUMULATION) f o r a l l s : studies @ n o _ f i e l d n o t i n dom(Preset s ) f o r a l l p : pa t i e n t s @ n o _ f i e l d n o t i n dom(Prescribed p) and dom(Prescribed p) = dom (Accumulated p) exceeded : ACCUMULATION <-> PRESCRIPTION f o r a l l counters : ACCUMULATION ; f i e l d s : PRESCRIPTION @ exceeded(counters, f i e l d s ) <=> (exists c : counter @ counters c >= f i e l d s z • ********* opera tor s ************''*****i'r*****,r*********************1 [OPERATOR] 112. no_opera-cr : OPERATOR ! operators, p h y s i c i s t s : P. OPERATOR | ph y s i c i s c s subseteq operators . j | . . w * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * ' * * * * * ! * * ** * **Session_State* * **************************»' MODE ::= therapy | experiment SessionVars mode : MODE operator : OPERATOR patient : PATIENT f i e l d : FIELD names : P PATIENT f i e l d s : FIELD +-> PRESCRIPTION counters : FIELD +-> ACCUMULATION operator = no_operator or operator i n operators mode = experiment implies operator i n p h y s i c i s t s names = i f mode = therapy then patients e l s e studies NoPatient SessionVars p a t i e n t = no_patient f i e l d = n o _ f i e l d f i e l d s = {} counters = {} PrescribedPatient SessionVars p a t i e n t /= no_patient p a t i e n t i n names f i e l d = no_f'ield or f i e l d i n dom f i e l d s f i e l d s = i f mode = therapy then Prescribed patient else Preset p a t i e n t mode = therapy implies counters = Accumulated p a t i e n t Session =A= PrescribedPatient or NoPatient I n i t S e s s i o n | NoPatient mode = therapy operator = no_operator * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * ******** *ODerat ions *********************************************** ExptModeS I Delta Session I operator i n p h y s i c i s t s NoPatient' (mode', names') = i f mode = therapy then (experiment, studies) e l s e (therapy, patients) operator' = ooerator IIJ -StoreFieldS J-Delta Session f i e l d ? : FIELD prescribed' : PRESCRIPTION accumulated' : ACCUMULATION patient /= no_patient f i e l d ' = f i e l d ? f i e l d s ' = f i e l d s union ( f i e l d ' -> prescribed'} mode = therapy implies counters' = counters union { f i e l d ' -> accumulated'} mode' = mode operator' = operator p a t i e n t ' = pa t i e n t names' = names *Login**•***' * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * ' -NewOperator Delta Session • operator? : OPERATOR operator' = operator? operator' i n operators P r i v i l e g e d -NewOperator mode = therapy or operator' i n p h y s i c i s t s mode' = mode p a t i e n t ' = patient names' = names f i e l d ' = f i e l d f i e l d s ' = f i e l d s counters' = counters -Unprivileged-NewOperator mode = experiment operator' n o t i n p h y s i c i s t s mode' = therapy NoPatient' | Logins = P r i v i l e g e d or Unprivileged * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * SelectPatient Delta Session patient? : PATIENT patient? i n names pat i e n t ' = patien t ? f i e l d ' = n o _ f i e l d f i e l d s ' = i f mode = therapy then Prescribed p a t i e n t ' e l s e Preset p a t i e n t ' mode.= therapy implies counters' = Accumulated p a t i e n t ' mode' = mode operator' = operator names' = names -SeiectFieldS Delta Session f i e l d ? : FIELD patient /= no_patien: f i e l d ? i n dom f i e l d s f i e l d ' = f i e l d ? operator' = operator mode' = mode patient' = patient f i e l d s ' = f i e l d s counters' = counters * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * ' * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * r ***** i r********p^g]_£^** ********************************************* * * * * p l _ l d g{-g£g******************************************** c a l _ f a c t o r , cal_const --> VALUE F i e l d • •"prescribed : PRESCRIPTION accumulated : ACCUMULATION measured : sensor --> VALUE overridden : prescr +-> VALUE computed, c a l i b r a t e d : dose_reg --> VALUE * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * T ! i • ir IT * T * T 1 Relation_to_Session_state* * ********************* P r e s c r i b e d F i e l d F i e l d Session f i e l d /= n o _ f i e l d mode = therapy implies p r e s c r i b e d = f i e l d s f i e l d no_prescrip == ( lambda p : p r e s c r i p @ blank) no_counter == (lambda c : counter @ blank) no_dose_reg ~= (lambda d : -d.ose_.reg ©"blank) no_dose == {p_dose -> blank, p_time -> blank} --NoFieldF-F i e l d p rescribed = no_prescrip accumulated = no_counter no_dose subseteq computed overridden = {} NoFieldS =~= [ Session | f i e l d = n o _ f i e l d ] NoField =A= NoFieldF and NoFieldS F i e l d S e s s i o n =A= P r e s c r i b e d F i e l d or NoField *,»*»»^,»*,»**,************************************** * * * * * * * * * * * * * * j - i t i a l i z a t i o n * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * r **** * - - I n i t F i e l d -NoFieldF computed' = c a l i b r a t e d = no_dose_reg + c a l _ f a c t o r : * * * * * * * * * * * * * * * * * * * * * * ' r ****** 1 • * * * * * * * * * * * * * * * * * i SelectPatientF Delta F i e l d NoField' computed' = computed * no_dose c a l i b r a t e d ' = c a l i b r a t e d * * * * * * * * * * * * * * » « * * * * * * • » • * * * * • * » * * • ' * * * * • » * * * ' ' * * • ' * Select p_ e__*****************»***********'*'****** NewFieldF — I Delta F i e l d S e s s i o n I prescribed' = f i e l d s f i e l d ' overridden' = {} SelectExptFieldF NewFieldF mode = experiment computed' = computed c a l i b r a t e d ' = c a l i b r a t e d DOSE == VALUE ; RATE == VALUE ; FACTOR == VALUE ; TIME == VALUE t_backup : (DOSE x RATE x FACTOR ) +-> TIME f o r a l l d : v a l i d dose, r : v a l i d d_rate ;f : v a l i d t _ f a c @ (d,r,f) i n dom_t_backup and t_backup(d,r,f) i n v a l i d p_time DoseTime Delta F i e l d ( l e t t == t_backup(computed' p_dose.computed' d_rate, computed- t_fac) ,@ c a l i b r a t e d ' =' c a l i b r a t e d + {p_time -> t}) computed' p_time = c a l i b r a t e d ' p_time {p_dose, p_time}<+ computed' = {p_dose, p_time} <+ computed NewTherapyField NewFieldF DoseTime mode = therapy-accumulated' = counters f i e l d ' SelectTherapyFieldF NewTherapyF i e1d computed' p_dose = pre s c r i b e d dose - accumulated dose overridden' = {} SelectSimpleFieidF =~= SelectExptFieldF or SelectTherapyFieldF 116 - -Se-ectCompiexr i e l d ? • NewTherapyFie Ld dose? : VALUE computed' p_dose = dose? ( l e t ovr == lambda c : counter | •accumulated' c >= prescribed' c @ accumulated c @ overridden' = i f dose? = prescribed' dose then ovr else ovr union { dose -> dose?}) r************************************ i Edit s e t t i n g * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * --EditF : , Delta F i e l d item? : ITEM value? : VALUE accumulated' = accumulated c a l i b r a t e d ' = c a l i b r a t e d EditPresetF - \ EditF item? i n preset prescribed' = pre s c r i b e d + { item? -> value? } overridden' = { item? } <+ overridden computed' = computed EditCalF EditE item ? i n dose_reg\ {p_dose, p_time} computed' = computed + { item? -> value? } prescribed' = prescribed 'overridden' = overridden EditDoseF---EditF. DoseTime item? = p_dose computed' p_dose = value? overridden' = overridden + { dose -> value? } prescribed' = pre s c r i b e d EditTimeF I EditF item? = p_time prescribed' = prescribed computed' = computed + { p_time -> value? } prescribed' = prescribed overridden' = overridden E d i t S e t t i n g F =~= Edi t C a l F or EditPresetF or EditDoseF or EditTimeF *********************************************** 111 'Override Over? I item? : ITEM Delta F i e l d j prescribed' = prescribed accumulated' = accumulated computed' = computed c a l i b r a t e d ' = c a l i b r a t e d Over ride_Set't ing* ******************** | OverF item? i n prescr overridden' = i f item n o t i n dom overridden then overridden + {item? -> measured item? } else {item? } <+ overridden -OverrideDose-OverF item? i n { p_dose, p_time} overridden' =" i f dose n o t i n dom overridden then overridden + {dose ->accumulated dose} else {dose } <+ overridden OverrideF =~= OverrideSetting or OverrideDose | ******************************************************* * * * * * store F i e l d * ************************************* * zero counter == (lambda c : counter @ 0) -StoreFieldF Delta F i e l d S e s s i o n computed' = computed + no_dose prescribed' = pres c r i b e d + ( p r e s c r i p <| measured) + no_counter + { n_frac -> 1 } accumulated' = zero_counter - overridden' = {} ca l i b r a t e d ' = c a l i b r a t e d i t * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * 1 r * * * * * * * * * * * * * * * * * -ExptModeF Delta F i e l d NoFieldF' computed' = computed + no_dose c a l i b r a t e d ' c a l i b r a t e d r*************************************************************** * * * * * * * * C a l i b r a t i o n _ f a c t o r s * * * * * * * * * * * * * * ! r * * * * * * * * * * * * : r * * * * * • PRESSURE == VALUE; TEMPRATURE == VALUE | pt_formula : (PRESSURE x TEMPRATURE) +-> FACTOR f o r a l l p : v a l i d p ress,t : v a l i d temp @ (p,t) i n dom pt_formula and pt_formula(p, t) i n v a l i d p t _ f a c t o r _Aute ="= [ F i e l d \ computed pt_mode = automatic PTIntlk---I n t l k F i e l d I i n t e r l o c k p t _ i n t l k = i f (PT_Auto and PT_Drift) orj ? _ I n v a l i d or T_In v a l i d then set else c l e a r ; i I i TherapySumlntlk | .Intlk j I therapy_sum = i f set i n i n t e r l o c k (|sw_intlk|). \ I then set else c l e a r j | * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * + * * * * * j * * * *setting_the_software_interlocks_and_flags * *********************** scanned == { gc_cc, fw_cc, fw_fault, l c _ c c , p t _ i n t l k , dmc_cal} Scanlntlk X i Session X i F i e l d Delta I n t l k Status' SS_Status' FilterWedgelntlk' DoseCallntlk' TherapySumlntlk' ( run = setup'and PTIntlk') or (run = running and i n t e r l o c k ' p t _ i n t l k = i n t e r l o c k p t _ i n t l k ) scanned <+ i n t e r l o c k ' = scanned <+ i n t e r l o c k ! * + * * * * * * * * * * * • * * * • * * . * * • * + * * * * * * • * * * * I n i t l n t l k | I n t l k run = setup therapy_sum = set rah c o n t r o l = { l o c a l } ran drive = { enabled } ran inconsistent = { set } ran status = ran ss_status = { not_ready } i n t e r l o c k = (lambda i : INTERLOCK © s e t ) + (lambda i:{ setup_timeout, start_timeout, update} @ c l e a r ) j *********************************•*****+***********•*************** j j + i n t e r f a c Q* * * * * * * * * * * ^ * * * * * * ^ ^ * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * . Event Delta Console '• input? : INPUT INPUT ::= filter_wedge | l e a f _ c o l l i m . dos e _ i n t l k | gantry_psa | dose_cal | startup | help | messages sele.ct_patient | s e l e c t _ f i e l d | field_summary | l o g i n | e d i t _ s e t t i n g edit_dose_reg | log_message | s^o'^e ' i p i c I override_crr.c i cancel_runl oassword I auto_setuo ! //f arrow | ignored OP : P INPUT OP = { filter_wedge, l e a f _ c o l l i m , dose_intlk, gantry_psa, dose_cal, startup, help, messages, se l e c t _ p a t i e n t , s e l e c t _ f i e l d , field_summary, lo g i n , e d i t _ s e t t i n g , edit_dose_reg, log_message, s t o r e _ f i e l d , override_cmd, cancel_run, password, auto_setup, expt_mode, cancel, r e f r e s h , shutdown, select} DISPLAY P : OP • DISPLAY = { filter_wedge, l e a f _ c o l l i m , dose_intlk, gantry_psa, dose_cal, startup, help, messages, sel e c t _ p a t i e n t , s e l e c t _ f i e l d , £ield_summa'ry, log * * * * * * *_onsole_state ********************************************** INTERACTION ::= a v a i l a b l e | d i a l o g | menu | confirm nmax : N SELECTION == {i : N | i <= nmax] [STRING] | empty .- STRING KEYSWITCH ::= locked | unlocked RUN ::= setup | running Console keyswitch : KEYSWITCH run : RUN d i s p l a y : DISPLAY op : OP i n t e r a c t i o n : INTERACTION item : ITEM n l i s t : P NAME l i s t _ i t e m : NAME menu_item : SELECTION bu f f e r : STRING InitConsole Console op = l o g i n d i s p l a y = l o g i n i n t e r a c t i o n = d i a l o g b u f f e r = empty * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * *****Elements_of_User_Interaction********************************* [ CAPTION, MESSAGE ] | a l e r t : CAPTION Ignore Event i X i Console | caption! : CAPTION caption! : a l e r t Unlocked. =~= [ Console | keyswitch = unlocked ] EventUnlocked ="= Event and Unlocked I2.0 E ver. t Un 1 o c ked input? = s e l e c t . 'Available* A v a i l a b l e ="= [ Console | i n t e r a c t i o n = av a i l a b l e ] -Op- EventUnlocked Available input? i n OP Setup [ A v a i l a b l e | run = setup Running =~= [ A v a i l a b l e | run = running ] SelectDisplay .1 OP input? i n DISPLAY display' = input? op' = d i s p l a y ' A v a i l a b l e ' Engaged = A = [ Console | i n t e r a c t i o n /= a v a i l a b l e ] . D o n e — ; I EventUnlocked Engaged op' = d i s p l a y d i s p l a y ' = d i s p l a y A v a i l a b l e ' Cancel ="= [ Done | input? = cancel ] x ^ * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * + + + *** *j^^s^s* ************ ***************************** l i s t : P DISPLAY default_name : PI NAME -> NAME . f o r a l l l i s t : PINAME @ default_name l i s t i n l i s t L i s t ="= [ Av a i l a b l e | d i s p l a y i n l i s t and n l i s t /= {} and list_it'em i n n l i s t ] S e l e c t L i s t I S e l e c t D i s p l a y input? i n l i s t ( ( n l i s t = {} and l i s t _ i t e m ' = no_name) or ( L i s t ' and l i s t _ i t e m ' = default_name n l i s t ' )) v_arrow == { up_arrow, down_arrow } aname : (v_arrow x NAME X PI NAME) -> NAME f o r a l l a : v_arrow; n : NAME; l i s t : P 1 N A M E @ aname (a, n, l i s t ) i n l i s t Continue = [ Delta Console | i n t e r a c t i o n ' = in t e r a c t i o n and op' = op and disp l a y ' = d i s p l a y GetListArrow .EventUnlocked Delta L i s t input? i n v_arrow i i s t _ i t e m ' = aname( input?, lit selected_msg : NAME -> MESSAGE SeiectName Select name! : NAME message! : MESSAGE L i s t name! = l i s t _ i t e m message! = selected_msg name! Tables * ********************************************* table : P DISPLAY default_item : table --> ITEM table_items : table —> PI ITEM f o r a l l d : table @ default_item d i n table_iterns d Table =~= [ A v a i l a b l e | d i s p l a y i n table and item i n table_items d i s p l a y SelectTable I S e l e c t D i s p l a y I input? i n table item' = default_item d i s p l a y ' Table' arrow == { right_arrow, left_arrow} union v I a s e t t i n g : ( arrow x ITEM x ta b l e f o r a l l a : arrow ;s : ITEM ; d : table @ ase t t i n g ( a , s, d) i n table_items d GetSettingArrow : EventUnlocked Delta. Table input? i n arrow item' = aset t i n g ( input?, item, d i s p l a y ) Continue s e t t i n g _ t a b l e , dose_reg_table : P table f o r a l l d : s e t t i n g _ t a b l e @ table_items d subseteq s e t t i n g f o r a l l d : dose_reg_table @ table_items d subseteq dose_reg •Selectltem Select | Setup Table item' = inem ( op' = edit_dose_reg and d i s p l a y i n dose_reg_table or op = e d i t _ s e t t i n g and item i n s e t t i n g E d i t i n g '• Console 11^ arrow -> ITEM automatic, manual VALUE -ScanPT Delta F i e l d c a l i b r a t e d ' p t _ f a c t o r = pt_formula ( c a l i b r a t e d press, c a l i b r a t e d temp) computed' pt _ f a c t o r = pt_formula (ca l i b r a t e d press, computed tempi (l e t p t _corr == i f computed pt_mode = automatic then c a l i b r a t e d ' p t _ f a c t o r e l s e computed' pt_factor© computed' c a l v o l t l = pt _ c o r r * c a l i b r a t e d c a l v o l t l and computed' c a l v o l t 2 = pt_corr * ca l i b r a t e d calvolt2) { p t _ f a c t o r } <+ c a l i b r a t e d ' = {pt_factor} <+ c a l i b r a t e d {pt_factor, c a l v o l t l , c a l v o l t 2 } <+ computed' ={pt_factor, c a l v o l t l , c a l v o l t 2 } <+ computed prescribed' = pre s c r i b e d accumulated' = accumulated overridden' = overridden * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * , * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * ' * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * *****Software_interlocks * * * * * * * * * * * * * * • • • i * * * * * * * * * * * * * * * * * * * * * * * * * * * * * 1 * * * I n t l k _ s t a t e * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * ' AUTO ::= l o c a l | auto RUN ::= setup | running ENABLE ::= enabled | disa b l e d READY ::= not_ready } ready•| override -Intlk run : RUN therapy_sum : INTLK i n t e r l o c k : INTERLICK —> INTLK status : s e t t i n g +->. READY ss_status : SUBSYS --> READY dr i v e : motion --> ENABLE inc o n s i s t e n t : motion --> INTLK co n t r o l : motion ---> AUTO * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * _Re1a t i on_t o_Se s s i on_and_F i e l d . * * * * * * * * * * * * * * * * * * * * * * * * * * * * * • * * * *,* * * * * * * * * * * * * * * * * * * * * * * * * -IntlkFieldSession-I n t l k F i e l d S e s s i o n dom overridden subseteq dom status dom status = i f mode = therapy then prescr e l s e preset * * * * * * * i * * * * * * : r************i : * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * **********2g*-£..j_~g. status f ] _ ^ g 5 * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * i | _ l == ( lambda x : Z @ max{x, -x}) SETUP .== s e t t i n g +-> VALUE . c~atus let: Match_) = = { 5 : s e t t i n g , setup : SETUP j (s i n s e l e c t i o n and setup s = measured s) or (s in scale and I setup s - measured s| <= t o i s)} @ status (lambda (lambda (lambda (lambda (lambda (lambda s : dom status © not_ready) + s : dom status [ Match (s, prescribed) © ready) + s : dom status i n t e r s e c t i o n counter j accumulated s < prescribed s © ready) + s : dom overridden | Match(s, overridden) © override)+ s : dom overridden i n t e r s e c t i o n counter © override) + s : dom status | measured s not i n v a l i d s @ not._ready) ) * * * * * *Check_and_confirm_interlocks ****** *********-** + * * * * * * * * * * * * * i -SS_Status . . I n t l k F i e l d S e s s i o n ( l e t ss_readiness (lambda ss == (lambda ss : SUBSYS @ not_ready) + SUBSYS | not_ready notin status (|settings ss |)©override) + (lambda ss : SUBSYS | {ready} = status (|settings ss|) © ready S (let(Check_Confirm_) == {ss:SUBSYS | ss_readiness ss = not_ready or enabled i n drive (|settings ss |) or set i n in c o n s i s t e n t (|settings ss|)}@ i n t e r l o c k fw_cc = i f CheckConfirm(filters) then set el s e c l e a r and i n t e r l o c k l c _ c c =if CheckConfirm(collimator) then set el s e c l e a r and i n t e r l o c k gc_cc = i f CheckConfirm (gantry_couch) then set else c l e a r and ss_status = (lambda ss : SUBSYS © i f set i n i n t e r l o c k (|interlocks ss |)then not_ready else ss_readiness ss))) . * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * • * * *Other_so ftware_interlocks * * *' FilterWedgelntlk I n t l k F i e l d * * * * * * * * * * * * * * * * ( l e t ms == {m : s e t t i n g s f i l t e r s | dr i v e m = dis a b l e d and measured m notin v a l i d m } © i n t e r l o c k fw_fault = i f ms /= 0 then set else c l e a r DoseCallntk I n t l k F i e l d ( l e t cs =={ c : c a l _ c o n s t | c a l i b r a t e d c n o t i n v a l i d c } © i n t e r l o c k dmc_cal = i f cs /= 0 then set else c l e a r p _ I n v a l i d = " = [ F i e l d computed press no t i n v a l i d press] T _ I n v a l i d =~= [ F i e l d computed temp not i n v a l i d temp] PT_Drift =~= [ F i e l d | computed p t _ f a c t o r - c a l i b r a t e d D"_factor | > t o l _ t _ f a c t o r ] IIH i n t e r a c t i o n i n { dialog, menu } (op = edit_dose_reg and item i n dose_reg or op = e d i t _ s e t t i n g and item i n s e t t i n g '•Confirm***********'****'*"** ** Confirm =A= [ Console | i n t e r a c t i o n = confirm | ocaption : OP -> CAPTION -ConfirmOp Op caption!, query! : CAPTION caption! = ocaption op' dis p l a y ' = d i s p l a y Confirm' AcceptConfirm =~= Confirm and Select and Done -| d e f a u l t _ s e l e c t i o n : SELECTION Menu =A= [ E d i t i n g | i n t e r a c t i o n = menu ] -MenuOp Op caption! : CAPTION menu! : iseqCAPTION menu_item' = d e f a u l t _ s e l e c t i o n d i s p l a y ' = d i s p l a y Menu' setting_info_name : ITEM -> CAPTION setting_value : s e l e c t i o n -> i s e q CAPTION f o r a l l s : s e l e c t i o n @ dom( setting_value s ) = v a l i d s -MenuEdit MenuOp Selectltem item i n s e l e c t i o n caption! = setting_info_name item; menu! = setting_value item amenu : (v_arrow x SELECTION x se l e c t i o n ) --> SELECTION f o r a l l s : s e l e c t i o n @ ( l e t n == #(valid s ) @ f o r a l l a : v_arrow, i : SELECTION @ d e f a u l t _ s e l e c t i o n <= n and amenu(a, i , s)) < = n) —GetMenuArrow EventUnlocked Delta Menu input? i n v_arrow menu_item' = amenu( input?, menu_item, i tem) Continue AcceptMenu ="= Menu and Select and Done MenuSettingC AcceptMenu • item! : ITEM ' • value! : VALUE • item! = item • j value! = menu_it;'em ! j | * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * *****Q^_^Qg************************* + * * * * * * * * * * * * * * * * * * * * * i | Dialog = * = [ Console | i n t e r a c t i o n = | dia l o g ]! | | DialogOp ! j Op i | | caption!, prompt! : CAPTION ". i l l caption! = ocaption op' displ a y ' = d i s p l a y Dialog' STRING, CHAR : P INPUT modify : (STRING x CHAR -> STRING GetChar EventUnlocked Delta Dialog input? i n CHAR", buf f e r ' = modify(buffer, input?) Continue | terminator : P INPUT Accept I Done Dialog input? i n terminator Reprompt EventUnlocked Delta Dialog input? i n terminator buf f e r ' = empty Continue MIN == VALUE ; MAX == VALUE | s e t t i n g _ i n f o : ITEM x MIN x MAX —> CAPTION| | | DialogEdit --• --DialogOp Selectltem item notin s e l e c t i o n prompt! = ( l e t v == v a l i d item @ s e t t i n g _ i n f o ( item, min v, max v )) sval : STRING --> VALUE EditSettingC Accept item! : ITEM value! : VALUE E d i t i n g item! = item ( l e t v == sval b u f f e r @ v i n v a l i d item and value! = v ) In v a l i d S e t t i n g = " = [ Reprompt | E d i t i n g and | sval buffer n o t i n v a l i d item ]I E d i t O r l n v a l i d S e t t i n g = EditSettingC or j I n v a l i d S e t t i n g | ****************************************************** — - f i r - - -*Therapy_console_operations ' * *Relation_tc_Session_state' ConsoleSession Console Session d i s p l a y d i s p l a y s e l e c t _ p a t i e n t implies n l i s t = names s e l e c t _ f i e l d implies n l i s t = dom f i e l d s r************************* 1 _Op_operatxons_ SimpleOp = ~ = Op and Continue ExptModeC SimpleOp Xi Session Delta ConsoleSession Setup input? = expt_mode operator i n p h y s i c i s t s auto_setup_display == { field_summary, filter_wedge, l e a f _ c o l l i m , dose_intlk} AutoSetupC SimpleOp Xi ConsoleSession subsystem! : auto_setup_display Setup f i e l d /= n o _ f i e l d d i s p l a y i n auto_setup_display input? = auto_setup subsystem! = d i s p l a y * * * * * * * * * * * * * * * * * * * * * r*********************************** ****** Select_Display_Operat i ons *************************** | simple_display == { fieldsummary, help } * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * *.* * * * * - * * * * * * * * * * * * * * * * * * * * * * * * * * * s e l e c t L i s t Operations******************************* l i s t = { s e l e c t _ p a t i e n t , s e l e c t _ f i e l d } S e l e c t P a t i e n t L i s t S e l e c t L i s t X i Session Delta ConsoleSession input? = s e l e c t _ p a t i e n t n l i s t ' = names S e l e c t F i e l d L i s t S e l e c t L i s t X i Session Delta ConsoleSession patient /= no_patient input? = s e l e c t _ f i e l d n l i s t ' = dom f i e l d s ********************************************************** *******SelectTableOperations********************* ********* | table = { gantry_psa, filter_wedge, l e a f _ c o l l i m , 111 ~ table_iterns = ( gan_ry_psa -> t gantry, c o l l i m , turnt • , { filter_wedge -> { f i l t e r , wedge, w_rot} l e a f _ c o l l i m -> leaves, dose_intlk -> { p_dose, p_time), dose_cai -> { pt_mode, press, temp, d_rate, j t_fac} ! se t t i n g _ t a b l e = { gantry_psa, filter_wedge, | lea f _ c o l l i m } | dose_reg_table = { dose_intlk, dose_cai } j * * * * * * * * * ConfirmOpOperations * * * * * * * * * * * * * * * i r ****** i cancel_run_query :- CAPTION •SelectCancelRun ConfirmOp Running input? = cancel_run op' = input? query! = cancel_run_query ********************************************************< * * * * * * * DialogOp_Operations * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * type_message_prompt, store_field_prompt: CAPTION -TypeMessage-DialogOp input? = l o g _ f i e l d op' = input? prompt! = type_message_prompt -E d i t F i e l d -DialogOp Setup input? = s t o r e _ f i e l d op' = input? prompt! = store_field_prompt r************************* *'* ***********************' * * * * * * ******** * Setup operations ******************************** SelectPatientC I SelectName Setup d i s p l a y = s e l e c t _ p a t i e n t Continue NewFieldC SelectName ConsoleSession Setup d i s p l a y = s e l e c t _ f i e l d SeleccSimpleFieldC I NewFieldC mode = experiment or ( counters name! dose = 0 and not exceeded! f i e l d s name!, counters name!)) Continue \1§ DoseDialogOp NewFieldC i DialogOp I Delta Consolel j 'op' = s e l e c t _ f i e l d p.ew_field' = name: mode = therapy Consolel ConsoleSession new_field : FIELD new_field i n dom -fields I i j ! s p r i n t f : VALUE -> STRING delivered_prompt : NAME x VALUE x VALUE x VALUE -> CAPTION S e l e c t D e l i v e r e d F i e l d DoseDialogOp counters new_field' > 0 not exceeded( f i e l d s new_field', counters new_field' ) ( l e t - d == f i e l d s new_field' dose; c == counters new_field' dose @ (l e t default_dose == d - c @ b u f f e r ' = s p r i n t f default_dose and prompt! = delivered_prompt ( new_field', d, c, default_dose))) exceeded_prompt : NAME x ACCUMULATION x ACCUMULATION -> CAPTION SelectExceededField : | DoseDialogOp exceeded; f i e l d s new_field', counters new_field') prompt! = exceeded_prompt (new_field', f i e l d s new_field', counters new^field') b u f f e r ' = empty Se l e c t F i e l d C = * = Sel'ectSimpleFieldC or S e l e c t D e l i v e r e d F i e l d or SelectExceededField SelectFieldOp-Consolel Dialog op = s e l e c t _ f i e l d o verride_table == { filter_wedge, l e a f _ c o l l i m , gantry_psa, d o s e _ i n t l k } | override_query : CAPTION -> CAPTION SelectOverride ConfirmOp Selectltem Xi Session f i e l d /= n o _ f i e l d d i s p l a y i n override_table input? = override_cmd op' = input query! = qverride_query ( setting_info_name item) ca l table == '{ dose_cal } (2-1 CalTable = - = [ConsoleSession | mode = experiment and d i s p l a y i n cal _ t a b l e ] -SettingTable ConsoleSession d i s p l a y i n dose_table or ( mode = experiment and di s p l a y i n preset_table) SelectCalMenu ="= CalTable and MenuEdit SelectCalDialog ="= CalTable and DialogEdit SelectSettingMenu ="= SettingTable and MenuEdit Selec t S e t t i n g D i a l o g -'"-SettingTable and DialogEdit | *************************************** * *Cancel Operations *********************************** Loggedln ="= [ Console | op noti n - { log i n , password }] CancelOp = * = Loggedln and Cancel ****************************************************** Accept_Confirm_Operations***************************** .OverrideC AcceptConfirm item! : ITEM op = override_cmd item! = item CancelRunC ="= [ AcceptConfirm I op = cancel run- 1 **************************** *„* * * * t ++ y ^ ++ ^ ^^ # + + ^-^^^^^| * * *Accept_Operations ********************************** log_msg : STRING --> MESSAGE —WriteMessageC Accept message! : MESSAGE op = log_message message! = log_msg buffer sname : STRING --> NAME store_msg : NAME --> MESSAGE •StoreFieldC Accept f i e l d ! : NAME message! : MESSAGE op = s t o r e _ f i e l d f i e l d ! = sname buffer message! = store_msg f i e l d ! SelectComplexFieldC Delta Consolel Accept f i e l d ! : FIELD dose! : VALUE SelectFieldOp f i e l d ! = new_field ( l e t d == sva'l buffer ( i d i n v a l i d dose and dose! = d ) ____ InvalidDose =^ = : Reprompt; Delta Consolel , j SeiectFieldOp and s v a l buffer ; notin v a l i d dose ] j ComplexOrlnvaiidField = ~ = SelectComplexFieldC or InvalidDose | Logout_and_Login | o_msg, lo_msg : OPERATOR -> MESSAGE Logout • : | Op . !' Xi Session < ! message! : MESSAGE | | Setup ' input? = l o g i n d i s p l a y ' = input? op' = d i s p l a y ' b u f f e r ' = empty message! = lo_msg operator Dialog' Console2 Console username : STRING EnterUsername--Delta Console2 Delta Dialog EventUnlocked op = l o g i n input? i n terminator username' = b u f f e r b u f f e r ' = empty op' = password di s p l a y ' = d i s p l a y USERNAME == STRING ; PASSWORD == STRING | soper: ( USERNAME x PASSWORD) -> OPERATOR .-LoginC DeltaConsdle2 ' EventUnlocked operator! : OPERATOR message! : MESSAGE op = password soper( username, buffer) i n operators input? i n terminator d i s p l a y ' = help op' = d i s p l a y operator! = soper ( username,' buffer) message! = o_message operator! A v a i l a b l e ' Unauthorized Delta Console2 Reprompt op = password soper( username, buffer) n o t i n operators username' = username LoginC or Unauthorized Even tun.:ocked op i n { lo g i n , password } input? = cancel op' = l o g i n buffer' = empty username' = empty display' = d i s p l a y .*»*other_Operations *•****•***•**»**•**** Refresh = ~ = [ Event | input? = refresh ] , Shutdown ="= [ Event | input? = shutdown ] | * * * * + * * • * • * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * *'* + Implementation* **********************************************' P h y s i c i s t ="= [ ConsoleSession | operator i n p h y s i c i s t s ] P a t i e n t L i s t = " = [ Console | d i s p l a y - s e l e c t _ p a t i e n t and n l i s t /= {} ] PatientSelected ="= [ ConsoleSession | patient /= no_patient ] F i e l d L i s t ="= [ Console | d i s p l a y = s e l e c t _ f i e l d and n l i s t /= {} ] F i e l d S e l e c t e d = * = [ ConsoleSession | f i e l d /= n o _ f i e l d ] AutoSetupDisplay = * = [ Console | d i s p l a y i n auto_setup_display ] OverrideTable ="= [ Console | d i s p l a y i n override_table ] Menultem = " = [ Console | item i n se l e c t i o n ] Dialogltem ="= [ Console | item n o t i n selection] LoggedOut =~= [ Console | op i n { l o g i n , password ] OverrideOp = ~ = [ Console | op = override_cmd ] • CancelRunOp = " = [ Console | op = cancel._run ] LogMessageOp = " = [ Console | op = log_message ] StoreFieldOp =A= [ Console | op = s t o r e _ f i e l d ] UsernameOp - = A= [ Console | op = l o g i n ] PasswordOp =A= [ Console | op = password ] Input =~= [ Input | input? : INPUT ] DisplayKey = * = [ Input | input? i n simple_display ] PatientKey =^ = [ Input | input? i n s e l e c t _ p a t i e n t ] FieldKey ="= [ Input | input? i n s e l e c t _ p a t i e n t ] TableKey = ~ = [ Input | input? i n table ] MessageKey =^ = [ Input | input? = log_message ] VArrowKey =A= [ Input | input? i n v_arrow ] SelectKey =~= [ Input | input? = s e l e c t ] ArrowKey ="= [Key =A= [ Input j input? Input | input? •Ill i r a r r o w ExptModeKey =*= [ Input i input? = expt_mode 1 AutoSetupKey =~= [ Input i input? = auto_setup ] StoreFieldKey = " = [ Input | input? = s t o r e _ f i e l d LoginKey ="= [ Input | input? =• l o g i n ] OverrideKey ="= [ Input | input? = override_cmd ] CancelRunKey =~= [ Input | input? = cancel_run ] CancelKey = ~ = [ Input | input? = cancel ] CharKey = * = [ Input | input? i n CHAR ] TerminatorKey = " = [ Input | input? i n terminator RefreshKey ="= [ Input | input? = r e f r e s h ] ShutdownKey = * = [ Input | input? = shutdown ] **„*,***,******************* • • + * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * 1 * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * *******C 0 +mbining_the_subsystems*************************'***************** ExptMode ="= ExptModeC and ExptModeS and ExptModeF Override .~' OverrideC OverrideF | item! = item? Override ="= OverrideC >> OverrideF Login ="= LoginC >> Logins E d i t S e t t i n g =~= EditSet t i n g C >> E d i t S e t t i n g F S t o r e F i e l d ="= StoreFieldC >> ( StoreFieldS and StoreFieldF ) SelectPatient = A = SelectPatientC >> ( SelectPatientS and Sele c t P a t i e n t F ) Selec t S i m p l e F i e l d = " = SelectSimpleFieldtC >> ( S e l e c t F i e l d S and SelectSimpleFieldF ) SelectComplexField ' ="= Se'lectComplexFieldC , >> ( S e l e c t F i e l d S and SelectComplexFieldF end s p e c i f i c a t i o n 

Cite

Citation Scheme:

        

Citations by CSL (citeproc-js)

Usage Statistics

Share

Embed

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

Comment

Related Items