PowerPoint PresentationSlide 2Slide 3Slide 4Slide 5Slide 6Slide 7Slide 8Slide 9Slide 10Slide 11Slide 12Cruise Control SystemSystem Block DiagramDriver InterfaceBrakes InterfaceAccelerator InterfaceSpeedMeter Interface(1)SpeedMeter Interface(2)Cruise Interface (1)Cruise Interface (2)Cruise Interface (3)Cruise Interface (4)Cruise Interface (5)Cruise Interface (6)The Architecture(1)The Architecture(2)Slide 28CS599 Formal Methods in Software Architectures1Temporal Examples in Rapide•Mohammad Al Said•Miheer Bhachech•Aditya GargCS599 Formal Methods in Software Architectures2Rapide SyntaxArchitecture•architecture_declaration ::= architecture identifier `(' [ parameter_list ] `)' [ return interface_expression ] is [ module_constituent_list ] [ connect { connection } ] end [ architecture ] [ identifier ] `;' •connection ::= pattern connector pattern `;' | other kinds of pattern connections ... •connector ::= `to' | `=>' | `||>'CS599 Formal Methods in Software Architectures3InterfaceThe interface type of a component consists of the set of constituents by which the component communicates with other components.•Interface types are declared using the following syntax: •type_declaration ::= type identifier is interface_expression `;' •interface_type_expression ::= interface { interface_constituent } [ behavior behavior_declaration ] end [ interface ] [ identifier ] •interface_constituent ::= provides { interface_declarative_item } | requires { interface_declarative_item } | action { action_name_declaration } | private { interface_declarative_item } | service { service_declarative_item } | constraint { pattern_constraint_list}CS599 Formal Methods in Software Architectures4Actions and Functions•action_name_declaration ::= action mode identifier `(' [ formal_parameter_list ] `)' `;' •mode ::= in | out •function_name_declaration ::= function identifier `(' [ formal_parameter_list ] `)' [ return type_expression ] `;' •For example, •action in Write(value : Data); function Read() return Data;CS599 Formal Methods in Software Architectures5Tool SupportThere are several tools to assist programmers who want to develop Rapide models of systems. The tools include: •an architecture-based editor for defining system models, •a compiler for producing executables from the system models, •a constraint checking runtime system that is used by an executable to produce a history of the execution, •a graphical browser for viewing histories, and •an animation facility providing another view of histories. •The Rapide Toolset is available for Solaris 2.5, SunOS 4.1.3. and Linux.CS599 Formal Methods in Software Architectures6CS599 Formal Methods in Software Architectures7Gas_StationAssumptions:• Operator schedules pumps to customers.• No mechanism that map customers to the right pump.• Main Gas tank refilling process is not included.• Main Gas Tank is divided into 3 tanks based on Fuel grade. • Car’ Gas tank is not included.CS599 Formal Methods in Software Architectures8type Dollars is Real; type Gallons is Real;type Fuel is Integer; type Customer is interface action out Pre_Pay(Cost : Dollars), Turn_On(), Walk(), Turn_Off(), Select_Grade(Fuel_Grade : Fuel); in Okay(), Change(Cost : Dollars); behavior D : Dollars; FG : Fuel; begin start => Pre_Pay(D);; Okay => Walk;; Okay => Select_Grade(FG); Turn_On();; end Customer;CustomerCS599 Formal Methods in Software Architectures9type Operator is interface action in Request(Cost : Dollars), Refill_Tank(FL : Boolean; Tank : Fuel), Result(Cost : Dollars); out Schedule(Cost : Dollars), behavior Payment : Dollars; Fuel_Level_Low : var Boolean :=False; Tank_Number: Fuel; Action Add_Fuel_To_Tank(Tank : Fuel); Begin (?X : Boolean ; ?Y : Fuel) (Refill_Tank(?X ; ?Y) => Fuel_Level_Low :=?X; Tank_Number :=?Y;; Fuel_Level_Low => Add_Fuel_To_Tank($Tank_Number);; (?X : Dollars)Request(?X) => Payment := ?X; Schedule(?X);; (?X : Dollars)Result(?X) => Remit($Payment - ?X);; end Operator;OperatorCS599 Formal Methods in Software Architectures10type Pump is interface action in On(), Off(), Activate(Cost : Dollars), Select_Fuel_Grade(Fuel_Grade : Fuel), Ok(); out Report(Amount : Gallons; Cost : Dollars), Request_Gas_From_Tank(GT : Fuel); behavior Free : var Boolean := True; Premium_Cost : var Real := 1.9; Plus_Cost : var Real := 1.8; Regular_Cost : var Real :=1.7; Reading, Limit : var Dollars := 0; Gallons_Dispensed : var Gallons :=0; action In_Use(), Done(), Fuel_Grade_Selected(); begin (?X : Dollars)(On ~ Activate(?X) AND Ok) where $Free => Free := False; Limit := ?X; Fuel_Grade_Selected;; Fuel_Grade_Selected => In_Use;; In_Use => if (((?Y : Fuel) Select_Fuel_Grade(?Y) == 1 ) then Reading := $Premium_Cost * $Gallons_Dispensed ) elsif (((?Y : Fuel) Select_Fuel_Grade(?Y) == 2) then Reading := $Plus_Cost * $Gallons_Dispensed ) else Reading := $Regular_Cost * $Gallons_Dispensed endif; Done;; Off or Done => Free := True; Report($Reading);; end Pump;PumpCS599 Formal Methods in Software Architectures11type Fuel_Tank is interface action in Requested_Gas_Type(Fuel_Grade : Fuel); out Ok(), Request_To_Refill_Tank(FL : Boolean ; Tank : Integer); behavior Fuel_Level : var Boolean :=True; Available_Gas , Threshold : Gallons; action Select_Tank_Type(Fuel_Grade : Fuel) , Send_To_Pump(); begin (?FG : Fuel) Request_Gas_Type(?FG) => Select_Tank_Type(?FG);; (Available_Gas <= Threshold ) => Fuel_Level_Ok :=False; Request_To_Refill_Tank($Fuel_Level, ?FG);; Send_To_Pump => Ok;; end Fuel_Tank; Fuel_TankCS599 Formal Methods in Software Architectures12architecture gas_station() return root is O : Operator; P1, P2, P3, P4 : Pump; C1, C2, C3, C4 : Customer; T : Tank; connect (?C : Customer; ?X : Dollars) ?C.Pre_Pay(?X) => O.Request(?X); (?X : Dollars; ?P : Pump) O.Schedule(?X) => ?P.Activate(?X); (?X : Dollars) O.Schedule(?X) => ?C.Okay; (?C : Customer; ?P : Pump; ?F : Fuel) ?C.Select_Grade(?F) => ?P.Select_Fuel_Grade(?F); (?P : Pump; T : Tank; ?F : Fuel) ?P.Request_Gas_From_Tank(?F) => T.Requested_Gas_Type(?F); (?F : Fuel ; FL : Boolean) T.Request_To_Refill_Tank(?FL , ?F) =>
View Full Document
Unlocking...