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