Lecture 6Operational SpecificationsKenneth M. AndersonFoundations of Software EngineeringCSCI 5828 - Spring Semester, 2000February 3, 2000 © Kenneth M. Anderson, 2000 2Today’s Lecture• Continue to discuss the Make example– It illustrates each of the three specificationstyles introduced in lecture 5• Begin to explore Operational Specificationsin more detailFebruary 3, 2000 © Kenneth M. Anderson, 2000 3The Make Example• Lecture 5– We worked on an example specifying someproperties of Make• However, Make is a specification languageitself– It specifies dependencies between artifacts– It specifies rules for creating new artifacts– It specifies actions to carry out the rulesFebruary 3, 2000 © Kenneth M. Anderson, 2000 4Make Specification Language• Dependencies are Relational– Described according to desired relationships– Usually given in terms of multi/hyper graphs• Rules are Declarative– Described according to desired properties– Usually given in terms of axioms or algebras• Actions are Imperative– Described according to desired actions– Usually given in terms of an execution modelFebruary 3, 2000 © Kenneth M. Anderson, 2000 5More on Make• Make is well-integrated into a Unix/Cenvironment– Primitive Components are Files– Actions are “shell commands”– Rules are placed in a file and denote the“specification”• Rules make explicit the dependencies of the systemand what to do about themFebruary 3, 2000 © Kenneth M. Anderson, 2000 6Example “Makefile”T1: T2 T3 T4 A1 A2 A3T2: T5 T6 A4T3: T5 T7 A5 A6TargetActionsDependenciesRulesFebruary 3, 2000 © Kenneth M. Anderson, 2000 7T1T2 T3 T4T5 T6 T7… and shared dependencies!Rules can have interdependenciesFebruary 3, 2000 © Kenneth M. Anderson, 2000 8Questions• What is the concept of dependence in thissystem? How is it modeled?• Why are rules considered declarative?February 3, 2000 © Kenneth M. Anderson, 2000 9Hybrid Style Issues• Consider programming languages– They are primarily operational• What about them are declarative or relational?• Most languages will have a chief modeling style– Contrast statements in a program with Make’s• S1 S2 S3… operational, do these statements in this order• Rules in a makefile: declarative, achieve this target– One style will lead you to ask different sorts ofquestions than with another style• Is there a unique way to achieve the target? Is a target feasible?February 3, 2000 © Kenneth M. Anderson, 2000 10Operational Specification• Focuses on Control Aspects– Here we choose to look at control issues rather thandata issues• Examples– Control the flight path of an airplane– Control the speed of a car• Of course, there are data aspects to theseproblems. However we view them more asparameters that influence the actions of the systemFebruary 3, 2000 © Kenneth M. Anderson, 2000 11Formalisms and Foundations• Formalisms– Finite State Machines (FSMs)– Petri Nets– Statecharts - used in UML– Communicating Sequential Processes (CSP)• Latter three are different attempts to add concurrency to FSMs• Mathematical Foundations– Graph theory, automata theory, modal logicFebruary 3, 2000 © Kenneth M. Anderson, 2000 12Preview of Finite State Machines• Informal Problem Description– When turned on by the driver, a cruise-controlsystem automatically maintains the speed of acar over varying terrain. When the brake isapplied, the system must relinquish speedcontrol until told to resume. The system mustalso steadily increase or decrease speed to reacha new maintenance speed when directed to doso by the driver.February 3, 2000 © Kenneth M. Anderson, 2000 13Example Continued• There are seven inputs:– System on/off: If on, denotes that the cruise-control system should maintain the car speed.– Engine on/off: If on, denotes that the car engineis turned on; the cruise-control system is onlyactive if the engine is on.– Pulses from wheel: A pulse is sent for everyrevolution of the wheel.February 3, 2000 © Kenneth M. Anderson, 2000 14Example Continued– Accelerator: Indication of how far the accelerator hasbeen pressed. Note: The accelerator does not turn offthe cruise-control system, it “pauses” the system– Brake: On when the brake is pressed; the cruise-controlsystem temporarily reverts to manual control if thebrake is pressed.– Increase/Decrease Speed: Increase or decrease themaintained speed; only applicable if the cruise-controlsystem is on.– Resume: Resume the last maintained speed; onlyapplicable if the cruise-control system is on.February 3, 2000 © Kenneth M. Anderson, 2000 15In-class Example• We will now develop a finite state machineto help formalize the problem description• Method– Identify states– Identify transistions between states– Keep it simple, if it starts to get too complex,we are heading down the wrong path• <See class video for rest of
View Full Document
Unlocking...