Today s Lecture Continue to discuss the Make example Lecture 6 Operational Specifications It illustrates each of the three specification styles introduced in lecture 5 Begin to explore Operational Specifications in more detail Kenneth M Anderson Foundations of Software Engineering CSCI 5828 Spring Semester 2000 February 3 2000 The Make Example 2 Make Specification Language Dependencies are Relational Lecture 5 Described according to desired relationships Usually given in terms of multi hyper graphs We worked on an example specifying some properties of Make Rules are Declarative However Make is a specification language itself Described according to desired properties Usually given in terms of axioms or algebras It specifies dependencies between artifacts It specifies rules for creating new artifacts It specifies actions to carry out the rules February 3 2000 Kenneth M Anderson 2000 Kenneth M Anderson 2000 Actions are Imperative Described according to desired actions Usually given in terms of an execution model 3 February 3 2000 Kenneth M Anderson 2000 4 Example Makefile More on Make Target Make is well integrated into a Unix C environment Dependencies T1 T2 T3 T4 A1 A2 A3 Primitive Components are Files Actions are shell commands Rules are placed in a file and denote the specification Rules Kenneth M Anderson 2000 5 February 3 2000 T1 T3 T5 T6 T7 Kenneth M Anderson 2000 6 Questions Rules can have interdependencies T2 Actions T3 T5 T7 A5 A6 Rules make explicit the dependencies of the system and what to do about them February 3 2000 T2 T5 T6 A4 What is the concept of dependence in this system How is it modeled T4 Why are rules considered declarative and shared dependencies February 3 2000 Kenneth M Anderson 2000 7 February 3 2000 Kenneth M Anderson 2000 8 Hybrid Style Issues Operational Specification Consider programming languages Focuses on Control Aspects They are primarily operational Here we choose to look at control issues rather than data issues What about them are declarative or relational Most languages will have a chief modeling style Examples Contrast statements in a program with Make s Control the flight path of an airplane Control the speed of a car 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 of questions than with another style Is there a unique way to achieve the target Is a target feasible February 3 2000 Kenneth M Anderson 2000 9 Formalisms and Foundations Kenneth M Anderson 2000 10 Informal Problem Description 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 logic February 3 2000 February 3 2000 Preview of Finite State Machines Formalisms Of course there are data aspects to these problems However we view them more as parameters that influence the actions of the system Kenneth M Anderson 2000 11 When turned on by the driver a cruise control system automatically maintains the speed of a car over varying terrain When the brake is applied the system must relinquish speed control until told to resume The system must also steadily increase or decrease speed to reach a new maintenance speed when directed to do so by the driver February 3 2000 Kenneth M Anderson 2000 12 Example Continued Example Continued There are seven inputs System on off If on denotes that the cruisecontrol system should maintain the car speed Engine on off If on denotes that the car engine is turned on the cruise control system is only active if the engine is on Pulses from wheel A pulse is sent for every revolution of the wheel February 3 2000 Kenneth M Anderson 2000 13 In class Example We will now develop a finite state machine to 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 example February 3 2000 Kenneth M Anderson 2000 15 Accelerator Indication of how far the accelerator has been pressed Note The accelerator does not turn off the cruise control system it pauses the system Brake On when the brake is pressed the cruise control system temporarily reverts to manual control if the brake is pressed Increase Decrease Speed Increase or decrease the maintained speed only applicable if the cruise control system is on Resume Resume the last maintained speed only applicable if the cruise control system is on February 3 2000 Kenneth M Anderson 2000 14
View Full Document
Unlocking...