Intro Software Eng
Intro Software Eng ECS 160
Popular in Course
Popular in Engineering Computer Science
This 37 page Class Notes was uploaded by Ashleigh Dare on Tuesday September 8, 2015. The Class Notes belongs to ECS 160 at University of California - Davis taught by Premkumar Devanbu in Fall. Since its upload, it has received 50 views. For similar materials see /class/187711/ecs-160-university-of-california-davis in Engineering Computer Science at University of California - Davis.
Reviews for Intro Software Eng
Report this Material
What is Karma?
Karma is the currency of StudySoup.
You can buy or earn more Karma at anytime and redeem it for class notes, study guides, flashcards, and more!
Date Created: 09/08/15
Notes on Z for E08160quot Premkumar Devanbu November 25 2008 1 Introduction Z is a language that can be used for formal speci cations It is used to deal with systems that have states inputs and outputs You can informally think of it this way system5tate fssystemmput and systemoutput f0systemmput system5tate Z can be used in such situations to describe the behaviour of the system Z has been widely accepted in industry and has been used in a range of different systems ranging from transportation to IT Transaction processing systems such as lBM7s 0108 and oating point arithmetic speci cation for micro computers Z offers all the standard advantages of formal speci cations 1 Z speci cations provide a precise statement of what the system should do the language is designed to make this convenient easy to under stand and express 3 Since it is a formal language that can be automatically processed it can be checked for correctness consistency desired properties etc 9 Certain kinds of partial completeness can be checked full completeness checking is impossible since we are modeling the real world how can we ever be sure we modeled everything in the real world that is relevant llve checked this carefully for mistakes But if you nd any please let me know as soon as possiblell Thank you 7 Doing formal speci cations early in the software development process can help nd faults early7 and thus save money Cf Formal speci cations can be used to validate continuously throughout the lifecycle Of course7 there are some disadvantages 1 Customers may not be able understand such speci cations 2 There is a fairly level of skill in mathematics that is required 3 There are some tools but a powerful7 integrated environment is lacking like say7 visual C or Symantec Cafe for Java trademarks both 2 The Basics Z speci cations clearly state whatthe operations in a system or subsystem do7 without stating how they are implemented For example7 a student in class asked if a 77 in a particular Z schema was an assignment or a conditional There are no assignments in Z it is not a programming language There are no conditionals either 77conditional only make sense if you were going to 77do77 something in either case Z speci cations just specify they such say what will be true about the system7 rather than saying how they should be implemented This is done abstractly7 by talking the systems behaviour in terms of sets7 relations7 types7 and other abstract mathematical objects In this sense7 Z is very similar to set theory in fact7 the language of Z is a logical language But7 while Z speci cations are written a logical language7 it uses symbols that strongly typed7 like the language Java In Java you cannot say int i j String X ji X Likewise7 in Z you cannot say aProf Professor meaning that aProf is of the type Professor and then say7 later on primeNumbermProf 21 So What are the types in Z Z has some built in types just like in most programming languages So Z has type N which are the natural numbers and the type Z which is the set of integers In addition Z also has enumerated types which are called free types So we can say this DayofWeek mon tues wed thurs fri sat sun Transaction insert delete modify In addition Z also has basic types What are these These are types that would correspond to structures records or other types of constructed types in languages like C Pascal and Java But here in Z we dont care about the actual implementation so we only use the names of the structures without stating their actual implementation So we might say Student Book ClassRoster Professor AirlineReserization to refer to some basic types which are to be implemented as some non trivial datastructures Z also has power set types so HDTransaction refers to the powerset of the Transaction free type above and likewise HDDayofWeek 22 Declarations All variables used in Z must be declared So we can have declarations such as thisProf Professor aDay DayofWeek We can declare variables like this classSize N quizGrade Z 23 Some Z Expression Z has the typical expressions from set theory Now consider the following declarations 239j N b Book 1 Author onLoan lP Book anAuthor Author publ2shedResearohers lP Author Are the following expressions are well typed 2 onLoan U b 239 739 Z39 739 297 07 b 2 j onLoan Q Book 2 E Book b E onLoan 27 b onLoan U publ2shedResearchers 3 What can you say with these Types Z describes systems by describing the following State which describes the states of the system7 including all the relevant properties that need to be modeled Events which can change various aspects of the states of the system7 and Observations which are ways in some variable with is a part of the state can be read 31 Basic Set Notation These things are described using formulae that come out of set theory So rst7 you get some notation N Natural Numbers Z Integers a E S a is an element of S a Z S a is not an element of S Q 27 f 7457 U H A B Those elements of A that are not in B EDA powerset of A Students Number of elements in the set Students And there are some logical operators V7 7 m D l P o x set of elements z according to declaration such that P a i b b is true whenever a is true a gt b b is true exactly when a is true And there are some expressions denoting relationships 1 lt gt 2 relationship between sets 1 and 2 1 a 2 total function from 1 to 2 1 4 2 partial function from 1 to 2 Using these notational devices7 we can state various things as predicates waitList7 enRolled lP Student maxClassSize N These declare the variables maiClassSize etc In Z declared variables represent the state ofthe system Z describes the effects of actions by talking about states before and after actions For this purpose7 you can talk about the state of a variable after an action by using the prime 77 7 77 notation thus enrolled refers to the set of enrolled students after some action With these declarations7 we can now state predicates such as enRolled S maiClassSize enROlled S maiClassSize as an invariant which is always true We can also describe the effect of an operations such as enrolls7 by waitList waitlist s7 enRolled enRolled Us7 32 States States in Z are described by schemas Schemas are a combination of a type declaration7 and a property speci cations ln Z notation a schema looks like this 7 aSchemaName Declarations or signatures Predicates For example7 i Class enrolled HDStudent enrolled S marClassSz ze It may be helpful to think of schemas by analogy to classes in C The declarations are like private member variable declarations the predicates make use of these variables to make assertions Schema names can refer to other schema names in the declaration part7 as a way of 77importing77 declarations into themselves7 and can then make assertions about them An initial state is described thus i Initial Class enrolled b In Z states after operations are shown with a prime 777 Thus7 as Class goes through various operations7 it7s 77post operative77 state can be described as i Class enrolled HDStudent enrolled S marClassSz ze 33 Events Now we can start describing events or operations For every state described as a schema we can have a change A operator de ned as follows i AClass Class Class or we can write this full detail by combining Class and Class i AClass enrolled HDStudent enrolled HDStudent enrolled S madClassSz ze enrolled S madClassSz ze Thus we can now describe the operation of adding a student to a class i AddClassO AClass s Student s Z enrolled enrolled lt maxClassStze enrolled enrolled Us leewise we can have DropClassO i DropClassO AClass s Student s E enrolled enrolled enrolled 57 34 Observations Z also has a facility for observing schemas7 ie7 checking out the values Thus for the Class schema7 we can de ne an observation schema i EClass enrolled HDStudent enrolled HDStudent enrolled S marClassSz ze enrolled S marClassSz ze enrolled enrolled Now we can 77import this schema into other observations which have some interesting properties i ClassSz39ze EClass numberInClass N numberInClass enrolled Here7s another one i StudentInClass EClass response yes no s Student 7s 6 enrolled response yes V 7s Z enrolled response no 35 Exceptions We can handle error conditions in this way Message ok alreadyInClass Full notInClass 8 i okMessoge output Message output ok One possible error schema i AddClossError ECloss s Student output Message s Z enrolled enrolled moxClossStze output Full Vs7 E enrolled output olreodyInCloss So the complete AddClass AddCloss AddClosso okMessoge V AddClossError Likewise DropClass i DropClossError ECloss s Student output Message s Z enrolled output notInCloss and the full DropClass DropCloss DropClosso okMessoge V DropClossError 4 Relations and Functions So far we7ve been talking about sets such as Class and Student7 and indi vidual members of such sets Z has special notations for talking about potrs of things FOr example7 consider the following sets Student Class Faculty GrodStudent ClossRooml 9 Now in Z you can de ne a cross product like this Student gtlt Class and thus set of all possible subsets of this relation HDStudent gtlt Class This is also denoted in Z Student lt gt Class and thus we can declare the Enrollment relation as Enrollment Student lt gt Class Z also has total functions which are denoted by a and partial functions which are denoted by 4 These can be used to denote the Instructs function every course has one speci c instructor and Venue partial function some courses may not meet Instructs Class a Faculty Venue Class 4 ClassRoom Additionally in relations you can have a particular instance of a relation called a maplet Here7s an example rnaplet of type Instructs E05160 gt gt prem oops is above right Z has notation for updating relations with rnaplets for example to change the instructor for E08160 I can do the following Instructs EB E05160 gt gt BtllClz nton The Instruct behaves exactly the same as before for every Class except E05160 which is now maps to BlllCllnton You can also specify the domain and range of functions or relations which corresponds to dom Instructs ran Venue What can we say about the domain of Instructs and the Range of Venue NOW let us de ne a simple transaction processing system for accounts payable 10 Accounts Payable Example First we have two types Firms Dollars Here7s the basic schema i AccountsPayable suppliers lP Firms amountsDue Firms 4 Dollars dom amountsDue Q suppliers This says that only people you owe money to are your suppliers well see that you can only purchase things from authorized suppliers amountsDue is a partial function its a partial function from Firms to Dollars Why is this becuase we can only owe money to rms who are suppliers7 and not all rms are suppliers However7 once a rm gets into our list of suppliers7 then each of those must have an amount that we owe to that rm In the initial state below7 we have 3 rms7 and we owe no money to each of them i Initial AeoountsPayabl e amountsDue Akai gt gt 07 Midori gt gt 07 Kinka gt gt 0 suppliers Altai7 Midori7 Kinka Ooops7 is the speci cation the dom of amountsDue correct Should it be a Q of suppliers or equal to it Now we consider a purchase transaction i PurchaseTr 39 AAecountsPayable supplier Firm amount Dollar supplier E suppliers amountsDue amountsDueEB supplier gt gt amountsDue supplier amount and a payment transaction i PaymentTr t39 AAccountsPayable supplier Firm amount Dollar supplier E suppliers amountsDue amountsDueEB supplier gt gt amountsDue supplier 7 payment We can also have a way to add suppliers i AddSupplier AAccountsPayable supplier Firm amountsDue amountsDue Usupplier gt gt 0 suppliers suppliers Usupplier And an observation about how much money we owe anybody i WhatDue EAccountsPayable supplier Firm amount Dollars supplier E suppliers amount amountsDue supplier 5 Sequences and some datastructures Z can be used to model abstract datastructures Stacks of anything7 Double ended queues of anything7 binary trees of anything that has a total order7 12 etc well look at stacks First what is a sequence in Z A sequence is declared thus z seq T where T is any of types in Z This is actually equivalent to the declaration zN14T where domx1x where z is the length of the sequence N1 refers to the natural numbers 2 1 Sequences are shown within angle brackets or as relations lt 9 14 2333 gt 07quot as 1 H 92 H 143 H 234 H33 and Empty sequences are shown as ltgt Sequences support several operations selection lt man tugs wedthurs fm39 sat sun gt 4 thurs concatenation lt mantues gt A lt wedthurs gtlt mantueswedthurs gt head head lt man tue5wed gt man last last lt man tugs wed gt wed tail tail lt mantueswed gtlt tue5wed gt front front lt mantues wed gtlt mantues gt 13 51 Stack Example i StackT st seqT i StackInit StackT st ltgt i pushT Astack item T stack lt item gt stack i poplTl Astack item T item head stack stack tail stack What7s rnissing errors7 of course How would I describe stack under ow How can describe the size of the stack etc Hint add another variable of type N to the stack 52 A Sequential File Such a le is a Sequence of records stored one after another on an external storage device A le can be either an input or an output le7 but not both at the same time In a sequential le7 access to the nth record is only possible if 7171 records are rst read in order T is the type ofthe record an unspeci ed basic type i sequleT file seq T unread seq T alreadyread seq T mode FileMode alreadyread read file FileMode input l output Keep in mind here that read and write are incompatible In this example7 a File cannot be open for read and write at the same time That simpli es matters for the purposes of this example Now lets open a le for input 7 openReale AsequlelT mode input unread file file file why is unread le and le the same as le Now lets do a read mode input unread 7Eltgt lt x gt Aunread unread alreadyread alreadyread lt x gt mode mode file file ECS 160 Devanbu Requirements wRapid Prototyping Use case Analysis 1 What are Use cases 2 A Use case Example 3 Where are they used 4 Use case FAQ 5 Relationship to next lecture Typeset by FoiITEX P Devanbu ECS 160 Devanbu Definition of Use cases A Use case is a collection of possible sequences of interactions between the system under discussion and its external actors related to a particular goal Aistair Cockburn Ivar Jacobson Important 0 Interaction Connects one actor39s goal to the system39s or another actors39 responsibilities 0 Scope External or Internal 0 Hierarchical Each interaction can summarize a lower level Use case 0 Complete They go on until success or abandonment Typeset by FoilTEX P Devanbu 2 ECS 160 Devanbu An Example Airline Ticket Purchase Goal Buy a ticket Scope External UI Pre Conditions UAL Res System Up Customer has acct Success State Purchased valid tkt 1 reservation on ight Failed State No Effect Primary Actor Customer Secondary Actor None Start Action Customer login to United Connections Description OOI OTHgtOJIDgt k Customer Logs into Website Customer Enters dates amp travel endpoints System checks availability amp price System shovvs availaibility to customer Customer selects ights System reserves seats System presents charge form to customer Customer enters charge information System charges the cost of ticket 9 System sends receipt to customer 10 Customer logs out Variations No seats ights available Customer rejects ightsprices Charge card invalid Extensions Ni OJNr K System may offer free upgrades to FF Payment may be with FF miles Typeset by FoiITEX P Devanbu 3 ECS 160 Devanbu Explanation of Use case Template Goal The Primary Actor s Goal Scope External to System or Internal Pre Conditions When this Use case is applicable Success State The state of the world When Use case ends Failed State and if it fails Primary Actor Whose goal is of concern Secondary Actor Who might help the system Start Action the trigger action Description 1 Interactions 2 Variations 1 Exceptional conditions 2 Extensions 1 Additions to basic function 2 Typeset by FoiITEX P Devanbu ECS 160 Devanbu Using Use cases 0 In Requirements 1 Help identify exceptional conditions 2 Help locate extesions 3 Can be used in other Use cases modular reuse or extended inheritance type reuse o In addition to requirements 1 To identify common functionality for software design Use cases are the key step in 00 Analysis methods 2 For validating software designs 3 For testing 84 validation implementations 4 For creating manuals 5 For designing Ul interfaces Typeset by FoilTEX P Devanbu 5 ECS 160 Devanbu Use case FAQ 1 How many Use cases 0 One for each main goal of each type of user 2 How many variations 0 One for each deviation that affects user39s goal in the particular Use case 3 What should NOT be in a Use case 0 Internal system details that don39t directly affect the user s goals 0 Any eventinteraction that doesn t relate to a specific goal 0 User interface design doesn t matter if buttons menus etc 4 When is a Use case complete 0 When goal has been acheived or there is a failure 5 How to use it with Rabid Prototyping 0 Implement each Use case so that variations amp extensions can be handled easily later Typeset by FoilTEX P Devanbu 6 ECS 160 Devanbu Ask these questions 1 Is the Use case complete Are there any details that need to be added Actors Goals Success state Failure State Variation Extension 2 Do feel confident that the actor39s goal is going to be properly met 3 Can the Use case be simplified By changing terminologyfunction etc 4 Are there any additional Actors that should participate in this Use case 5 Are there any additional Goals of the Actor that are not addressed 6 Have I considered all the Actors Questions applicable to entire set of Use cases Typeset by FoilTEX P Devanbu 7 ECS 160 Devanbu Thinking about Requirements Methods 0 What are the common goals of requirements methods the AYE method and the Use case method How are they different 0 Applicability review o Is this an exact science Can we prove these methods work 0 The big players Michael Jackson Pamela Zave lvar Jacobson David Parnas Sol Greenspan Alex Borgida Typeset by FoilTEX P Devanbu 8 ECS 160 Devanbu L11 Architectural Styles Outline 1 Architectural Style Outline 2 Several Example StylesTradeoffs 3 A practical Example Aer Monitoring software Typeset by FoiITEX P Devanbu ECS 160 Devanbu L11 Example A Compiler Perry amp W011P Two possible configurations same components different con DECOFS Internal Representation Typeset by FoiITEX P Devanbu 2 ECS 160 Devanbu L11 Architectural Styles quotAn Architectural Style defines a vocabulary of components and connector types and a set of constraints on how they can be combined there may also exist one or more semantic models that specify how to determine a system39s overall properties from the properties of it s parts Garlan amp Shaw Describing Architectures vocabulary types of components amp connectors allowable structural patterns underlying computational model invariants of this style common examples of use Chowpotng advantages and disadvantages Typeset by FoiITEX P Devanbu 3 ECS 160 Devanbu L11 Pipes and Filters Style Examples Unix pipesfilters some batch processing systems HTTP clientsservers arranged as content filters Vocabulary Components gt filters and connectors gt pipes COmputational Model Pipes are data streamers Data is processed when available filters are concurrent processes Invariants Filters mutually unaware Data types are uniform across the pipe line Filters terminate when EOF is reached or when connection is closed No state shared across filters Design Trade offs Must consider ve Simple interface and composition filters reusable and separately evolvable can be analyzed for thoughput resource consumption etc naturally concurrent execution Typeset by FoiITEX P Devanbu 4 ECS 160 Devanbu L11 ve Each filter is monolithic not compatible with interactive computing because of data uniformity may force lowest common denominator data format Communication patters are restricted Typeset by FoilTEX P Devanbu 5 ECS 160 Devanbu L11 Layered Style Examples TCPIP Protocol Stack Java Virtual Machine Vocabulary component gt layers connectors gt callsrequests C0mputational Model Layers implement services for enclosing layers as procedure calls or Synchronous RPC using services provided by enclosed layers as clients Invariants Layer service requests go only quotinsidequot and only to the immediately enclosed layer Design Trade offs Must Consider ve Increasing well defined layers of abstraction separation of concerns greater evolvability ve Levels of abstractions may not always be clear optimization difficulties eg partial evaluation Typeset by FoiITEX P Devanbu 6 ECS 160 Devanbu L11 BulletinBoard Style Chat Transcript I Repository Examples Compilers rule based systems file systems chat groups Vocabulary components gt knowledge sources connectors gt blackboard da tastructures BB COmputational Model Knowledge sources post updates to BBDS other knowledge sources can then observe this and respond with their updates Invariants Knowledge sources find out updates in order that they happen all knowledge sources are quotawarequot of all data Design Trade offs Must Consider ve Suitable for evolving applications new types of data can easily be added Promises modular addition of new knowledge sources Typeset by FoiITEX P Devanbu 7 ECS 160 Devanbu L11 ve Effects of an update can be difficult to trace through the system Typeset by FoiITEX P Devanbu 8 ECS 160 Devanbu L11 EventBased St Event Channel Examples Office Automation monitoringalarm systems distributed software configuration GUIs trading systems Vocabulary components gt sourcessinks connector gt event channels multicast groups etc C0mputational Model Sources generate events sinks that register events are notified of events Invariants Sources don39t know all the subscribers event generation and notification are asynchronous Design Trade offs Must Consider ve Late binding Components new events can be introduces at any time ve Event sources have no control over the computational ramifications of Typeset by FoiITEX P Devanbu 9 ECS 160 Devanbu L11 event generation no centralized control deadlocks message saturation etc are possible Typeset by FoilTEX P Devanbu 10 ECS 160 Devanbu L11 ClientServer Systems Examples Web POP SMTP etc Vocabulary components gt client server connector can vary C0mputational Model Server is persistent Clients initiate use synch calls Invariants server location known to clients many clients share a server servers highly reliable fast etc clients are not Design Tradeoffs Consider ve Scaleability simple concurrency control widely used ve Fat hard to maintainevolve clients administrative headaches single point of failure can be difficult to maintainevolve ThreeTier Systems Examples AuctionE commerce Servers Vocabulary components gt client middlebusiness logic DBlegacy connector can vary C0mputational Model middleDB layers are persistent and shared Clients initiate Invariants Thin clients Middle tier has concurrency control etc Legacy systems wrapped for inter operability Design Tradeoffs Consider ve Thin Clients easy to care for Separation of Concerns Inter operability reuseleverage Typeset by FoilTEX P Devanbu 11 ECS 160 Devanbu L11 ve Points of Failure middle layer complexity eg SAP SSA wrappers hard to buildcare for Typeset by FoilTEX P Devanbu 12 ECS 160 Devanbu L11 Case Study Event Monitoring System Monitoring System Alarm 1 Sytem Being Monitorm Alarm2 Monitored System Alarm 3 Monitoring System 0 0 Logging Device tor O quotC D 3 What39s a good high level architecture Typeset by FoiITEX P Devanbu 13 ECS 160 Devanbu L11 Just one Monitoring Element Monitoring System 4 R1116 1 Events Rule 2 Rule 3 Rule 11 A Hybrid architecture Typeset by FoiITEX P Devanbu 14
Are you sure you want to buy this material for
You're already Subscribed!
Looks like you've already subscribed to StudySoup, you won't need to purchase another subscription to get this material. To access this material simply click 'View Full Document'