State-based SpecificationSlide 2BenefitsConceptsConcepts (2)Techniques and MethodsStatechartsDecomposition in StatechartsPowerPoint PresentationDefault and History StatesOrthogonalitySlide 12Semantics of statechartsAdditional featuresIntegration With Other MethodsMerits and demeritsRequirements ModelingSCR ConceptsSCR SemanticsSCR ExampleFormalizing SCR RequirementsModel CheckingRequirements to CTL MachinesInvariant PropertiesSlide 25Merits & DemeritsA Specification LANguageNotationMathematical ApproachASLAN ExampleEntry & Exit AssertionsTop level specificationNo Change StatesUnparametrized ExampleProcedural vs. NonproceduralMerits and DemeritsReal-Time Systems and Object ParadigmModeling Real-Time BehaviorEvent-driven behavior modelingUML State MachinesHierarchical states and transitionsTime-driven behavior modelingModeling Inter-object BehaviorArchitectural ModelingRose RealTimeSlide 46State-based SpecificationMiheer Bhachech, Ebru Dincel, Nikunj MehtaState-based Specification•Describe behavior of a system in terms of possible states and transitions–Capture the condition of a system in terms of its state•Hardware and control systems where the behavior of a system is reactive•State-based specification techniques have:–Explicit description and complete coverage of states and transitions–Specification language and formal reasoning–Precise mathematics–Analysis toolsBenefits•Objectives–Clarify requirements–Locate and correct inconsistency and non-determinism–Refine requirements consistently into design–Decomposition of system–Prove or disprove assertions about system behavior•End Result–Predictably safe systems, more deterministic behavior–Links between customer needs and system designConcepts•State–A state represents the computational readiness of a system at that instance of time during its lifetime•Initial state–The state in which a system starts•Condition–Represents an existing on-going state of the system•Quantification–The application of a condition over more than one variableConcepts (2)•Transition–A transition is a change in the state of the system•Event–An event is an instantaneous change in the environmental or internal condition of a system.•Action/activity–The function that is carried out or the event that is emitted upon the transition of the system from one state to another•Invariant–A global or local property that holds true for the duration of the system lifetimeTechniques and Methods•Finite state machines•Augmented transition networks•SDL•Petri nets•Sequence diagrams•Statecharts•Computational tree logic•ASLAN specifications•UML state diagramsStatecharts•Purpose–Specification and design of discrete-event systems–Provide behavioral description of reactive systemsWhen event α occurs in state A and condition C is true, transfer state to B•Features–State-transition diagrams–Hierarchy, concurrency and communication–Uses area and location of graphical objects–Statecharts = state diagrams + depth + orthogonality + broadcast-communicationDecomposition in Statecharts•Use of higraphs–Hierarchical graph•Super-states –Exclusive-OR combination of states–Economize number of arrows•Abstraction or refinement?–Capture a common property–Bottom up and top-down•Exclusive disjunction of individual states•ZoomingBDadbACg(P)BDadbdisplaysalarms-beepalarm1 beepsboth beepalarm2 beepsT hits T1 (P1)any button pressed30 sec in alarms-beepT hits T1 (P)T hits T2 (P2)displaysalarms-beepT hits T1 (P1)any button pressed30 sec in alarms-beepT hits T1 (P)T hits T2 (P2)Default and History States•Default states–Equivalent to start states for FSM•History–(H) Record of the last state at the current level–(H*) Deep history stores last state at all levels current and belowAADADalarm1offond dHKGHH*ABCDEOrthogonality•AND combination of states •Concurrency and synchronization–Simultaneous transitions in component states•Independence–Independent transition in one of the component state•Orthogonality = concurrency + independence•Communication among states by common events•Exits–Synchronized, independent and -transition exitABDCabin (G)GEgFdaYSemantics of statecharts•Challenges–Depth of states, non-determinism, concurrency–Use of communication mechanism for concurrency–One part generates and all other parts sense it–Atomic event propagation•State machine–State tree and a set of transitions–Nextstep(X, C, E)–Select relevant transitions by analyzing trigger for E–Check source configuration for ancestral relation of X–Analyze consequences of applying actions of transition–Generate next full basic configurationAdditional features•Condition and selection entrances–Abbreviated decisions•Parameterized states–Repeating structure across states,•Delays and timeouts–Prevent starvation and deadlocks•Overlapping states–Convert XOR into OR•Non-determinism–Assign probabilities to transitionsIntegration With Other Methods•Pure statecharts represent control part only–Internal state change•Actions and activities–Generate events and change value of conditions•Activity charts for functional description•Module charts for structural description•Specify eventualities, absence of deadlocks, timing constraints using TL–Synthesis of statecharts from TL specs–Describe scenarios using TL and derive statecharts from a large set of scenariosMerits and demerits•No explosive growth of states•Can be refined into designs•Simple but powerful notation and techniques•Tool support for editing and analysis - STATEMATE•Strong semantic underpinning•Rich graphical notation•Difficult to synthesize complex systems•Mapping between hierarchies of states and hierarchies of objectsRequirements Modeling•Applicable to verify–Safety properties of event-driven systems•Premise–Informal requirements specs–Implicit assumptions about the system•Formal Method–Requirement specs•An informal description of system behavior–Formalizing requirements•Adding the implicit assumptions in the specs•Dealing with non-determinism, ambiguity–Automated Model checking using logical formulasSCR Concepts•Mode–Set of system states that share a common property•Modeclass–Set of modes, describing one aspect of the system’s behavior•Mode transition–Occurs between modes in the same modeclass due to system
View Full Document
Unlocking...