1、A General Framework for Formalizing Object-Oriented Modeling Techniques,Betty H. C. Cheng Software Engineering and Network Systems Laboratory Department of Computer Science and Engineering Michigan State University East Lansing, Michigan 48824 Chengbcse.msu.edu www.cse.msu.edu/chengb,Acknowledgement
2、s,Joint work with the following people: Robert Bourdeau Laura Campbell William McUmber Enoch Wang Ryan Stephenson Sponsored in part by: National Science Foundation Grants: (CCR-9633391, CCR-9901017, EIA-0000433) DARPA Grant (EDCS Program): F30602-96-1-0298 Motorola Eaton Corporation Siemens Automoti
3、ve Detroit Diesel Corporation,Bridge the Gap Between Informal and Formal Methods,Object-Oriented “Blueprints”,Formal Representations,Informal specifications,graphical models,easy for humans toformulate, may be inconsistent andincomplete.,Objective:formal specificationsexecutable codethat can be veri
4、fiedfor correctnessand completeness,Benefits: Automated Analysis Consistency, completeness Rapid Prototyping Behavior SimulationDesign Transformations Test Case generation,Build a Bridge,Automated formalization and integration of the informal models can help properly bridge the two sides,Informal sp
5、ecifications,graphical models,easy for humans toformulate, may be inconsistent andincomplete.,Objective:formal specificationsexecutable codethat can be verifiedfor correctnessand completeness,Overview,Introduction Background/Related Work Formalization Framework Validation: Tool Support Case Study Co
6、nclusions and Future Investigations,Motivation,Embedded systems are difficult to develop Object-Oriented Design can be powerful for embedded systems Diagrammatic notations facilitate abstraction UML is de facto standard Object-Oriented Commonly used More intuitive But diagrams lack formality precise
7、ly predicting behavior is difficult,Objectives and Results,Overarching goals: Broaden base of developers who can use rigorous software engineering techniques Provide palatable path to more rigorous SE techniques Leverage existing expertise and technology Enable use of intuitive diagrammatic notation
8、s (UML) for embedded system design Provide path from UML to existing formal languages Existing user base Support ToolsEnable automated analyses of model Simulation Model checking,Additional Results,Provide precise semantics for diagrams Establish consistency of mapping rules Allow choice of formaliz
9、ation language,Background: Embedded Systems,Code difficult to design and analyze Time-dependent difficult to instrument often highly concurrent High level of robustness required control real-world, physical processes,Background: UML,“General-purpose” visual modeling language de facto Standard (At le
10、ast) nine different diagrams Diagrams described by metamodels: A graphical model that describes syntax of model Therefore, nine different metamodels,UML Class Diagram,Class A,Class A1,Class A2,Class A3,Class B,Class X,UML Metamodel,Metamodel defines UML syntax using class diagram notation. Semantics
11、 not defined by metamodel Note: Any language or diagram syntax can be defined with a metamodel,Example MetaModel,Program,Simple,Statement,Compound,Statement,Block,0*,Metamodel - Diagram - System Relationship,Metamodel,UMLDiagram Instance,Constrains syntax,System,Specifies aspect of,Background: VHDL,
12、IEEE standard language Intended for abstract description of hardware Uses multiple, concurrent, communicating processes Communication through “signals” Syntax is Ada-like, procedural in nature Models can be “executed” in simulation.,Background:VHDL Structure,entity port (sig.),architecture. beginpro
13、cesssig = value;endprocessend,Static description ofprocess interface,Dynamic description of entity behavior,entity port (sig),architecture. beginprocessendprocesswait for sig;end,One “unit” of execution containing multiple processes,Background: Promela (SPIN),Promela is language for SPIN model check
14、er Simulation and model checking of concurrent systems SPIN: commonly used in telecommunication domain Developed by Bell Labs (now Lucent) Protocol verification Guarded Command Language + CSP + C Collection of processes, channels, and variables,Background: Promela Example,typdef A_type int x; int y;
15、 bool unused; mtype vals; chan queue=3 of mtype; A_type A; mtype=on, off, none;init atomic A.x = 1; A.y = 2 run abc() proctype abc() int I; do : A.x 1 - A.y = A.y + 1; A.x = A.x + 1; od; queue!on; if : queue?vals : A.y 4 - goto skip1 fi,“structure” typedef,Guarded statement,Homomorphisms,Preserve op
16、erations, hence structure and semantics,Metamodel mapping,UML metamodel,Formal language metamodel,Homomorphism,Unified Class/Dynamic Metamodel,Model,Class,Relationships,Instance Variables,Aggregation,Generalization,Association,Behavior,State Vertex,Transition,Rest of dynamic model,Class related,Dyna
17、mic related,Dynamic Model Portion of Unified Metamodel,Behavior,State Vertex,Transition,Guard,Pseudostate,State,CompositeState,SimpleState,ActionSequence,Event,SignalEvent,TimeEvent,ChangeEvent,Start,Final,Join,History,01,01,01,01,01,01,01,01,1,1,1*,To Class,Example Metamodel Mapping,h:,Introduction
18、 to Mapping Rules,VHDL used for embedded systems VHDL contains time notations Many commercial tools available Comprehensive simulation capability SPIN used in industry Spin provides model simulation and checking Concurrency is a feature of both,VHDL Class Diagram Mapping Rules,Map static class struc
19、ture to Ent/Arch structure Provide “packages” for VHDL syntactic details, instance variables Map class relationships to port signatures,VHDL Dynamic Diagram Rules,Objects map to entity/architectures States map to processes each process dormant until state name on signal Transitions map to signal ass
20、ignments Composite states map to entity/architectures Other pseudo-states map to special processes,VHDL Mapping Rules Summary,entity port (sig.),architecture. beginprocesssig = value;endprocessend,Class,composite state,Simple state,relationships,Transition/event mechanism,VHDL Analyses,Widely unders
21、tood by and available in embedded systems community Extensive simulation capability “Signal tracing” in some tools Good for timing dependent systems Good for hardware-coupled simulation (if hardware modeled in VHDL),Promela Class Diagram Mapping Rules,Classes (objects) map to proctypes.Relationships
22、 map to channels.Instance variables map to global typdef structures.,Promela Dynamic Model Mapping Rules,Simple states map to blocks of Promela statements. Transitions map to goto and run() Composite states map to proctypes Events map to channel writes/receives Pseudo-states map to blocks of various
23、 Promela statements,SPIN Analyses,Random simulation Exhaustive search of states State transition system checked by temporal logic assertions Often provides counter-examples (path to problem state) “Easier” than theorem proving Better than simulation when precise timing not required,Summary of Mappin
24、gs,VHDL,Promela,Tool Support,MINERVA,Hydra,Analysis Tool*,HIL,Analysis results,Diagram reports,Analysis reports,Spec*,UML,Hydra Translation Tool,Hydra parser,Implements mapping rules for specific language,Uses library and parserto implement rules,Modular per formal language,Language Specific Class L
25、ibrary,HIL,Formal Specifications,Minerva,Architecture of Minerva,UML,Diagram in DoME format,Diagram reports,Analysis reports,Visualization commands,HIL,Analysis results (raw),Analysis results (processed),UML diagram editors,Plug-ins,Text processing scripts,High-Level Design Process Data Flow,Develop
26、 Use case + Context model,Develop Class Model,Develop Dynamic Model,Hydra,Simulation Model checking,Develop Sequence Diagrams,Requirements,context,scenario-info,sequence diagrams,UML Diagrams,formal specs,refinements,class model,scenarios,Case Study: Smart Cruise Control,Validate formalization and a
27、nalyze diagrams Need simulation for initial testing Want to exercise model checking: SPIN / Promela is target language Characteristics: Multiple Objects (object communication) Concurrency (intra- and inter-object),Smart Cruise Requirements,Safety zone,Desired trail distance,Coast zone,Closing zone,A
28、bout 400 ft - acquires target vehicle. Closing speed low enough to control.,Starts coasting to match speed,Safe zone,Maintain proper trail distance - speeds match,Closing speed too high.,Issues warnings to avoid this condition,This is what we want,Class - Context Diagram,Control,Car,Radar,Target acq
29、uisition target loss distance,Car speed throttle control,Car speed,Warnings,Target,Distance,System boundary,ThrottleControl,Brakes,“set”,brakes,Smart Cruise Class Model,Control,Radar,Car,Car speed,Car speed throttle control,Target acquisition target loss distance to target,High Level Radar Dynamic M
30、odel,Get car speed,Check distance,Off,Wait for ack,target = 400target-acquired,target 400,Ack-from-control,Turn-off,Car-speed,Turn-on,car1,car1,car4,car3,Get-speedreal=setspeed,Get-speedrealset/adjust real speedspeed,Set-speed,Get-speedspeed,Unset speed,updatex,updatespd,dogetspd,dounset,Supply spee
31、d to radar,Supply speed to control,Set cruise speed,Car Dynamic Model,Unset cruise speed,High Level Control Dynamic Model,Get speed and distance,Wait for “set”,Wait for target,Warning or Alarm,Check bounds,Closing on target,Maintain Trail position,set,target,closing,trailing,Ack from car,exceed boun
32、ds,SPIN Analyses Performed,Random simulation State reachability State reachability with assertions Progress loop analysis (cycle checks) Model checking with temporal claim Model checking with temporal claim and non-deterministic execution paths.,Use of Simulation,Check that model runs (does not dead
33、lock) Model appears to achieve basic requirements Model not erratic (simulation is random) Exercise common paths Explore extremes for initial proper behavior Basically, high level debugging strategy,State Reachability Analysis,Reachability is exhaustive (unlike simulation) For common scenarios, ensu
34、re state set correct and exception states not entered For exception scenarios, ensure exception states entered,State Reachability for Normal Scenario,Get speed and distance,Wait for “set”,Wait for target,Warning or Alarm,Check bounds,Closing on target,Maintain Trail position,set,target,closing,trail
35、ing,Only unreached state, as expected,Ack from car,control dynamic model,(Establish target trail),= reached,exceed bounds,SPIN Progress Loop Analysis,Ensures no cycles of only unmarked states.Reports cycles unless state(s) are marked. If nothing marked, reports cycles If known cycles are marked, rep
36、orts unexpected cycles,Progress Cycle Analysis of Model,Liveness check: Ensure state cycle “follow target” established Differs from reachability by ensuring cycle exists, not just state visit.Safety check: Ensure no unexpected cycles encountered,Progress Loop Checks,Get speed and distance,Wait for “
37、set”,Wait for target,Warning or Alarm shut off system,Check bounds,Closing on target,Maintain Trail position,set,target,closing,trailing,1. Blue states reported as cycle when unmarked,2. After marked, no other cycles appeared (complement of first check),None of these reported,Ack from car,Model Chec
38、king Tests,Car achieves trail position, and stays there. Three checks: Once in idle, model never comes back when target sent, ack replied Remove ack to demonstrate check worksBrake application leads to return to idle state. Revealed missed an event on transition,Hand Written Never Claim,/* Verifies
39、that at low enough closure speeds, the car comes up behind thetarget and stays there forever. If the trail loop is exited, we returnto state idle */ 1: never 2: /* wait until state idle is entered */ 3: do 4: : skip 5: : controlcontrolpididle - break 6: od; /* now wait until state idle is exited */
40、7: do 8: : skip 9: : !(controlcontrolpididle) - break 10: od; /* and if we come back to state idle, its an error */ 11: do 12: : controlcontrolpididle - break 13: od ,A never claim specifying that state idle isonly entered once, at the start of execution.,Analysis Output From Hand-Written Never Clai
41、m,warning: for p.o. reduction to be valid the never claim must be stutter-closed (never claims generated from LTL formulae are stutter-closed) (Spin Version 3.3.1 - 11 July 1999)+ Partial Order ReductionFull statespace search for:never-claim +assertion violations + (if within scope of claim)acceptan
42、ce cycles + (fairness disabled)invalid endstates - (disabled by never-claim)State-vector 504 byte, depth reached 3114, errors: 06314 states, stored2919 states, matched9233 transitions (= stored+matched)3445 atomic steps hash conflicts: 72 (resolved) (max size 218 states)4.565 memory usage (Mbyte),No
43、 mention of failing claimor “acceptance cycles”. Implies claim succeeded.,SPIN Generated Never Claim for “p leads-to q”,never /* !(p - q)*/ /* 0,0 goto accept_S4: (1) - goto T0_initfi; accept_S4:if: (! (q) - goto T0_S4fi; T0_S4:if: (! (q) - goto accept_S4fi; accept_all:skip ,Always(p implies eventua
44、lly q),p leads-to q which is the same as:,p leads-to q frequently used assertion for liveness,Ensure target Never Missed,Control,Radar,Target acquired,acknowledgement,Using: always(p implies eventually q),This check succeeded,Never, not always(p implies eventually q),SPIN version for claim,Demonstra
45、te Check Works,Control,Radar,Target acquired,acknowledgement,This check failed (as expected),Remove this message to force claim to fail,warning: for p.o. reduction to be valid the never claim must be stutter-closed (never claims generated from LTL formulae are stutter-closed) pan: acceptance cycle (
46、at depth 298) pan: wrote sc.v9.pr.trail (Spin Version 3.3.1 - 11 July 1999) Warning: Search not completed + Partial Order ReductionFull statespace search for:never-claim +assertion violations + (if within scope of claim)acceptance cycles + (fairness disabled)invalid endstates - (disabled by never-cl
47、aim)State-vector 500 byte, depth reached 299, errors: 1134 states, stored (135 visited)1 states, matched136 transitions (= visited+matched)32 atomic steps hash conflicts: 0 (resolved) (max size 218 states),Check Demonstration: target leads-to ack failing never claim output,Acceptance cycle in never
48、claim. Implies claim has failed.,Never claim is p leads-to q. p is target, q is acknowledgement.,Non-deterministic Paths (checking brake signal behavior),r3,tmode & x400control.lost,tmode & x=400control.dist(x),tmode & x=400control.brakes,Non-deterministic choice between these two transitions. Either is possible after x=400,New transition added for verification. Send brakes at random times.,Matching guards,Never Claim to Test Brakes,
