DOC PREVIEW
USC CSCI 599 - October5a

This preview shows page 1-2-21-22 out of 22 pages.

Save
View full document
View full document
Premium Document
Do you want full access? Go Premium and unlock all 22 pages.
Access to all documents
Download any document
Ad free experience
View full document
Premium Document
Do you want full access? Go Premium and unlock all 22 pages.
Access to all documents
Download any document
Ad free experience
View full document
Premium Document
Do you want full access? Go Premium and unlock all 22 pages.
Access to all documents
Download any document
Ad free experience
View full document
Premium Document
Do you want full access? Go Premium and unlock all 22 pages.
Access to all documents
Download any document
Ad free experience
Premium Document
Do you want full access? Go Premium and unlock all 22 pages.
Access to all documents
Download any document
Ad free experience

Unformatted text preview:

Axiomatic Specification, Examples in ANNAA Brief Overview of AnnaAnna Formal CommentsSlide 4Gas Station ExampleGas Station ExampleSlide 7Slide 8Slide 9Slide 10Slide 11Cruise Control ExampleSlide 13Slide 14Slide 15Slide 16ANNA features utilizedMerits of Axiomatic SpecsDemerits of Axiomatic SpecsExperience with Anna Experience with Anna, Discussion, Q& ACS599 Formal Methods in Software Architectures1Axiomatic Specification, Examples in ANNAEbru DincelAli RampurwalaCS599 Formal Methods in Software Architectures2A Brief Overview of Anna•A Specification Language for ADA•Extensions: –Generalization of existing constructs eg. subprograms– new constructs : eg. exceptions •Formal comments:1) virtual Ada text ( --: ): programming concepts not implemented eg. Length of stack2) annotations (--| ) : Boolean valued expressions•Quantified expressions: forall, existsCS599 Formal Methods in Software Architectures3Anna Formal Comments•Type: used to constrain a type/subtypeSubtype EVEN is INTEGER;--| where X: EVEN => X mod 2 = 0;•Statement: used to specify properties of statementX:=X+1; --| X = in X +1;CS599 Formal Methods in Software Architectures4Anna Formal Comments•Exception: Procedure PUSH(E: in ITEM);--| where in STACK.LENGTH=SIZE=>raise OVERFLOW,--| raise OVERFLOW=> STACK= in STACKCS599 Formal Methods in Software Architectures5Gas Station Example •package body STATION is--| limited to TANK_REGULAR_LEFT,TANK_PLUS_LEFT,TANK_PREMIUM_LEFT,THRESHOLD;--| UNDER_THRESHOLD, IOVERPAID: exception;type GRADE is (REGULAR,PLUS,PREMIUM);•--:function GET_AMOUNT_LEFT(G:GRADE) return FLOAT;•--:function GET_UNIT_PRICE(G:GRADE) return FLOAT;•--:function REFILL_TANK_MAX(G:GRADE);CS599 Formal Methods in Software Architectures6Gas Station Example•type PUMP is record PUMP_NUMBER : NATURAL range 0..3; GAS_GRADE : GRADE; IS_ENABLED : BOOLEAN := FALSE; IS_GRADE_CHOSEN : BOOLEAN := FALSE; METER_READING : FLOAT := 0; LEVER_POSITION_UP : BOOLEAN := FALSE; CURRENT_SPENT, PAID_AMOUNT: INTEGER; end record;•--| where P:PUMP => P.METER_READING <= GET_AMOUNT_LEFT(P.GAS_GRADE);CS599 Formal Methods in Software Architectures7Gas Station Example•type PUMP_GROUP is array (POSITIVE RANGE <>) of PUMP;PG : PUMP_GROUP(0..3);for all PG : PUMP_GROUP => PG(I) = PG(J) => I=J •procedure enable(P : in out PUMP);--| where in P.IS_ENABLED = FALSE,--| out (P.IS_ENABLED = TRUE and P.METER_READING=0 and P.CURRENT_SPENT=0);CS599 Formal Methods in Software Architectures8Gas Station Example•procedure disable(P : in out PUMP);--| where in P.IS_ENABLED = TRUE,--| out P.IS_ENABLED = FALSE;CS599 Formal Methods in Software Architectures9Gas Station Example•procedure fill(P: in out PUMP; PAID_AMOUNT : in FLOAT) isbegin•--| where in (P.IS_ENABLED = TRUE and P.IS_GRADE_CHOSEN = TRUE and P.METER_READING = 0 and P.CURRENT_SPENT = 0 and P.LEVER_POSITION_UP = TRUE);•--| where out (P.IS_ENABLED = FALSE and (P.LEVER_POSITION_UP = FALSE or C.TANK_FULL = TRUE or P.CURRENT_SPENT = P.PAID_AMOUNT));--where C is an instance of the car Package While (P.CURRENT_SPENT<P.PAID_AMOUNT OR C.TANK_FULL=FALSE OR P. LEVER_POSITION_UP=TRUE) fill_discrete(P,P.CURRENT_SPENT,P.PAID_AMOUNT); Loop;end fill;CS599 Formal Methods in Software Architectures10Gas Station Example•procedure fill_discrete(P: in out PUMP; CURRENT_SPENT: in out FLOAT; PAID_AMOUNT : in FLOAT) is begin•--| raise UNDER_THRESHOLD => (GET_AMOUNT_LEFT(P.GAS_GRADE) < THRESHOLD) •--| where out (P.PAID_AMOUNT> P.CURRENT_SPENT and P.LEVER_POSITION_UP = FALSE) raise IOVERPAID,•--| raise IOVERPAID => P.IS_ENABLED = FALSE; CURRENT_SPENT = GET_UNIT_PRICE(P.GAS_GRADE) * P.METER_READING ;end fill_discrete;CS599 Formal Methods in Software Architectures11Gas Station Example•procedure choose_grade(P: in out PUMP); --| where in (P.IS_ENABLED = TRUE)--| out (P.IS_GRADE_CHOSEN = TRUE)•--|axiom --| for all SS: STATION'TYPE => --| P.CURRENT_SPENT <= P.AMOUNT_PAID; end STATION;CS599 Formal Methods in Software Architectures12Cruise Control Example•Assumptions/Clarification: four CC buttons: CC, set_speed, resume, cruise_accelerateCC turns Cruise Control on, set_speed enables Cruise Control.two pedals: pedal_accelerate, brakepedal_decelerate is releasing the pedal.•Exceptions: SpeedTooLow, SpeedTooHigh, CruiseOutofBounds•Procedures: cruise on/off, engine on/off, cruise en/disable, set_speed, pedal/cruise accelerate, brake, pedal_decelerate, resumeCS599 Formal Methods in Software Architectures13Cruise Control Example•Cruise package embodies both the cruise control and the manual operations of the carBOOLEAN IS_ENGINE_ON, IS_CC_ON, IS_ENGINE_ENABLED, IS_CC_ENABLED;INTEGER SPEED, CRUISE_SPEED;--SPEED is the physical speed dynamically updated by calculate_speed function, and CRUISE_SPEED is only set when the Cruise Control is enabled--SpeedTooLowException calls the pedal_accelerate function, SpeedTooHighException calls the brake function internally. Finally, CruiseOutOfBounds calls cruise_disable function•procedure set_speed;--| where in IS_ENGINE_ON=TRUE AND IS_CC_ON=TRUE AND 30<SPEED AND SPEED<90 ,--| out IS_ENGINE_ON=TRUE AND IS_CC_ON=TRUE AND IS_CC_ENABLED=TRUE AND CRUISE_SPEED=SPEED;CS599 Formal Methods in Software Architectures14Cruise Control Example•procedure pedal_accelerate ;--| where in IS_ENGINE_ON=TRUE ,--| out (if in IS_CC_ON=TRUE AND in IS_CC_ENABLED=TRUE) then--| IS_ENGINE_ON=TRUE AND IS_CC_ON=TRUE AND IS_CC_ENABLED=FALSE AND SPEED > in CRUISE_SPEED,--| else IS_ENGINE_ON=TRUE AND IS_CC_ON=in IS_CC_ON AND IS_CC_ENABLED=in IS_CC_ENABLED AND SPEED> in SPEED;•procedure cruise_accelerate ;--| where in IS_ENGINE_ON=TRUE AND IS_CC_ON=TRUE AND IS_CC_ENABLED=TRUE,--| out IS_ENGINE_ON=TRUE AND IS_CC_ON=TRUE AND ((SPEED<90 AND IS_CC_ENABLED=TRUE AND CRUISE_SPEED > in CRUISE_SPEED) || (SPEED>=90 AND IS_CC_ENABLED=FALSE AND SPEED> in CRUISE SPEED));CS599 Formal Methods in Software Architectures15Cruise Control Example•procedure brake;--| where in IS_ENGINE_ON=TRUE,--| out (if in IS_ENGINE_ON=TRUE AND in IS_CC_ON=TRUE AND in IS_CC_ENABLED=TRUE) then--| IS_ENGINE_ON=TRUE AND in IS_CC_ON=TRUE AND in IS_CC_ENABLED=FALSE AND SPEED < in CRUISE_SPEED, --| else IS_CC_ON= in IS_CC_ON AND IS_CC_ENABLED = in IS_CC_ENABLED AND SPEED < in SPEED ;•procedure resume;--| where in IS_ENGINE_ON=TRUE AND IS_CC_ON=TRUE AND IS_CC_ENABLED=FALSE,--| out


View Full Document

USC CSCI 599 - October5a

Documents in this Course
Week8_1

Week8_1

22 pages

Week2_b

Week2_b

10 pages

LECT6BW

LECT6BW

20 pages

LECT6BW

LECT6BW

20 pages

5

5

44 pages

12

12

15 pages

16

16

20 pages

Nima

Nima

8 pages

Week1

Week1

38 pages

Week11_c

Week11_c

30 pages

afsin

afsin

5 pages

October5b

October5b

43 pages

Week11_2

Week11_2

20 pages

final

final

2 pages

c-4

c-4

12 pages

0420

0420

3 pages

Week9_b

Week9_b

20 pages

S7Kriegel

S7Kriegel

21 pages

Week4_2

Week4_2

16 pages

sandpres

sandpres

21 pages

Week6_1

Week6_1

20 pages

4

4

33 pages

Week10_c

Week10_c

13 pages

fft

fft

18 pages

LECT7BW

LECT7BW

19 pages

24

24

15 pages

14

14

35 pages

Week9_c

Week9_c

24 pages

Week11_67

Week11_67

22 pages

Week1

Week1

37 pages

LECT3BW

LECT3BW

28 pages

Week8_c2

Week8_c2

19 pages

Week5_1

Week5_1

19 pages

LECT5BW

LECT5BW

24 pages

Week10_b

Week10_b

16 pages

Week11_1

Week11_1

43 pages

Week7_2

Week7_2

15 pages

Week5_b

Week5_b

19 pages

Week11_a

Week11_a

29 pages

LECT14BW

LECT14BW

24 pages

T7kriegel

T7kriegel

21 pages

0413

0413

2 pages

3

3

23 pages

C2-TSE

C2-TSE

16 pages

10_19_99

10_19_99

12 pages

s1and2-v2

s1and2-v2

37 pages

Week10_3

Week10_3

23 pages

jalal

jalal

6 pages

1

1

25 pages

T3Querys

T3Querys

47 pages

CS17

CS17

15 pages

porkaew

porkaew

20 pages

LECT4BW

LECT4BW

21 pages

Week10_1

Week10_1

25 pages

wavelet

wavelet

17 pages

p289-korn

p289-korn

12 pages

2

2

33 pages

rose

rose

36 pages

9_7_99

9_7_99

18 pages

Week10_2

Week10_2

28 pages

Week7_3

Week7_3

37 pages

Load more
Download October5a
Our administrator received your request to download this document. We will send you the file to your email shortly.
Loading Unlocking...
Login

Join to view October5a and access 3M+ class-specific study document.

or
We will never post anything without your permission.
Don't have an account?
Sign Up

Join to view October5a 2 2 and access 3M+ class-specific study document.

or

By creating an account you agree to our Privacy Policy and Terms Of Use

Already a member?